diff --git a/.github/workflows/c-cpp.yml b/.github/workflows/c-cpp.yml index f9d60434..710738d9 100644 --- a/.github/workflows/c-cpp.yml +++ b/.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}}/ diff --git a/.github/workflows/macOS.yml b/.github/workflows/macOS.yml index 0b72912f..2fdc1c70 100644 --- a/.github/workflows/macOS.yml +++ b/.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; diff --git a/.github/workflows/regress.yml b/.github/workflows/regress.yml index 249d7ece..5ac73660 100644 --- a/.github/workflows/regress.yml +++ b/.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 diff --git a/README.md b/README.md index 375394f0..b1c0ea75 100644 --- a/README.md +++ b/README.md @@ -64,9 +64,9 @@ cmake .. -DCMAKE_BUILD_TYPE=Release \ ```bash # Classic -"build/src/bin/kepler_formal <-verilog/-naja_if> [...]" +"build/src/bin/kepler-formal <-verilog/-naja_if> [...]" # Through yaml config file -"build/src/bin/kepler_formal --config " +"build/src/bin/kepler-formal --config " ``` ## Example diff --git a/example/README.md b/example/README.md index da3868c5..a743b650 100644 --- a/example/README.md +++ b/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 ``` diff --git a/src/bin/CMakeLists.txt b/src/bin/CMakeLists.txt index bf576969..df030f2b 100644 --- a/src/bin/CMakeLists.txt +++ b/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}) diff --git a/src/bin/KeplerFormal.cpp b/src/bin/KeplerFormal.cpp index ee94c780..f4e828cf 100644 --- a/src/bin/KeplerFormal.cpp +++ b/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(); } + // Add log file name + if (cfg["log_file"] && cfg["log_file"].IsScalar()) { + logFileName = cfg["log_file"].as(); + } + 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 { diff --git a/src/strategies/miter/BuildPrimaryOutputClauses.cpp b/src/strategies/miter/BuildPrimaryOutputClauses.cpp index 4ac3fff4..661a9e1c 100644 --- a/src/strategies/miter/BuildPrimaryOutputClauses.cpp +++ b/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) diff --git a/src/strategies/miter/MiterStrategy.cpp b/src/strategies/miter/MiterStrategy.cpp index c04dfff0..7e0c3d44 100644 --- a/src/strategies/miter/MiterStrategy.cpp +++ b/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 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( logFileName, true); logger = std::make_shared("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& inputs0, std::vector& inputs1, @@ -328,11 +347,25 @@ 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 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); } } @@ -340,12 +373,12 @@ void MiterStrategy::normalizeOutputs( 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 topModels; topModels.push_back(top0_); topModels.push_back(top1_); diff --git a/src/strategies/miter/MiterStrategy.h b/src/strategies/miter/MiterStrategy.h index 339044c2..4581858e 100644 --- a/src/strategies/miter/MiterStrategy.h +++ b/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::vector>, naja::DNL::DNLID>& outputs0Map, const std::map, std::vector>, naja::DNL::DNLID>& outputs1Map); - + static std::string logFileName_; private: std::shared_ptr buildMiter( const tbb::concurrent_vector>& A, const tbb::concurrent_vector>& B) const; - + static naja::NL::SNLDesign* top0_; static naja::NL::SNLDesign* top1_; tbb::concurrent_vector POs0_; diff --git a/thirdparty/naja b/thirdparty/naja index 7093e127..ee3d489e 160000 --- a/thirdparty/naja +++ b/thirdparty/naja @@ -1 +1 @@ -Subproject commit 7093e127c5ead385cd0044f105c72b25eac3eca5 +Subproject commit ee3d489e8f5d9b0d3d026b73eef6c965b83bbe3a