Verilog

.github/workflows/c-cpp.yml

@@ -30,7 +30,7 @@ jobs:
         sudo apt-get install -yq \
           build-essential cmake ninja-build clang pkg-config \
           libboost-dev libfl-dev libtbb-dev capnproto libcapnp-dev \
-          libgtest-dev libspdlog-dev libfmt-dev
+          libgtest-dev libspdlog-dev libfmt-dev libboost-iostreams-dev zlib1g-dev
 
     - name: Configure CMake
       working-directory: ${{github.workspace}}/

.github/workflows/macOS.yml

@@ -27,7 +27,7 @@ jobs:
       run: git submodule update --init --recursive
     # install dependencies
     - name: Install dependencies
-      run: brew install cmake doxygen capnp tbb bison flex boost spdlog
+      run: brew install cmake doxygen capnp tbb bison flex boost spdlog zlib
     - name: set env variable
       run: |
         echo "/usr/local/opt/flex/bin" >> $GITHUB_PATH; echo "/usr/local/opt/bison/bin" >> $GITHUB_PATH;

.github/workflows/regress.yml

@@ -30,7 +30,7 @@ jobs:
     - name: Checkout submodules
       run: git submodule update --init --recursive
     - name: Install boost & capnproto
-      run: sudo apt-get update && sudo apt-get install -y pkg-config libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev libspdlog-dev 
+      run: sudo apt-get update && sudo apt-get install -y pkg-config libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev libspdlog-dev libboost-iostreams-dev zlib1g-dev
 
     - name: Configure CMake
       run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20
@@ -51,7 +51,7 @@ jobs:
       run: |
         mkdir -p regress-output
         # Run kepler-formal on the example files (files are in example/)
-        ./build/src/bin/kepler_formal -naja_if \
+        ./build/src/bin/kepler-formal -naja_if \
           ./example/tinyrocket_naja.if \
           ./example/tinyrocket_naja.if \
           ./example/NangateOpenCellLibrary_typical.lib \
@@ -63,7 +63,7 @@ jobs:
       run: |
         mkdir -p regress-output
         # Run kepler-formal on the example files (files are in example/)
-        ./build/src/bin/kepler_formal -verilog \
+        ./build/src/bin/kepler-formal -verilog \
           ./example/tinyrocket.v \
           ./example/tinyrocket.v \
           ./example/NangateOpenCellLibrary_typical.lib \
@@ -82,14 +82,14 @@ jobs:
       run: |
         mkdir -p regress-output
         # Run kepler-formal on the example files (files are in example/)
-        ../build/src/bin/kepler_formal --config test_config_naja_if.yaml
+        ../build/src/bin/kepler-formal --config test_config_naja_if.yaml
 
     - name: Run on verilog edited
       working-directory: ${{github.workspace}}/example
       run: |
         mkdir -p regress-output
         # Run kepler-formal on the example files (files are in example/)
-        ../build/src/bin/kepler_formal --config test_config_verilog.yaml
+        ../build/src/bin/kepler-formal --config test_config_verilog.yaml
 
 
 

README.md

@@ -64,9 +64,9 @@ cmake .. -DCMAKE_BUILD_TYPE=Release \
 
 ```bash
 # Classic 
-"build/src/bin/kepler_formal <-verilog/-naja_if> <netlist1> <netlist2> [<liberty-file>...]"
+"build/src/bin/kepler-formal <-verilog/-naja_if> <netlist1> <netlist2> [<liberty-file>...]"
 # Through yaml config file
-"build/src/bin/kepler_formal --config <yaml file>"
+"build/src/bin/kepler-formal --config <yaml file>"
 ```
 
 ## Example 

example/README.md

@@ -7,10 +7,10 @@ cd example
 pip install najaeda
 python edit.py
 # For naja_if
-../build/src/bin/kepler_formal -naja_if tinyrocket_naja.if tinyrocket_naja_edited.if NangateOpenCellLibrary_typical.lib fakeram45_1024x32.lib fakeram45_64x32.lib
+../build/src/bin/kepler-formal -naja_if tinyrocket_naja.if tinyrocket_naja_edited.if NangateOpenCellLibrary_typical.lib fakeram45_1024x32.lib fakeram45_64x32.lib
 # For verilog
-../build/src/bin/kepler_formal -verilog tinyrocket_pre_edited.v tinyrocket_edited.v NangateOpenCellLibrary_typical.lib fakeram45_1024x32.lib /example/fakeram45_64x32.lib
+../build/src/bin/kepler-formal -verilog tinyrocket_pre_edited.v tinyrocket_edited.v NangateOpenCellLibrary_typical.lib fakeram45_1024x32.lib /example/fakeram45_64x32.lib
 # Through config file
-../build/src/bin/kepler_formal --config test_config_naja_if.yaml
-../build/src/bin/kepler_formal --config test_config_verilog.yaml 
+../build/src/bin/kepler-formal --config test_config_naja_if.yaml
+../build/src/bin/kepler-formal --config test_config_verilog.yaml 
 ```

src/bin/CMakeLists.txt

@@ -1,11 +1,11 @@
 # Copyright 2024-2025 keplertech.io
 # SPDX-License-Identifier: GPL-3.0-only
 
-add_executable(kepler_formal KeplerFormal.cpp)
-target_include_directories(kepler_formal SYSTEM BEFORE PUBLIC ${Boost_INCLUDE_DIR})
-target_include_directories(kepler_formal PUBLIC ${ARGPARSE_DIR})
+add_executable(kepler-formal KeplerFormal.cpp)
+target_include_directories(kepler-formal SYSTEM BEFORE PUBLIC ${Boost_INCLUDE_DIR})
+target_include_directories(kepler-formal PUBLIC ${ARGPARSE_DIR})
 
-target_link_libraries(kepler_formal
+target_link_libraries(kepler-formal
   PRIVATE
     naja_snl_pyloader
     naja_dnl
@@ -15,5 +15,5 @@ target_link_libraries(kepler_formal
     ${SPDLOG_TARGET}
 )
 
-install(TARGETS kepler_formal DESTINATION ${CMAKE_INSTALL_BINDIR})
+install(TARGETS kepler-formal DESTINATION ${CMAKE_INSTALL_BINDIR})
 

src/bin/KeplerFormal.cpp

@@ -59,6 +59,9 @@ int main(int argc, char** argv) {
 
   // Check for config mode (--config or -c). If present, YAML takes precedence.
   bool usedConfig = false;
+
+  std::string logFileName;
+
   for (int i = 1; i < argc; ++i) {
     std::string a = argv[i];
     if (a == "--config" || a == "-c") {
@@ -94,6 +97,11 @@ int main(int argc, char** argv) {
           logLevel = cfg["log_level"].as<std::string>();
         }
 
+        // Add log file name
+        if (cfg["log_file"] && cfg["log_file"].IsScalar()) {
+          logFileName = cfg["log_file"].as<std::string>();
+        }
+
         usedConfig = true;
       } catch (const std::exception& e) {
         SPDLOG_CRITICAL("Failed to parse config {}: {}", cfgPath, e.what());
@@ -253,7 +261,7 @@ int main(int argc, char** argv) {
   // 4. Hand off to the rest of the editing/analysis workflow
   // --------------------------------------------------------------------------
   try {
-    KEPLER_FORMAL::MiterStrategy MiterS(top0, top1);
+    KEPLER_FORMAL::MiterStrategy MiterS(top0, top1, logFileName);
     if (MiterS.run()) {
       SPDLOG_INFO("No difference was found.");
     } else {

src/strategies/miter/BuildPrimaryOutputClauses.cpp

@@ -360,7 +360,7 @@ void BuildPrimaryOutputClauses::collect() {
     KeyT key{ path, std::move(ids) };
     outputsMap_[std::move(key)]  =
             output;
-    printf("Output collected: %s\n", naja::DNL::get()
+    DEBUG_LOG("Output collected: %s\n", naja::DNL::get()
                                          ->getDNLTerminalFromID(output)
                                          .getSnlBitTerm()
                                          ->getName()
@@ -395,7 +395,7 @@ void BuildPrimaryOutputClauses::build() {
   tbb::task_arena arena(40);
   auto processOutput = [&](size_t i) {
     DNLID out = outputs_[i];
-    printf("Procssing output %zu/%zu: %s\n", ++processedOutputs,
+    DEBUG_LOG("Procssing output %zu/%zu: %s\n", ++processedOutputs,
            outputs_.size(),
            get()
                ->getDNLTerminalFromID(out)

src/strategies/miter/MiterStrategy.cpp

@@ -34,6 +34,7 @@ using namespace KEPLER_FORMAL;
 
 SNLDesign* MiterStrategy::top0_ = nullptr;
 SNLDesign* MiterStrategy::top1_ = nullptr;
+std::string MiterStrategy::logFileName_ = "";
 namespace {
 
 static std::shared_ptr<spdlog::logger> logger;
@@ -45,6 +46,10 @@ void ensureLoggerInitialized() {
       // already exist and then crete mitter_log_(x+1).txt
       int logIndex = 0;
       while (true) {
+        if (MiterStrategy::logFileName_ != "") {
+          logIndex = -1;
+          break;
+        }
         std::string logFileName =
             "miter_log_" + std::to_string(logIndex) + ".txt";
         std::ifstream infile(logFileName);
@@ -56,6 +61,13 @@ void ensureLoggerInitialized() {
       }
       std::string logFileName =
           "miter_log_" + std::to_string(logIndex) + ".txt";
+      if (MiterStrategy::logFileName_ != "") {
+        if (!MiterStrategy::logFileName_.empty()) {
+            std::filesystem::path p(MiterStrategy::logFileName_);
+            std::filesystem::create_directories(p.parent_path());
+            logFileName = p.string();
+        }
+      }
       auto file_sink = std::make_shared<spdlog::sinks::basic_file_sink_mt>(
           logFileName, true);
       logger = std::make_shared<spdlog::logger>("miter_logger", file_sink);
@@ -225,6 +237,13 @@ Glucose::Lit tseitinEncode(
 
 }  // namespace
 
+ MiterStrategy::MiterStrategy(naja::NL::SNLDesign* top0, naja::NL::SNLDesign* top1, const std::string& logFileName, const std::string& prefix)
+      : prefix_(prefix) {
+    top0_ = top0;
+    top1_ = top1;
+    logFileName_ = logFileName;
+  }
+
 void MiterStrategy::normalizeInputs(
     std::vector<naja::DNL::DNLID>& inputs0,
     std::vector<naja::DNL::DNLID>& inputs1,
@@ -328,24 +347,38 @@ void MiterStrategy::normalizeOutputs(
   for (const auto& [path0, output0] : outputs0Map) {
     if (pathsCommon.find(path0) == pathsCommon.end()) {
       diff0.push_back(output0);
+      std::string fullName;
+      for (const auto& name : path0.first) {
+        fullName += name.getString() + ".";
+      }
+      fullName += std::to_string(path0.second[0]) + ".";
+      fullName += std::to_string(path0.second[1]);
+      logger->info("Will ignore the analysis for: {} from netlist 0 as it does not exist in netlist 1", fullName);
     }
   }
   std::vector<naja::DNL::DNLID> diff1;
   for (const auto& [path1, output1] : outputs1Map) {
     if (pathsCommon.find(path1) == pathsCommon.end()) {
+      std::string fullName;
+      for (const auto& name : path1.first) {
+        fullName += name.getString() + ".";
+      }
+      fullName += std::to_string(path1.second[0]) + ".";
+      fullName += std::to_string(path1.second[1]);
+      logger->info("Will ignore the analysis for: {} from netlist 1 as it does not exist in netlist 0", fullName);
       diff1.push_back(output1);
     }
   }
   outputs0.clear();
   for (const auto& path : pathsCommon) {
     outputs0.push_back(outputs0Map.at(path));
   }
-  outputs0.insert(outputs0.end(), diff0.begin(), diff0.end());
+  //outputs0.insert(outputs0.end(), diff0.begin(), diff0.end());
   outputs1.clear();
   for (const auto& path : pathsCommon) {
     outputs1.push_back(outputs1Map.at(path));
   }
-  outputs1.insert(outputs1.end(), diff1.begin(), diff1.end());
+  //outputs1.insert(outputs1.end(), diff1.begin(), diff1.end());
   logger->debug("size of common outputs: {}", pathsCommon.size());
   logger->debug("size of diff0 outputs: {}", diff0.size());
   logger->debug("size of diff1 outputs: {}", diff1.size());
@@ -484,6 +517,24 @@ bool MiterStrategy::run() {
     for (size_t i = 0; i < POs0.size(); ++i) {
       if (builder0.getOutputs2OutputsIDs().at(builder0.getDNLIDforOutput(i)) !=
           builder1.getOutputs2OutputsIDs().at(builder1.getDNLIDforOutput(i))) {
+        auto path0 = builder0.getOutputs2OutputsIDs().at(builder0.getDNLIDforOutput(i));
+        auto path1 = builder1.getOutputs2OutputsIDs().at(builder1.getDNLIDforOutput(i));
+        // print path0
+        for (const auto& name : path0.first) {
+          logger->info("%s.", name.getString().c_str());
+        }
+        for (const auto& id : path0.second) {
+          logger->info("%lu.", id);
+        }
+        logger->info("\n");
+        // print path1
+        for (const auto& name : path1.first) {
+          logger->info("%s.", name.getString().c_str());
+        }
+        for (const auto& id : path1.second) {
+          logger->info("%lu.", id);
+        }
+        logger->info("\n");
         throw std::runtime_error("Miter PO index " + std::to_string(i) +
                                  " DNLIDs do not match");
       }
@@ -506,6 +557,25 @@ bool MiterStrategy::run() {
         logger->info("Found difference for PO: {}", i);
         // logger->info("Clause 0 {}", POs0[i]->toString());
         // logger->info("Clause 1 {}", POs1[i]->toString());
+        // print path of index i
+        auto path0 = builder0.getOutputs2OutputsIDs().at(builder0.getDNLIDforOutput(i));
+        std::string pathString = "";
+        for (const auto& name : path0.first) {
+          pathString += name.getString() + ".";
+        }
+        for (const auto& id : path0.second) {
+          pathString += std::to_string(id) + ".";
+        }
+        logger->info("Path of differing PO {}: {}", i, pathString);
+        auto path1 = builder1.getOutputs2OutputsIDs().at(builder1.getDNLIDforOutput(i));
+        std::string pathString1 = "";
+        for (const auto& name : path1.first) {
+          pathString1 += name.getString() + ".";
+        }
+        for (const auto& id : path1.second) {
+          pathString1 += std::to_string(id) + ".";
+        }
+        logger->info("Path of differing PO {}: {}", i, pathString1);
         std::vector<naja::NL::SNLDesign*> topModels;
         topModels.push_back(top0_);
         topModels.push_back(top1_);

src/strategies/miter/MiterStrategy.h

@@ -18,11 +18,7 @@ namespace KEPLER_FORMAL {
 
 class MiterStrategy {
  public:
-  MiterStrategy(naja::NL::SNLDesign* top0, naja::NL::SNLDesign* top1, const std::string& prefix = "")
-      : prefix_(prefix) {
-    top0_ = top0;
-    top1_ = top1;
-  }
+  MiterStrategy(naja::NL::SNLDesign* top0, naja::NL::SNLDesign* top1, const std::string& logFileName = "", const std::string& prefix = "");
 
   bool run();
 
@@ -36,12 +32,12 @@ class MiterStrategy {
                         const std::map<std::pair<std::vector<NLName>, std::vector<NLID::DesignObjectID>>, naja::DNL::DNLID>& outputs0Map,
                         const std::map<std::pair<std::vector<NLName>, std::vector<NLID::DesignObjectID>>, naja::DNL::DNLID>& outputs1Map);
 
-
+  static std::string logFileName_;
  private:
   std::shared_ptr<BoolExpr> buildMiter(
       const tbb::concurrent_vector<std::shared_ptr<BoolExpr>>& A,
       const tbb::concurrent_vector<std::shared_ptr<BoolExpr>>& B) const;
-
+  
   static naja::NL::SNLDesign* top0_;
   static naja::NL::SNLDesign* top1_;
   tbb::concurrent_vector<BoolExpr> POs0_;