diff --git a/example/tinyrocket_naja_edited.if/db_implementation.snl b/example/tinyrocket_naja_edited.if/db_implementation.snl new file mode 100644 index 00000000..6d5f7c84 Binary files /dev/null and b/example/tinyrocket_naja_edited.if/db_implementation.snl differ diff --git a/example/tinyrocket_naja_edited.if/db_interface.snl b/example/tinyrocket_naja_edited.if/db_interface.snl new file mode 100644 index 00000000..7f94fbaa Binary files /dev/null and b/example/tinyrocket_naja_edited.if/db_interface.snl differ diff --git a/example/tinyrocket_naja_edited.if/snl.mf b/example/tinyrocket_naja_edited.if/snl.mf new file mode 100644 index 00000000..aeb39ed6 --- /dev/null +++ b/example/tinyrocket_naja_edited.if/snl.mf @@ -0,0 +1,7 @@ +################################################################################ +# Fri Jan 2 15:15:16 2026 +# SNL manifest +# naja version: 0.3.2 +# Git hash: 220af8e +################################################################################ +V 0 1 0 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index f4db0756..650425a3 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -5,4 +5,5 @@ add_subdirectory(bin) add_subdirectory(formal) add_subdirectory(strategies) add_subdirectory(clauses) -add_subdirectory(utils) \ No newline at end of file +add_subdirectory(utils) +add_subdirectory(scope) \ No newline at end of file diff --git a/src/bin/CMakeLists.txt b/src/bin/CMakeLists.txt index efeff3ac..4fac4c88 100644 --- a/src/bin/CMakeLists.txt +++ b/src/bin/CMakeLists.txt @@ -11,6 +11,7 @@ target_link_libraries(kepler-formal naja_dnl naja_opt formal_strategies + scope_extraction yaml-cpp ${SPDLOG_TARGET} ) diff --git a/src/bin/KeplerFormal.cpp b/src/bin/KeplerFormal.cpp index a34407c9..0f0a3fa2 100644 --- a/src/bin/KeplerFormal.cpp +++ b/src/bin/KeplerFormal.cpp @@ -23,6 +23,7 @@ #include "SNLVRLConstructor.h" #include "SNLVRLDumper.h" #include "SNLUtils.h" +#include "ScopeExtraction.h" static void print_usage(const char* prog) { std::printf( @@ -43,7 +44,7 @@ static std::vector yamlToVector(const YAML::Node& node) { int main(int argc, char** argv) { using namespace std::chrono; - enum class FormatType { VERILOG, SNL }; + enum class FormatType { VERILOG, NAJA_IF }; // Default values FormatType inputFormatType = FormatType::VERILOG; @@ -62,6 +63,9 @@ int main(int argc, char** argv) { std::string logFileName; + bool useScopes = false; + bool cleanScopes = false; + for (int i = 1; i < argc; ++i) { std::string a = argv[i]; if (a == "--config" || a == "-c") { @@ -77,7 +81,7 @@ int main(int argc, char** argv) { if (cfg["format"] && cfg["format"].IsScalar()) { std::string fmt = cfg["format"].as(); if (fmt == "naja_if" || fmt == "naja-if" || fmt == "snl") - inputFormatType = FormatType::SNL; + inputFormatType = FormatType::NAJA_IF; else if (fmt == "verilog" || fmt == "v") inputFormatType = FormatType::VERILOG; else { @@ -101,6 +105,16 @@ int main(int argc, char** argv) { if (cfg["log_file"] && cfg["log_file"].IsScalar()) { logFileName = cfg["log_file"].as(); } + + // use_scopes + if (cfg["use_scopes"] && cfg["use_scopes"].IsScalar()) { + useScopes = cfg["use_scopes"].as(); + } + + // clean_scopes + if (cfg["clean_scopes"] && cfg["clean_scopes"].IsScalar()) { + cleanScopes = cfg["clean_scopes"].as(); + } usedConfig = true; } catch (const std::exception& e) { @@ -121,7 +135,7 @@ int main(int argc, char** argv) { std::string formatType = argv[1]; if (formatType == "-naja_if" || formatType == "-naja-if") { - inputFormatType = FormatType::SNL; + inputFormatType = FormatType::NAJA_IF; } else if (formatType == "-verilog") { inputFormatType = FormatType::VERILOG; } else { @@ -162,7 +176,7 @@ int main(int argc, char** argv) { spdlog::set_level(spdlog::level::info); std::printf("KEPLER FORMAL: Run.\n"); - std::printf("Input format: %s\n", (inputFormatType == FormatType::SNL) ? "SNL" : "VERILOG"); + std::printf("Input format: %s\n", (inputFormatType == FormatType::NAJA_IF) ? "SNL" : "VERILOG"); std::printf("Netlist 1: %s\n", inputPaths[0].c_str()); std::printf("Netlist 2: %s\n", inputPaths[1].c_str()); if (!libertyFiles.empty()) { @@ -238,6 +252,7 @@ int main(int argc, char** argv) { } if (inputFormatType == FormatType::VERILOG) { + printf("Parsing verilog file: %s\n", inputPaths[1].c_str()); auto designLibrary = NLLibrary::create(db1, NLName("DESIGN")); SNLVRLConstructor constructor(designLibrary); constructor.construct(inputPaths[1].c_str()); @@ -274,18 +289,56 @@ int main(int argc, char** argv) { // -------------------------------------------------------------------------- // 4. Hand off to the rest of the editing/analysis workflow // -------------------------------------------------------------------------- - try { - KEPLER_FORMAL::MiterStrategy MiterS(top0, top1, logFileName); - if (MiterS.run()) { - SPDLOG_INFO("No difference was found."); - } else { - SPDLOG_INFO("Difference was found. Please refer to the log(miter_log_x.txt) for details."); + if (inputFormatType == FormatType::NAJA_IF && useScopes) { + KEPLER_FORMAL::MiterStrategy MiterS(top0, top1); + MiterS.init(); + ScopeExtraction extractor(top0, top1); + extractor.collectVerificationScopes(); + if (cleanScopes) { + extractor.cleanVerificationScopes(MiterS.getPIs0(), MiterS.getPIs1()); + } + for (auto scopes : extractor.getScopesToVerify()) { + SPDLOG_INFO("Looking at scope: {} ", + scopes.first->getName().getString()); + // std::string scopeLogFile = (logFileName.empty() ? "kf_" : logFileName) + "_" + + // scopes.first->getName().getString() + ".txt"; + try { + KEPLER_FORMAL::MiterStrategy MiterScope(scopes.first, scopes.second, logFileName); + MiterScope.init(); + if (MiterScope.run()) { + SPDLOG_INFO("No difference was found for scope: {} , {}", + scopes.first->getName().getString(), + scopes.second->getName().getString()); + } else { + SPDLOG_INFO("Difference was found for scope: {} , {}. Please refer to the log(miter_log_x.txt) for details.", + scopes.first->getName().getString(), + scopes.second->getName().getString()); + } + } catch (const std::exception& e) { + // LCOV_EXCL_START + SPDLOG_ERROR("Workflow failed for scope: {} , {}: {}", + scopes.first->getName().getString(), + scopes.second->getName().getString(), + e.what()); + return EXIT_FAILURE; + // LCOV_EXCL_STOP + } + } + } else { + try { + KEPLER_FORMAL::MiterStrategy MiterS(top0, top1, logFileName); + MiterS.init(); + if (MiterS.run()) { + SPDLOG_INFO("No difference was found."); + } else { + SPDLOG_INFO("Difference was found. Please refer to the log(miter_log_x.txt) for details."); + } + } catch (const std::exception& e) { + // LCOV_EXCL_START + SPDLOG_ERROR("Workflow failed: {}", e.what()); + return EXIT_FAILURE; + // LCOV_EXCL_STOP } - } catch (const std::exception& e) { - // LCOV_EXCL_START - SPDLOG_ERROR("Workflow failed: {}", e.what()); - return EXIT_FAILURE; - // LCOV_EXCL_STOP } return EXIT_SUCCESS; diff --git a/src/formal/BoolExpr.cpp b/src/formal/BoolExpr.cpp index f78c7b2d..eccff31c 100644 --- a/src/formal/BoolExpr.cpp +++ b/src/formal/BoolExpr.cpp @@ -280,6 +280,30 @@ BoolExpr* BoolExpr::simplify(BoolExpr* e) { return memo.count(e) ? memo[e] : e; } +std::set BoolExpr::getSupportVars() const { + std::set support; + std::unordered_map visited; + std::vector stack; + stack.push_back(this); + + while (!stack.empty()) { + const BoolExpr* node = stack.back(); + stack.pop_back(); + + if (visited[node]) continue; + visited[node] = true; + + if (node->getOp() == Op::VAR) { + support.insert(node->getId()); + } else { + if (node->getLeft()) stack.push_back(node->getLeft()); + if (node->getRight()) stack.push_back(node->getRight()); + } + } + + return support; +} + } // namespace KEPLER_FORMAL diff --git a/src/formal/BoolExpr.h b/src/formal/BoolExpr.h index 400c12ea..44c33655 100644 --- a/src/formal/BoolExpr.h +++ b/src/formal/BoolExpr.h @@ -12,6 +12,7 @@ #include #include #include "BoolExprCache.h" +#include //#include "tbb/concurrent_unordered_map.h" namespace KEPLER_FORMAL { @@ -85,6 +86,8 @@ class BoolExpr : public std::enable_shared_from_this { // Memoized, safe on DAGs. static BoolExpr* simplify(BoolExpr* e); + std::set getSupportVars() const; + private: // Private ctor: use factory methods BoolExpr(Op op, diff --git a/src/scope/CMakeLists.txt b/src/scope/CMakeLists.txt new file mode 100644 index 00000000..4ab630fb --- /dev/null +++ b/src/scope/CMakeLists.txt @@ -0,0 +1,17 @@ +# Copyright 2024-2025 keplertech.io +# SPDX-License-Identifier: GPL-3.0-only + +cmake_minimum_required(VERSION 3.10) +project(scope_extraction_lib) + +set(CMAKE_CXX_STANDARD 20) +set(CMAKE_CXX_STANDARD_REQUIRED ON) + +# Create a static library target +add_library(scope_extraction STATIC + ScopeExtraction.cpp +) + +# Make headers accessible to other targets +target_include_directories(scope_extraction PUBLIC ${CMAKE_CURRENT_SOURCE_DIR}) +target_link_libraries(scope_extraction PUBLIC naja_nl naja_dnl naja_opt kepler_formal_utils) diff --git a/src/scope/ScopeExtraction.cpp b/src/scope/ScopeExtraction.cpp new file mode 100644 index 00000000..8d506623 --- /dev/null +++ b/src/scope/ScopeExtraction.cpp @@ -0,0 +1,281 @@ +#include "ScopeExtraction.h" +#include +#include +#include "DNL.h" +#include "NLUniverse.h" +#include "RemoveLoadlessLogic.h" +#include "SNLDesign.h" +#include "SNLLogicCone.h" +#include + +// #define DEBUG_PRINTS + +#ifdef DEBUG_PRINTS +#define DEBUG_LOG(fmt, ...) printf(fmt, ##__VA_ARGS__) +#else +#define DEBUG_LOG(fmt, ...) +#endif + +using namespace naja::NL; +using namespace naja::DNL; + +void ScopeExtraction::collectVerificationScopes() { + // Find leaf models(model that contain leaf only) + // DFS + std::stack> stack; + std::pair toCompare; + toCompare.first = top0_; + toCompare.second = top1_; + stack.push(toCompare); + while (!stack.empty()) { + std::pair toCompareNew = + stack.top(); + stack.pop(); + auto design0 = toCompareNew.first; + auto design1 = toCompareNew.second; + bool modelsAreEqual = true; + // First check, same number of instances + if (design0->getInstances().size() == design1->getInstances().size()) { + // We have same number of instances moving on to next checks + // 1. Check same child instances + DEBUG_LOG(" - Comparing models %s and %s\n", + design0->getName().getString().c_str(), + design1->getName().getString().c_str()); + std::vector childInstances0; + for (auto instance : design0->getInstances()) { + childInstances0.push_back(instance->getID()); + } + std::vector childInstances1; + for (auto instance : design1->getInstances()) { + childInstances1.push_back(instance->getID()); + } + if (childInstances0 != childInstances1) { + DEBUG_LOG(" - Child instances are different.\n"); + modelsAreEqual = false; + } + if (modelsAreEqual) { + DEBUG_LOG(" - Child instances are the same -> Comparing nets.\n"); + // Same child instances, now we will check all nets + std::vector nets0; + for (auto net : design0->getBitNets()) { + nets0.push_back(net); + } + std::vector nets1; + for (auto net : design1->getBitNets()) { + nets1.push_back(net); + } + if (nets0.size() != nets1.size()) { + DEBUG_LOG(" - Different number of nets.\n"); + modelsAreEqual = false; + } + if (modelsAreEqual) { + for (size_t i = 0; i < nets0.size(); ++i) { + DEBUG_LOG(" - Comparing net %s and %s\n", + nets0[i]->getName().getString().c_str(), + nets1[i]->getName().getString().c_str()); + DEBUG_LOG("Comparing bit terms.\n"); + auto net0 = nets0[i]; + auto net1 = nets1[i]; + // Check drivers + std::vector bitTerms0; + for (auto bitterm : net0->getBitTerms()) { + bitTerms0.push_back(bitterm); + } + std::vector bitTerms1; + for (auto bitterm : net1->getBitTerms()) { + bitTerms1.push_back(bitterm); + } + if (bitTerms0.size() != bitTerms1.size()) { + modelsAreEqual = false; + break; + } + for (size_t j = 0; j < bitTerms0.size(); ++j) { + auto term0 = bitTerms0[j]; + auto term1 = bitTerms1[j]; + if (term0->getID() != term1->getID()) { + modelsAreEqual = false; + break; + } + } + if (modelsAreEqual) { + DEBUG_LOG("Comparing inst terms.\n"); + // bit terms are same, now check ins terms + std::vector instTerms0; + for (auto instterm : net0->getInstTerms()) { + instTerms0.push_back(instterm); + } + std::vector instTerms1; + for (auto instterm : net1->getInstTerms()) { + instTerms1.push_back(instterm); + } + if (instTerms0.size() != instTerms1.size()) { + modelsAreEqual = false; + break; + } + for (size_t j = 0; j < instTerms0.size(); ++j) { + auto term0 = instTerms0[j]; + auto term1 = instTerms1[j]; + if (term0->getInstance()->getID() != + term1->getInstance()->getID() || + term0->getBitTerm()->getID() != + term1->getBitTerm()->getID()) { + modelsAreEqual = false; + break; + } + } + } + } + } + } + } else { + DEBUG_LOG(" - Different number of instances.\n"); + modelsAreEqual = false; + } + if (!modelsAreEqual) { + designsToVerify_.insert(toCompareNew); + } else { + // Add checks for children instances in next interation + std::vector instancesVector0; + for (auto instance : design0->getInstances()) { + if (instance->isPrimitive()) { + continue; + } + instancesVector0.push_back(instance); + } + std::vector instancesVector1; + for (auto instance : design1->getInstances()) { + if (instance->isPrimitive()) { + continue; + } + instancesVector1.push_back(instance); + } + for (size_t i = 0; i < instancesVector1.size(); ++i) { + std::pair pair; + pair.first = instancesVector0[i]->getModel(); + pair.second = instancesVector1[i]->getModel(); + stack.push(pair); + } + } + } +} + +void ScopeExtraction::cleanVerificationScopes( + const std::vector& pis0, + const std::vector& pis1) { + std::vector tops; + tops.push_back(top0_); + tops.push_back(top1_); + std::vector> pis; + pis.push_back(pis0); + pis.push_back(pis1); + for (size_t i = 0; i < tops.size(); ++i) { + naja::DNL::destroy(); + // Setting top to top0 + auto top = tops[i]; + naja::NL::NLUniverse::get()->setTopDesign(top); + // Collecting all scopes to verify under top0 + std::set scopes; + for (const auto& scope : designsToVerify_) { + naja::NL::SNLDesign* design = i == 0 ? scope.first : scope.second; + scopes.insert(design); + } + // Collecting all leaves who are under model is in scopes + std::set scopeLeaves; + auto dnl = naja::DNL::get(); + tbb::concurrent_unordered_set isosToKeep; + for (const auto& leaf : dnl->getLeaves()) { + const naja::NL::SNLDesign* model = + dnl->getDNLInstanceFromID(leaf).getSNLModel(); + naja::DNL::DNLInstanceFull currentInstance = + dnl->getDNLInstanceFromID(leaf); + while (currentInstance.isTop() == false) { + if (scopes.find(model) != scopes.end()) { + break; + } + currentInstance = currentInstance.getParentInstance(); + model = currentInstance.getSNLModel(); + // keep all isos on terminals of model + } + if (scopes.find(model) != scopes.end()) { + scopeLeaves.insert(leaf); + for (DNLID termId = currentInstance.getTermIndexes().first; + termId != DNLID_MAX && termId <= currentInstance.getTermIndexes().second; + termId++) { + const DNLTerminalFull& term = dnl->getDNLTerminalFromID(termId); + DNLID isoID = term.getIsoID(); + if (isoID != DNLID_MAX) { + isosToKeep.insert(isoID); + } + } + } + } + std::set readers; + for (const auto& leaf : dnl->getLeaves()) { + // For each terminal collect the readers of it's iso + DNLInstanceFull instance = dnl->getDNLInstanceFromID(leaf); + for (DNLID termId = instance.getTermIndexes().first; + termId != DNLID_MAX && termId <= instance.getTermIndexes().second; + termId++) { + const DNLTerminalFull& term = dnl->getDNLTerminalFromID(termId); + DNLID isoID = term.getIsoID(); + if (isoID != DNLID_MAX) { + auto iso = dnl->getDNLIsoDB().getIsoFromIsoIDconst(isoID); + for (const auto& reader : iso.getReaders()) { + DNLInstanceFull readerInstance = + dnl->getDNLTerminalFromID(reader).getDNLInstance(); + DNLID readerLeafID = readerInstance.getID(); + if (scopeLeaves.find(readerLeafID) != scopeLeaves.end()) { + readers.insert(reader); + } + } + } + } + } + // After this loop the dnl variable contain deleted DNL as cone destroy it in constructor for safety + size_t readerCount = 0; + std::vector readersVector; + readersVector.assign(readers.begin(), readers.end()); + KEPLER_FORMAL::SNLLogicCone cone(readersVector, pis[i]); + cone.run(); + for (const auto& isoID : cone.getConeIsoIDs()) { + isosToKeep.insert(isoID); + } + // if (getenv("KEPLER_NO_MT") || true) { + // for (const auto& reader : readersVector) { + // printf("Processing reader %zu / %zu\r", readerCount + 1, + // readersVector.size()); + // readerCount++; + // KEPLER_FORMAL::SNLLogicCone cone(reader, pis[i]); + // cone.initConeIsos(isosToKeep); + // cone.run(); + // printf("inserting isos %zu\n", cone.getConeIsoIDs().size()); + // // for (const auto& isoID : cone.getConeIsoIDs()) { + // // isosToKeep.insert(isoID); + // // } + // printf("inserted\n"); + // } + // } else { + // tbb::enumerable_thread_specific> localIsosToKeep; + // tbb::parallel_for(tbb::blocked_range(0, readersVector.size()), + // [&](const tbb::blocked_range& r) { + // for (DNLID j = r.begin(); j < r.end(); ++j) { + // KEPLER_FORMAL::SNLLogicCone cone(readersVector[j], pis[i]); + // //cone.initConeIsos(isosToKeep); + // cone.run(); + // auto& localIsosToKeepSet = localIsosToKeep.local(); + // localIsosToKeepSet.insert( + // cone.getConeIsoIDs().begin(), + // cone.getConeIsoIDs().end()); + // } + // }); + // for (const auto& localSet : localIsosToKeep) { + // for (const auto& isoID : localSet) { + // isosToKeep.insert(isoID); + // } + // } + // } + naja::NAJA_OPT::LoadlessLogicRemover remover; + auto loadlessInstances = remover.getLoadlessInstances(*naja::DNL::get(), isosToKeep); + remover.removeLoadlessInstances(top, loadlessInstances); + } +} diff --git a/src/scope/ScopeExtraction.h b/src/scope/ScopeExtraction.h new file mode 100644 index 00000000..fb7c2a70 --- /dev/null +++ b/src/scope/ScopeExtraction.h @@ -0,0 +1,46 @@ +// src/scope/ScopeExtraction.h +// SPDX-License-Identifier: GPL-3.0-only +// +// Small, test-friendly adjustment: +// - add a protected default constructor so test subclasses can default-construct +// - make internal members protected so test subclasses can set/inspect them +// The public API is preserved (existing constructor and getScopesToVerify()). + +#ifndef SCOPE_EXTRACTION_H +#define SCOPE_EXTRACTION_H + +#include "DNL.h" +#include +#include + +class ScopeExtraction { + public: + // Existing public constructor (preserve original API) + ScopeExtraction(naja::NL::SNLDesign* top0, naja::NL::SNLDesign* top1) + : top0_(top0), top1_(top1) {} + + virtual ~ScopeExtraction() = default; + + void collectVerificationScopes(); + + std::set> getScopesToVerify() const { + return designsToVerify_; + } + // Provide extracted verification scopes for debugging purposes by: + // 1 Collecting scopes via collectVerificationScopes() + // 2 Collecting logic cones for all differ elements in the scopes with SNLLogicCone + // 4 Deleting all elements not in the collected cones from the cloned tops + void cleanVerificationScopes(const std::vector& pis0, const std::vector& pis1); + + protected: + // Allow derived test helpers to default-construct and inspect internals. + // Protected so only subclasses (e.g., test helpers) can use it. + ScopeExtraction() = default; + + // Internal state made protected so test subclasses can set and inspect them. + naja::NL::SNLDesign* top0_ = nullptr; + naja::NL::SNLDesign* top1_ = nullptr; + std::set> designsToVerify_; +}; + +#endif // SCOPE_EXTRACTION_H diff --git a/src/strategies/miter/BuildPrimaryOutputClauses.cpp b/src/strategies/miter/BuildPrimaryOutputClauses.cpp index 867253a5..5f7e69ee 100644 --- a/src/strategies/miter/BuildPrimaryOutputClauses.cpp +++ b/src/strategies/miter/BuildPrimaryOutputClauses.cpp @@ -10,8 +10,8 @@ #include #include -// #define DEBUG_PRINTS -// #define DEBUG_CHECKS +//#define DEBUG_PRINTS +//#define DEBUG_CHECKS #ifdef DEBUG_PRINTS #define DEBUG_LOG(fmt, ...) printf(fmt, ##__VA_ARGS__) @@ -35,12 +35,26 @@ std::vector BuildPrimaryOutputClauses::collectInputs() { DEBUG_LOG("Collecting input %s\n", term.getSnlBitTerm()->getName().getString().c_str()); assert(termId < naja::DNL::get()->getDNLTerms().size()); - inputs.push_back(termId); + inputs.emplace_back(termId); } } for (DNLID leaf : dnl->getLeaves()) { + auto iter = modelCache_.find(dnl->getDNLInstanceFromID(leaf).getSNLModel()); const DNLInstanceFull& instance = dnl->getDNLInstanceFromID(leaf); + if ((iter != modelCache_.end()) && iter->second.analyzedPIs) { + const auto& cache = iter->second; + for (DNLID termId = instance.getTermIndexes().first; + termId != DNLID_MAX && termId <= instance.getTermIndexes().second; + termId++) { + const auto& term = dnl->getDNLTerminalFromID(termId); + if (cache.PIs.find(term.getSnlBitTerm()) != cache.PIs.end()) { + inputs.emplace_back(termId); + } + } + continue; + } + modelCache_[instance.getSNLModel()].analyzedPIs = true; size_t numberOfInputs = 0, numberOfOutputs = 0; for (DNLID termId = instance.getTermIndexes().first; termId != DNLID_MAX && termId <= instance.getTermIndexes().second; @@ -60,7 +74,9 @@ std::vector BuildPrimaryOutputClauses::collectInputs() { if (term.getSnlBitTerm()->getDirection() != SNLBitTerm::Direction::Input) { assert(termId < naja::DNL::get()->getDNLTerms().size()); - inputs.push_back(termId); + inputs.emplace_back(termId); + modelCache_[instance.getSNLModel()].PIs.insert( + term.getSnlBitTerm()); DEBUG_LOG( "Collecting input %s of model %s\n", term.getSnlBitTerm()->getName().getString().c_str(), @@ -81,12 +97,14 @@ std::vector BuildPrimaryOutputClauses::collectInputs() { if (!related.empty()) { isSequential = true; for (auto bitTerm : related) { - seqBitTerms.push_back(bitTerm); + seqBitTerms.emplace_back(bitTerm); } if (term.getSnlBitTerm()->getDirection() != SNLBitTerm::Direction::Input) { assert(termId < naja::DNL::get()->getDNLTerms().size()); - inputs.push_back(termId); + inputs.emplace_back(termId); + modelCache_[instance.getSNLModel()].PIs.insert( + term.getSnlBitTerm()); DEBUG_LOG( "Collecting seq input %s of model %s\n", term.getSnlBitTerm()->getName().getString().c_str(), @@ -107,7 +125,9 @@ std::vector BuildPrimaryOutputClauses::collectInputs() { term.getSnlBitTerm()->getOrderID()); if (!tt.isInitialized()) { assert(termId < naja::DNL::get()->getDNLTerms().size()); - inputs.push_back(termId); + inputs.emplace_back(termId); + modelCache_[instance.getSNLModel()].PIs.insert( + term.getSnlBitTerm()); DEBUG_LOG("Collecting input %s of model %s\n", term.getSnlBitTerm()->getName().getString().c_str(), term.getSnlBitTerm() @@ -120,7 +140,9 @@ std::vector BuildPrimaryOutputClauses::collectInputs() { if (tt.all0() || tt.all1()) { assert(termId < naja::DNL::get()->getDNLTerms().size()); - inputs.push_back(termId); + inputs.emplace_back(termId); + modelCache_[instance.getSNLModel()].PIs.insert( + term.getSnlBitTerm()); DEBUG_LOG("Collecting constant input %s of model %s\n", term.getSnlBitTerm()->getName().getString().c_str(), term.getSnlBitTerm() @@ -142,7 +164,9 @@ std::vector BuildPrimaryOutputClauses::collectInputs() { if (std::find(seqBitTerms.begin(), seqBitTerms.end(), term.getSnlBitTerm()) != seqBitTerms.end()) { assert(termId < naja::DNL::get()->getDNLTerms().size()); - inputs.push_back(termId); + inputs.emplace_back(termId); + modelCache_[instance.getSNLModel()].PIs.insert( + term.getSnlBitTerm()); DEBUG_LOG( "Collecting seq input %s of model %s\n", term.getSnlBitTerm()->getName().getString().c_str(), @@ -177,6 +201,20 @@ std::vector BuildPrimaryOutputClauses::collectOutputs() { } for (DNLID leaf : dnl->getLeaves()) { const DNLInstanceFull& instance = dnl->getDNLInstanceFromID(leaf); + auto iter = modelCache_.find(instance.getSNLModel()); + if ((iter != modelCache_.end()) && iter->second.analyzedPOs) { + const auto& cache = iter->second; + for (DNLID termId = instance.getTermIndexes().first; + termId != DNLID_MAX && termId <= instance.getTermIndexes().second; + termId++) { + const auto& term = dnl->getDNLTerminalFromID(termId); + if (cache.POs.find(term.getSnlBitTerm()) != cache.POs.end()) { + outputsSet.insert(termId); + } + } + continue; + } + modelCache_[instance.getSNLModel()].analyzedPOs = true; bool isSequential = false; std::vector seqBitTerms; @@ -189,11 +227,13 @@ std::vector BuildPrimaryOutputClauses::collectOutputs() { if (!related.empty()) { isSequential = true; for (auto bitTerm : related) { - seqBitTerms.push_back(bitTerm); + seqBitTerms.emplace_back(bitTerm); } if (term.getSnlBitTerm()->getDirection() != SNLBitTerm::Direction::Output) { outputsSet.insert(termId); + modelCache_[instance.getSNLModel()].POs.insert( + term.getSnlBitTerm()); DEBUG_LOG( "Collecting seq output %s of model %s\n", term.getSnlBitTerm()->getName().getString().c_str(), @@ -228,13 +268,13 @@ std::vector BuildPrimaryOutputClauses::collectOutputs() { const auto& tt = SNLDesignModeling::getTruthTable(tTerm.getSnlBitTerm()->getDesign(), tTerm.getSnlBitTerm()->getOrderID()); if (tt.isInitialized()) { - tts.push_back(tt); + tts.emplace_back(tt); // print deps for (const auto& d : tt.getDependencies()) { DEBUG_LOG("TT deps: %llu\n", d); } } else if (tt.all0() || tt.all1()) { - tts.push_back(tt); + tts.emplace_back(tt); } } bool inTermInTTDeps = false; @@ -306,6 +346,8 @@ std::vector BuildPrimaryOutputClauses::collectOutputs() { } if (/*deps.empty() &&*/ !inTermInTTDeps) { outputsSet.insert(termId); + modelCache_[instance.getSNLModel()].POs.insert( + term.getSnlBitTerm()); DEBUG_LOG("Collecting output %s of model %s\n", term.getSnlBitTerm()->getName().getString().c_str(), term.getSnlBitTerm() @@ -327,6 +369,8 @@ std::vector BuildPrimaryOutputClauses::collectOutputs() { if (std::find(seqBitTerms.begin(), seqBitTerms.end(), term.getSnlBitTerm()) != seqBitTerms.end()) outputsSet.insert(termId); + modelCache_[instance.getSNLModel()].POs.insert( + term.getSnlBitTerm()); DEBUG_LOG( "Collecting seq output %s of model %s\n", term.getSnlBitTerm()->getName().getString().c_str(), @@ -335,21 +379,29 @@ std::vector BuildPrimaryOutputClauses::collectOutputs() { } } outputs.clear(); - outputs.assign(outputsSet.begin(), outputsSet.end()); + // keep only terminals who are connected to nets + for (const auto& out : outputsSet) { + const DNLTerminalFull& term = dnl->getDNLTerminalFromID(out); + if (term.getIsoID() != DNLID_MAX) { + outputs.emplace_back(out); + } + } + //outputs.assign(outputsSet.begin(), outputsSet.end()); return outputs; } void BuildPrimaryOutputClauses::collect() { inputs_ = collectInputs(); - sortInputs(); + //sortInputs(); <- cannot sort inputs as it has to respect the inputs vector order for (const auto& input : inputs_) { std::vector path = naja::DNL::get()->getDNLTerminalFromID(input).getDNLInstance().getPath().getPathNames(); - auto pathIDs = naja::DNL::get()->getDNLTerminalFromID(input).getFullPathIDs(); + path.emplace_back(naja::DNL::get()->getDNLTerminalFromID(input).getSnlBitTerm()->getName()); using KeyT = std::pair, std::vector>; std::vector ids = { - (NLID::DesignObjectID)pathIDs[pathIDs.size()-2], - (NLID::DesignObjectID)pathIDs[pathIDs.size()-1] + (NLID::DesignObjectID) naja::DNL::get()->getDNLTerminalFromID(input).getSnlBitTerm()->getBit() + // (NLID::DesignObjectID)pathIDs[pathIDs.size()-2], + // (NLID::DesignObjectID)pathIDs[pathIDs.size()-1] }; KeyT key{ path, std::move(ids) }; @@ -357,15 +409,17 @@ void BuildPrimaryOutputClauses::collect() { input; } outputs_ = collectOutputs(); - sortOutputs(); + //sortOutputs(); <- cannot sort as it needs to keep the order for POs_ for (const auto& output : outputs_) { std::vector path = naja::DNL::get()->getDNLTerminalFromID(output).getDNLInstance().getPath().getPathNames(); - auto pathIDs = naja::DNL::get()->getDNLTerminalFromID(output).getFullPathIDs(); + path.emplace_back(naja::DNL::get()->getDNLTerminalFromID(output).getSnlBitTerm()->getName()); + //auto pathIDs = naja::DNL::get()->getDNLTerminalFromID(output).getFullPathIDs(); using KeyT = std::pair, std::vector>; std::vector ids = { - (NLID::DesignObjectID)pathIDs[pathIDs.size()-2], - (NLID::DesignObjectID)pathIDs[pathIDs.size()-1] + (NLID::DesignObjectID) naja::DNL::get()->getDNLTerminalFromID(output).getSnlBitTerm()->getBit() + //(NLID::DesignObjectID)pathIDs[pathIDs.size()-2], + // (NLID::DesignObjectID)pathIDs[pathIDs.size()-1] }; KeyT key{ path, std::move(ids) }; @@ -406,6 +460,7 @@ void BuildPrimaryOutputClauses::initVarNames() { } void BuildPrimaryOutputClauses::build() { + //printf("Building primary output clauses\n"); naja::DNL::get(); POs_.clear(); POs_ = tbb::concurrent_vector(outputs_.size()); @@ -421,15 +476,21 @@ void BuildPrimaryOutputClauses::build() { // init arena with automatic number of threads // unsigned hw = std::thread::hardware_concurrency(); // if (hw == 0) hw = 1; // fallback - tbb::global_control gc(tbb::global_control::max_allowed_parallelism, 20); tbb::task_arena arena(20); - arena.initialize(); IsPIs_ = std::vector(naja::DNL::get()->getNBterms(), false); for (auto pi : inputs_) { + if (pi >= IsPIs_.size()) { + std::string error = "PI " + std::to_string(pi) + " is out of range"; + throw std::runtime_error(error); + } IsPIs_[pi] = true; } IsPOs_ = std::vector(naja::DNL::get()->getNBterms(), false); for (auto po : outputs_) { + if (po >= IsPOs_.size()) { + std::string error = "PO " + std::to_string(po) + " is out of range"; + throw std::runtime_error(error); + } IsPOs_[po] = true; } auto processOutput = [&](size_t i) { @@ -475,7 +536,7 @@ void BuildPrimaryOutputClauses::build() { std::chrono::duration elapsed_seconds_comp = endComp - startComp; printf("Computation time for %lu: %f seconds\n", i, elapsed_seconds_comp.count()); #endif - // //cloud.getTruthTable().print(); + // //cloud.SNLDesignModeling::getTruthTable().print(); // std::vector test1; // std::vector test2; // for (auto in : cloud.getAllInputs()) { @@ -485,11 +546,11 @@ void BuildPrimaryOutputClauses::build() { // cloud.getInputs().size()); // // //assert(false && "Input in cloud is out of range"); // // } - // test1.push_back(in); + // test1.emplace_back(in); // } // for (auto in : cloud.getInputs()) { // printf("Input in cloud: %lu\n", in); - // test2.push_back(in); + // test2.emplace_back(in); // } // std::sort(test1.begin(), test1.end()); // std::sort(test2.begin(), test2.end()); @@ -501,22 +562,22 @@ void BuildPrimaryOutputClauses::build() { auto net = term.getSnlTerm()->getNet(); if (net != nullptr) { if (net->isConstant0()) { - varNames.push_back("0"); + varNames.emplace_back("0"); continue; } else if (net->isConstant1()) { - varNames.push_back("1"); + varNames.emplace_back("1"); continue; } } auto model = const_cast( term.getSnlBitTerm()->getDesign()); - auto tt = model->getTruthTable(term.getSnlBitTerm()->getOrderID()); + auto tt = model->SNLDesignModeling::getTruthTable(term.getSnlBitTerm()->getOrderID()); if (tt.isInitialized()) { if (tt.all0()) { - varNames.push_back("0"); + varNames.emplace_back("0"); continue; } else if (tt.all1()) { - varNames.push_back("1"); + varNames.emplace_back("1"); continue; } } @@ -531,20 +592,20 @@ void BuildPrimaryOutputClauses::build() { get()->getDNLTerminalFromID(input).getSnlBitTerm()->getDesign()->getName().getString().c_str()); assert(it != inputs_.end()); size_t index = std::distance(inputs_.begin(), it); - varNames.push_back(std::to_string(index + 2)); // +2 to avoid 0 and 1 + varNames.emplace_back(std::to_string(index + 2)); // +2 to avoid 0 and 1 which are reserved for constants }*/ #ifdef DEBUG_CHECKS - assert(cloud.getTruthTable().isInitialized()); + assert(cloud.SNLDesignModeling::getTruthTable().isInitialized()); #endif // DEBUG_LOG("Truth Table: %s\n", - // cloud.getTruthTable().print().c_str()); + // cloud.SNLDesignModeling::getTruthTable().print().c_str()); /*std::shared_ptr expr = Tree2BoolExpr::convert( - cloud.getTruthTable(), varNames);*/ + cloud.SNLDesignModeling::getTruthTable(), varNames);*/ // BoolExpr::getMutex().lock(); // if (POs_.size() - 1 < i) { // for (size_t j = POs_.size(); j <= i; ++j) { - // POs_.push_back(nullptr); + // POs_.emplace_back(nullptr); // } // } assert(POs_.size() - 1 >= i); @@ -598,43 +659,47 @@ void BuildPrimaryOutputClauses::build() { } void BuildPrimaryOutputClauses::setInputs2InputsIDs() { + //printf("Setting inputs to input IDs mapping\n"); inputs2inputsIDs_.clear(); for (const auto& input : inputs_) { if (get()->getDNLTerminalFromID(input).isNull()) { throw std::runtime_error("Input terminal is null"); } - DNLInstanceFull currentInstance = + const DNLInstanceFull& currentInstance = get()->getDNLTerminalFromID(input).getDNLInstance(); - std::vector termIDs; - termIDs.push_back( - get()->getDNLTerminalFromID(input).getSnlBitTerm()->getID()); - termIDs.push_back( - get()->getDNLTerminalFromID(input).getSnlBitTerm()->getBit()); - std::pair, std::vector> - pair; + //std::vector termIDs; + //termIDs.emplace_back( + // get()->getDNLTerminalFromID(input).getSnlBitTerm()->getID()); + //termIDs.emplace_back( + // get()->getDNLTerminalFromID(input).getSnlBitTerm()->getBit()); + std::pair, std::vector>& + pair = inputs2inputsIDs_[input]; pair.first = currentInstance.getPath().getPathNames(); - pair.second = termIDs; - inputs2inputsIDs_[input] = pair; + pair.first.emplace_back( + get()->getDNLTerminalFromID(input).getSnlBitTerm()->getName()); + pair.second.emplace_back( + get()->getDNLTerminalFromID(input).getSnlBitTerm()->getBit()); } } void BuildPrimaryOutputClauses::setOutputs2OutputsIDs() { + //printf("Setting outputs to output IDs mapping\n"); outputs2outputsIDs_.clear(); for (const auto& output : outputs_) { - std::pair, std::vector> path; - std::vector termIDs; - DNLInstanceFull currentInstance = + //std::vector termIDs; + const DNLInstanceFull& currentInstance = get()->getDNLTerminalFromID(output).getDNLInstance(); - termIDs.push_back( - get()->getDNLTerminalFromID(output).getSnlBitTerm()->getID()); - termIDs.push_back( - get()->getDNLTerminalFromID(output).getSnlBitTerm()->getBit()); - std::pair, std::vector> - pair; + //termIDs.emplace_back( + // get()->getDNLTerminalFromID(output).getSnlBitTerm()->getID()); + //termIDs + std::pair, std::vector>& + pair = outputs2outputsIDs_[output]; pair.first = currentInstance.getPath().getPathNames(); - pair.second = termIDs; - outputs2outputsIDs_[output] = pair; + pair.first.emplace_back( + get()->getDNLTerminalFromID(output).getSnlBitTerm()->getName()); + pair.second.emplace_back( + get()->getDNLTerminalFromID(output).getSnlBitTerm()->getBit()); } } @@ -642,7 +707,8 @@ void BuildPrimaryOutputClauses::sortInputs() { // Sort based on inputs2inputsIDs_ content std::sort(inputs_.begin(), inputs_.end(), [this](const DNLID& a, const DNLID& b) { - return inputs2inputsIDs_[a].first < inputs2inputsIDs_[b].first; + return inputs2inputsIDs_[a].first < inputs2inputsIDs_[b].first && + inputs2inputsIDs_[a].second < inputs2inputsIDs_[b].second; }); } @@ -650,6 +716,18 @@ void BuildPrimaryOutputClauses::sortOutputs() { // Sort based on outputs2outputsIDs_ content std::sort( outputs_.begin(), outputs_.end(), [this](const DNLID& a, const DNLID& b) { - return outputs2outputsIDs_[a].first < outputs2outputsIDs_[b].first; + return outputs2outputsIDs_[a].first < outputs2outputsIDs_[b].first && + outputs2outputsIDs_[a].second < outputs2outputsIDs_[b].second; }); -} \ No newline at end of file +} + +// const naja::NL::SNLTruthTable& BuildPrimaryOutputClauses::getTruthTable(naja::NL::SNLDesign* design, size_t orderID) { +// auto designID = design->getID(); +// auto iter = ttCache_.find({designID, orderID}); +// if (iter != ttCache_.end()) { +// return iter->second; +// } +// const auto& tt = SNLDesignModeling::getTruthTable(design, orderID); +// ttCache_[{designID, orderID}] = tt; +// return tt; +// } \ No newline at end of file diff --git a/src/strategies/miter/BuildPrimaryOutputClauses.h b/src/strategies/miter/BuildPrimaryOutputClauses.h index 1c034460..35cde7bb 100644 --- a/src/strategies/miter/BuildPrimaryOutputClauses.h +++ b/src/strategies/miter/BuildPrimaryOutputClauses.h @@ -6,6 +6,9 @@ #include "BoolExpr.h" #include "DNL.h" #include +#include "SNLTruthTable.h" +#include +#include #pragma once @@ -13,6 +16,20 @@ namespace KEPLER_FORMAL { class BuildPrimaryOutputClauses { public: + + struct KeyHash { + size_t operator()(const std::pair, std::vector>& k) const { + size_t res = 0; + for (const auto& name : k.first) { + res ^= std::hash()(name.getString()) + 0x9e3779b9 + (res << 6) + (res >> 2); + } + for (const auto& id : k.second) { + res ^= std::hash()(id) + 0x9e3779b9 + (res << 6) + (res >> 2); + } + return res; + } + }; + BuildPrimaryOutputClauses() = default; void collect(); void build(); @@ -22,37 +39,48 @@ class BuildPrimaryOutputClauses { } const std::vector& getInputs() const { return inputs_; } const std::vector& getOutputs() const { return outputs_; } - const std::map, std::vector>>& getInputs2InputsIDs() const { return inputs2inputsIDs_; } - const std::map, std::vector>>& getOutputs2OutputsIDs() const { return outputs2outputsIDs_; } void setInputs(const std::vector& inputs) { - inputs_ = inputs; /*sortInputs();*/ + inputs_ = std::move(inputs); /*sortInputs();*/ setInputs2InputsIDs(); } void setOutputs(const std::vector& outputs) { - outputs_ = outputs; /*sortOutputs();*/ + outputs_ = std::move(outputs); /*sortOutputs();*/ setOutputs2OutputsIDs(); } - const std::map, std::vector>, naja::DNL::DNLID>& + const std::unordered_map, std::vector>, naja::DNL::DNLID, KeyHash>& getInputsMap() const { return inputsMap_; } - const std::map, std::vector>, naja::DNL::DNLID>& + const std::unordered_map, std::vector>, naja::DNL::DNLID, KeyHash>& getOutputsMap() const { return outputsMap_; } naja::DNL::DNLID getDNLIDforOutput(size_t index) const { return outputs_[index]; } + naja::DNL::DNLID getDNLIDforInput(size_t index) const { + return inputs_[index]; + } + + const std::vector& getTermDNLID2VarID() const { + return termDNLID2varID_; + } + void setLastCommonID(size_t id) { lastCommonID = id; } private: + + //const naja::NL::SNLTruthTable& getTruthTable(naja::NL::SNLDesign* design, size_t orderID); + std::vector collectInputs(); void setInputs2InputsIDs(); void sortInputs(); @@ -60,21 +88,48 @@ class BuildPrimaryOutputClauses { void setOutputs2OutputsIDs(); void sortOutputs(); void initVarNames(); - + tbb::concurrent_vector POs_; std::vector inputs_; std::vector IsPIs_; std::vector outputs_; std::vector IsPOs_; - std::map, std::vector>, naja::DNL::DNLID> inputsMap_; - std::map, std::vector>, naja::DNL::DNLID> outputsMap_; - std::map, std::vector>, naja::DNL::DNLID, KeyHash> inputsMap_; + std::unordered_map, std::vector>, naja::DNL::DNLID, KeyHash> outputsMap_; + std::unordered_map, std::vector>> inputs2inputsIDs_; - std::map, std::vector>> outputs2outputsIDs_; std::vector termDNLID2varID_; // Only for PIs + size_t lastCommonID = 1; + + struct hash { + size_t operator()(const std::pair& p) const noexcept { + // A simple, solid 64-bit mix + uint64_t h = (uint64_t(p.first) << 32) ^ uint64_t(p.second); + h ^= (h >> 33); + h *= 0xff51afd7ed558ccdULL; + h ^= (h >> 33); + h *= 0xc4ceb9fe1a85ec53ULL; + h ^= (h >> 33); + return size_t(h); + } + }; + + std::unordered_map, naja::NL::SNLTruthTable, hash> ttCache_; + + struct CachedModel { + CachedModel() : analyzedPIs(false), analyzedPOs(false) {} + std::unordered_set PIs; + bool analyzedPIs = false; + std::unordered_set POs; + bool analyzedPOs = false; + }; + + std::unordered_map modelCache_; }; } // namespace KEPLER_FORMAL \ No newline at end of file diff --git a/src/strategies/miter/MiterStrategy.cpp b/src/strategies/miter/MiterStrategy.cpp index d9095604..c4865b30 100644 --- a/src/strategies/miter/MiterStrategy.cpp +++ b/src/strategies/miter/MiterStrategy.cpp @@ -28,6 +28,8 @@ #include // ensure console sink is available #include +//#define DEBUG_CHECKS + using namespace naja; using namespace naja::NL; using namespace KEPLER_FORMAL; @@ -288,12 +290,12 @@ Glucose::Lit tseitinEncode( logFileName_ = logFileName; } -void MiterStrategy::normalizeInputs( +size_t MiterStrategy::normalizeInputs( std::vector& inputs0, std::vector& inputs1, - const std::map, std::vector>, naja::DNL::DNLID>& + const std::unordered_map, std::vector>, naja::DNL::DNLID, KEPLER_FORMAL::BuildPrimaryOutputClauses::KeyHash>& inputs0Map, - const std::map, std::vector>, naja::DNL::DNLID>& + const std::unordered_map, std::vector>, naja::DNL::DNLID, KEPLER_FORMAL::BuildPrimaryOutputClauses::KeyHash>& inputs1Map) { ensureLoggerInitialized(); logger->info("normalizeInputs: starting"); @@ -320,8 +322,8 @@ void MiterStrategy::normalizeInputs( std::vector diff0; for (const auto& [path0, input0] : inputs0Map) { if (pathsCommon.find(path0) == pathsCommon.end()) { - diff0.push_back(input0); - auto pathInstance = path0; + diff0.emplace_back(input0); + const auto&pathInstance = path0; std::string pathString = ""; for (const auto& name : pathInstance.first) { pathString += name.getString() + "."; @@ -332,8 +334,8 @@ void MiterStrategy::normalizeInputs( std::vector diff1; for (const auto& [path1, input1] : inputs1Map) { if (pathsCommon.find(path1) == pathsCommon.end()) { - diff1.push_back(input1); - auto pathInstance = path1; + diff1.emplace_back(input1); + const auto&pathInstance = path1; std::string pathString = ""; for (const auto& name : pathInstance.first) { pathString += name.getString() + "."; @@ -343,7 +345,7 @@ void MiterStrategy::normalizeInputs( } inputs0.clear(); for (const auto& path : pathsCommon) { - inputs0.push_back(inputs0Map.at(path)); + inputs0.emplace_back(inputs0Map.at(path)); } inputs0.insert(inputs0.end(), diff0.begin(), diff0.end()); for (size_t i = 0; i < inputs0.size(); ++i) { @@ -351,7 +353,7 @@ void MiterStrategy::normalizeInputs( } inputs1.clear(); for (const auto& path : pathsCommon) { - inputs1.push_back(inputs1Map.at(path)); + inputs1.emplace_back(inputs1Map.at(path)); } inputs1.insert(inputs1.end(), diff1.begin(), diff1.end()); for (size_t i = 0; i < inputs1.size(); ++i) { @@ -360,17 +362,18 @@ void MiterStrategy::normalizeInputs( logger->info("size of common inputs: {}", pathsCommon.size()); logger->info("size of diff0 inputs: {}", diff0.size()); logger->info("size of diff1 inputs: {}", diff1.size()); + return pathsCommon.size(); } void MiterStrategy::normalizeOutputs( std::vector& outputs0, std::vector& outputs1, - const std::map, std::vector>, naja::DNL::DNLID>& + const std::unordered_map, std::vector>, naja::DNL::DNLID, KEPLER_FORMAL::BuildPrimaryOutputClauses::KeyHash>& outputs0Map, - const std::map, std::vector>, naja::DNL::DNLID>& + const std::unordered_map, std::vector>, naja::DNL::DNLID, KEPLER_FORMAL::BuildPrimaryOutputClauses::KeyHash>& outputs1Map) { ensureLoggerInitialized(); - logger->debug("normalizeOutputs: starting"); + logger->info("normalizeOutputs: starting"); // find the intersection of outputs0 and outputs1 based on the getFullPathIDs // of DNLTerminal and the diffs @@ -390,7 +393,7 @@ void MiterStrategy::normalizeOutputs( std::vector diff0; for (const auto& [path0, output0] : outputs0Map) { if (pathsCommon.find(path0) == pathsCommon.end()) { - diff0.push_back(output0); + diff0.emplace_back(output0); std::string fullName; for (const auto& name : path0.first) { fullName += name.getString() + "."; @@ -410,22 +413,23 @@ void MiterStrategy::normalizeOutputs( 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); + diff1.emplace_back(output1); } } outputs0.clear(); for (const auto& path : pathsCommon) { - outputs0.push_back(outputs0Map.at(path)); + outputs0.emplace_back(outputs0Map.at(path)); } //outputs0.insert(outputs0.end(), diff0.begin(), diff0.end()); outputs1.clear(); for (const auto& path : pathsCommon) { - outputs1.push_back(outputs1Map.at(path)); + outputs1.emplace_back(outputs1Map.at(path)); } //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()); + logger->info("size of common outputs: {}", pathsCommon.size()); + logger->info("size of diff0 outputs: {}", diff0.size()); + logger->info("size of diff1 outputs: {}", diff1.size()); + #ifdef DEBUG_CHECKS if (outputs0.size() == outputs1.size()) { if (outputs0 != outputs1) { // build the paths vector for outputs0 and outputs1 @@ -439,7 +443,7 @@ void MiterStrategy::normalizeOutputs( break; } } - paths0.push_back(path); + paths0.emplace_back(path); } for (const auto& output1 : outputs1) { std::pair, std::vector> path; @@ -449,7 +453,7 @@ void MiterStrategy::normalizeOutputs( break; } } - paths1.push_back(path); + paths1.emplace_back(path); } if (paths0 != paths1) { logger->error("Miter outputs must match in order"); @@ -466,68 +470,103 @@ void MiterStrategy::normalizeOutputs( } } } + #endif } -bool MiterStrategy::run() { +void MiterStrategy::init() { ensureLoggerInitialized(); logger->info("MiterStrategy::run starting"); - // build both sets of POs topInit_ = NLUniverse::get()->getTopDesign(); NLUniverse* univ = NLUniverse::get(); naja::DNL::destroy(); univ->setTopDesign(top0_); - BuildPrimaryOutputClauses builder0; - printf("Collecting POs for design 0: %s\n", top0_->getName().getString().c_str()); - builder0.collect(); - printf("Collected %lu POs for design 0\n", builder0.getOutputs().size()); + logger->info("Collecting POs for design 0: {}\n", top0_->getName().getString().c_str()); + builder0_.collect(); + logger->info("Collected {} POs for design 0\n", builder0_.getOutputs().size()); + PIs0_ = builder0_.getInputs(); naja::DNL::destroy(); univ->setTopDesign(top1_); - BuildPrimaryOutputClauses builder1; - printf("Collecting POs for design 1: %s\n", top1_->getName().getString().c_str()); - builder1.collect(); - printf("Collected %lu POs for design 1\n", builder1.getOutputs().size()); + logger->info("Collecting POs for design 1: {}\n", top1_->getName().getString().c_str()); + builder1_.collect(); + logger->info("Collected {} POs for design 1\n", builder1_.getOutputs().size()); + PIs1_ = builder1_.getInputs(); +} +bool MiterStrategy::run() { + NLUniverse* univ = NLUniverse::get(); // normalize inputs and outputs - auto inputs0sort = builder0.getInputs(); - auto inputs1sort = builder1.getInputs(); - auto outputs0sort = builder0.getOutputs(); - auto outputs1sort = builder1.getOutputs(); + std::vector inputs0sort; + std::vector inputs1sort; + std::vector outputs0sort; + std::vector outputs1sort; + size_t commonSize = normalizeInputs(inputs0sort, inputs1sort, builder0_.getInputsMap(), + builder1_.getInputsMap()); + builder0_.setLastCommonID(commonSize > 0 ? commonSize + 2 : 1); + builder1_.setLastCommonID(commonSize > 0 ? commonSize + 2 : 1); + lastCommonVarID_ = commonSize -1 > 0 ? (commonSize - 1) + 2/* 0, 1*/ : 1 /* 0, 1*/; + normalizeOutputs(outputs0sort, outputs1sort, builder0_.getOutputsMap(), + builder1_.getOutputsMap()); + logger->info("size of PIs in circuit 0: {}", inputs0sort.size()); logger->info("size of PIs in circuit 1: {}", inputs1sort.size()); logger->info("size of POs in circuit 0: {}", outputs0sort.size()); logger->info("size of POs in circuit 1: {}", outputs1sort.size()); - normalizeInputs(inputs0sort, inputs1sort, builder0.getInputsMap(), - builder1.getInputsMap()); - normalizeOutputs(outputs0sort, outputs1sort, builder0.getOutputsMap(), - builder1.getOutputsMap()); // return false; naja::DNL::destroy(); univ->setTopDesign(top0_); - builder0.setInputs(inputs0sort); - builder0.setOutputs(outputs0sort); + builder0_.setInputs(inputs0sort); + builder0_.setOutputs(outputs0sort); naja::DNL::destroy(); univ->setTopDesign(top1_); - builder1.setInputs(inputs1sort); - builder1.setOutputs(outputs1sort); + builder1_.setInputs(inputs1sort); + builder1_.setOutputs(outputs1sort); naja::DNL::destroy(); univ->setTopDesign(top0_); - builder0.build(); - const auto& PIs0 = builder0.getInputs(); - const auto& POs0 = builder0.getPOs(); - auto outputs0 = builder0.getOutputs(); - auto inputs2inputsIDs0 = builder0.getInputs2InputsIDs(); - auto outputs2outputsIDs0 = builder0.getOutputs2OutputsIDs(); + builder0_.build(); + const auto& PIs0 = builder0_.getInputs(); + const auto& POs0 = builder0_.getPOs(); + const auto& outputs0 = builder0_.getOutputs(); + const auto& inputs2inputsIDs0 = builder0_.getInputs2InputsIDs(); + const auto&outputs2outputsIDs0 = builder0_.getOutputs2OutputsIDs(); naja::DNL::destroy(); univ->setTopDesign(top1_); - builder1.build(); - const auto& PIs1 = builder1.getInputs(); - const auto& POs1 = builder1.getPOs(); - auto outputs1 = builder1.getOutputs(); - auto inputs2inputsIDs1 = builder1.getInputs2InputsIDs(); - auto outputs2outputsIDs1 = builder1.getOutputs2OutputsIDs(); - - std::vector outputs2DnlIds = builder1.getOutputs(); + builder1_.build(); + const auto& PIs1 = builder1_.getInputs(); + const auto& POs1 = builder1_.getPOs(); + const auto& outputs1 = builder1_.getOutputs(); + const auto& inputs2inputsIDs1 = builder1_.getInputs2InputsIDs(); + const auto& outputs2outputsIDs1 = builder1_.getOutputs2OutputsIDs(); + + // print path to var names + const auto & inputs2DnlIds = builder0_.getInputs(); + // var names for inputs + const auto & varNames = builder0_.getTermDNLID2VarID(); + for (size_t i = 0; i < inputs2DnlIds.size(); ++i) { + const auto&path = builder0_.getInputs2InputsIDs().at(builder0_.getDNLIDforInput(i)); + logger->info("VARID {} DNLID {}", varNames[inputs2DnlIds[i]], inputs2DnlIds[i]); + for (const auto& name : path.first) { + logger->info("{}.", name.getString().c_str()); + } + for (const auto& id : path.second) { + logger->info("bit: {}.", id); + } + logger->info("\n"); + } + // same for builder1 + const auto & inputs2DnlIds1 = builder1_.getInputs(); + const auto & varNames1 = builder1_.getTermDNLID2VarID(); + for (size_t i = 0; i < inputs2DnlIds1.size(); ++i) { + const auto& path = builder1_.getInputs2InputsIDs().at(builder1_.getDNLIDforInput(i)); + logger->info("VARID {} DNLID {}", varNames1[inputs2DnlIds1[i]], inputs2DnlIds1[i]); + for (const auto& name : path.first) { + logger->info("{}.", name.getString().c_str()); + } + for (const auto& id : path.second) { + logger->info("bit: {}.", id); + } + logger->info("\n"); + } if (topInit_ != nullptr) { univ->setTopDesign(topInit_); @@ -540,7 +579,9 @@ bool MiterStrategy::run() { } // build the Boolean-miter expression + logger->info("Building miter expression"); auto miter = buildMiter(POs0, POs1); + logger->info("Finished building miter expression"); // Now SAT check via Glucose Glucose::SimpSolver solver; @@ -563,25 +604,29 @@ bool MiterStrategy::run() { if (sat) { logger->warn("Miter found a difference -> moving to analyze individual POs"); for (size_t i = 0; i < POs0.size(); ++i) { - if (builder0.getOutputs2OutputsIDs().at(builder0.getDNLIDforOutput(i)) != - builder1.getOutputs2OutputsIDs().at(builder1.getDNLIDforOutput(i))) { + if (POs0[i] == POs1[i]) { // We can do this comparison because of the caching in, if they are the same, they are the same pointer + logger->info("PO index {} expressions are equal; skipping", i); + continue; + } + if (builder0_.getOutputs2OutputsIDs().at(builder0_.getDNLIDforOutput(i)) != + builder1_.getOutputs2OutputsIDs().at(builder1_.getDNLIDforOutput(i))) { // LCOV_EXCL_START - auto path0 = builder0.getOutputs2OutputsIDs().at(builder0.getDNLIDforOutput(i)); - auto path1 = builder1.getOutputs2OutputsIDs().at(builder1.getDNLIDforOutput(i)); + const auto&path0 = builder0_.getOutputs2OutputsIDs().at(builder0_.getDNLIDforOutput(i)); + const auto&path1 = builder1_.getOutputs2OutputsIDs().at(builder1_.getDNLIDforOutput(i)); // print path0 for (const auto& name : path0.first) { - logger->info("%s.", name.getString().c_str()); + logger->info("{}.", name.getString().c_str()); } for (const auto& id : path0.second) { - logger->info("%lu.", id); + logger->info("bit: {}.", id); } logger->info("\n"); // print path1 for (const auto& name : path1.first) { - logger->info("%s.", name.getString().c_str()); + logger->info("{}.", name.getString().c_str()); } for (const auto& id : path1.second) { - logger->info("%lu.", id); + logger->info("bit: {}.", id); } logger->info("\n"); throw std::runtime_error("Miter PO index " + std::to_string(i) + @@ -589,9 +634,9 @@ bool MiterStrategy::run() { // LCOV_EXCL_STOP } tbb::concurrent_vector singlePOs0S; - singlePOs0S.push_back(POs0[i]); + singlePOs0S.emplace_back(POs0[i]); tbb::concurrent_vector singlePOs1S; - singlePOs1S.push_back(POs1[i]); + singlePOs1S.emplace_back(POs1[i]); auto singleMiter = buildMiter(singlePOs0S, singlePOs1S); std::unordered_map singleNode2var; @@ -603,12 +648,31 @@ bool MiterStrategy::run() { singleSolver.addClause(singleRootLit); if (singleSolver.solve()) { - failedPOs_.push_back(i); + bool unSupportedVar = false; + const auto&varSupportA = POs0[i]->getSupportVars(); + for (const auto&var : varSupportA) { + if (lastCommonVarID_ < var) { + logger->warn("Unsupported var for PO0: {}", var); + unSupportedVar = true; + } + } + const auto&varSupportB = POs1[i]->getSupportVars(); + for (const auto&var : varSupportB) { + if (lastCommonVarID_ < var) { + logger->warn("Unsupported var for PO1: {}", var); + unSupportedVar = true; + } + } + if (unSupportedVar) { + logger->warn("buildMiter skipping output index {} due to unsupported variable", i); + continue; + } + failedPOs_.emplace_back(i); logger->info("Found difference for PO: {}", i); - // logger->info("Clause 0 {}", POs0[i]->toString()); - // logger->info("Clause 1 {}", POs1[i]->toString()); + //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)); + const auto&path0 = builder0_.getOutputs2OutputsIDs().at(builder0_.getDNLIDforOutput(i)); std::string pathString = ""; for (const auto& name : path0.first) { pathString += name.getString() + "."; @@ -616,8 +680,9 @@ bool MiterStrategy::run() { for (const auto& id : path0.second) { pathString += std::to_string(id) + "."; } + const auto&terminal0 = naja::DNL::get()->getDNLTerminalFromID(outputs0[i]); logger->info("Path of differing PO {}: {}", i, pathString); - auto path1 = builder1.getOutputs2OutputsIDs().at(builder1.getDNLIDforOutput(i)); + const auto&path1 = builder1_.getOutputs2OutputsIDs().at(builder1_.getDNLIDforOutput(i)); std::string pathString1 = ""; for (const auto& name : path1.first) { pathString1 += name.getString() + "."; @@ -627,15 +692,15 @@ bool MiterStrategy::run() { } logger->info("Path of differing PO {}: {}", i, pathString1); std::vector topModels; - topModels.push_back(top0_); - topModels.push_back(top1_); + topModels.emplace_back(top0_); + topModels.emplace_back(top1_); std::vector> PIs; - PIs.push_back(PIs0); - PIs.push_back(PIs1); + PIs.emplace_back(PIs0); + PIs.emplace_back(PIs1); naja::NL::SNLEquipotential::Terms terms0; naja::NL::SNLEquipotential::Terms terms1; - naja::NL::SNLEquipotential::InstTermOccurrences insTerms0; - naja::NL::SNLEquipotential::InstTermOccurrences insTerms1; + std::unordered_set insTerms0; + std::unordered_set insTerms1; for (size_t j = 0; j < topModels.size(); ++j) { DNL::destroy(); NLUniverse::get()->setTopDesign(topModels[j]); @@ -649,11 +714,11 @@ bool MiterStrategy::run() { // naja::DNL::get()->getDNLTerminalFromID(outputs1[i]).getSnlBitTerm()->getDesign()->getName().getString().c_str()); // } - if (dnls_.size() <= j) { - dnls_.push_back(*naja::DNL::get()); - } + // if (dnls_.size() <= j) { + // dnls_.emplace_back(*naja::DNL::get()); + // } SNLLogicCone cone(j == 0 ? outputs0[i] : outputs1[i], PIs[j], - &dnls_[j]); + naja::DNL::get()); cone.run(); // std::string dotFileNameEquis( // std::string(prefix_ + "_" + @@ -666,25 +731,53 @@ bool MiterStrategy::run() { // + std::to_string(outputs0[i]) + "_" + std::to_string(j) + // std::string(".svg"))); // SnlVisualiser snl2(topModels[j], cone.getEquipotentials()); - for (const auto& equi : cone.getEquipotentials()) { - for (const auto& term : equi.getTerms()) { + // for (const auto& equi : cone.getEquipotentials()) { + // for (const auto& term : equi.getTerms()) { + // if (j == 0) { + // terms0.insert(term); + // // logger->info("$$$ Term 0: {}", term->getString().c_str()); + // } else { + // terms1.insert(term); + // // logger->info("### Term 1: {}", term->getString().c_str()); + // } + // } + // for (const auto& termOcc : equi.getInstTermOccurrences()) { + // if (j == 0) { + // insTerms0.insert(termOcc); + // // logger->info("$$$ Inst Term 0: {}", + // // termOcc.getString().c_str()); + // } else { + // insTerms1.insert(termOcc); + // // logger->info("### Inst Term 1: {}", + // // termOcc.getString().c_str()); + // } + // } + // } + for (const auto& DNLID : cone.getCollectedTerms()) { + const naja::DNL::DNLTerminalFull& termFull = + naja::DNL::get()->getDNLTerminalFromID(DNLID); + if (termFull.isTopPort()) { if (j == 0) { - terms0.insert(term); - // logger->info("$$$ Term 0: {}", term->getString().c_str()); + terms0.insert(termFull.getSnlBitTerm()); } else { - terms1.insert(term); - // logger->info("### Term 1: {}", term->getString().c_str()); + terms1.insert(termFull.getSnlBitTerm()); } - } - for (const auto& termOcc : equi.getInstTermOccurrences()) { + } else { + std::string fullPath; + SNLDesign* design = NLUniverse::get()->getTopDesign(); + fullPath += design->getName().getString() + "."; + const auto& idPath = termFull.getFullPathIDs(); + for (size_t i = 0 ; i < idPath.size() - 2; ++i) { + fullPath += design->getInstance(idPath[i])->getName().getString() + "."; + design = design->getInstance(idPath[i])->getModel(); + } + fullPath += design->getTerm(idPath[idPath.size() - 2])->getName().getString() + "."; + fullPath += + std::to_string(termFull.getFullPathIDs().back()); if (j == 0) { - insTerms0.insert(termOcc); - // logger->info("$$$ Inst Term 0: {}", - // termOcc.getString().c_str()); + insTerms0.insert(fullPath); } else { - insTerms1.insert(termOcc); - // logger->info("### Inst Term 1: {}", - // termOcc.getString().c_str()); + insTerms1.insert(fullPath); } } } @@ -702,7 +795,7 @@ bool MiterStrategy::run() { for (const auto& term0 : terms0) { bool found = false; for (const auto& term1 : terms1) { - if (term0->getID() == term1->getID() && + if (term0->getName().getString() == term1->getName().getString() && term0->getBit() == term1->getBit()) { found = true; break; @@ -722,7 +815,7 @@ bool MiterStrategy::run() { for (const auto& term1 : terms1) { bool found = false; for (const auto& term0 : terms0) { - if (term0->getID() == term1->getID() && + if (term0->getName().getString() == term1->getName().getString() && term0->getBit() == term1->getBit()) { found = true; break; @@ -746,76 +839,38 @@ bool MiterStrategy::run() { // logger->info("Diff term: {}", term->getString()); // } // find intersection and diff of insTerms0 and insTerms1 - naja::NL::SNLEquipotential::InstTermOccurrences insTermsCommon; - naja::NL::SNLEquipotential::InstTermOccurrences insTermsDiff; + std::set insTermsCommon; + std::set insTermsDiff; for (const auto& term0 : insTerms0) { bool found = false; - for (const auto& term1 : insTerms1) { - if (term0.getPath().getPathNames() == term1.getPath().getPathNames() && - term0.getInstTerm()->getInstance()->getName() == - term1.getInstTerm()->getInstance()->getName() && - term0.getInstTerm()->getBitTerm()->getID() == - term1.getInstTerm()->getBitTerm()->getID() && - term0.getInstTerm()->getBitTerm()->getBit() == - term1.getInstTerm()->getBitTerm()->getBit()) { - found = true; - break; - } + if (insTerms1.find(term0) != insTerms1.end()) { + found = true; } if (found) { insTermsCommon.insert(term0); } else { insTermsDiff.insert(term0); - if (term0.getInstTerm()->getDirection() == - naja::NL::SNLInstTerm::Direction::Input || - !term0.getInstTerm() - ->getInstance() - ->getModel() - ->getInstances() - .empty()) { - continue; - } - logger->info("Diff 0 inst term {} with direction {}", - term0.getString(), - term0.getInstTerm()->getDirection().getString()); + logger->info("Diff 0 inst term {}", + term0); } } for (const auto& term1 : insTerms1) { bool found = false; - for (const auto& term0 : insTerms0) { - if (term0.getPath().getPathNames() == term1.getPath().getPathNames() && - term0.getInstTerm()->getInstance()->getName() == - term1.getInstTerm()->getInstance()->getName() && - term0.getInstTerm()->getBitTerm()->getID() == - term1.getInstTerm()->getBitTerm()->getID() && - term0.getInstTerm()->getBitTerm()->getBit() == - term1.getInstTerm()->getBitTerm()->getBit()) { - found = true; - break; - } + if (insTerms0.find(term1) != insTerms0.end()) { + found = true; } if (!found) { insTermsDiff.insert(term1); - if (term1.getInstTerm()->getDirection() == - naja::NL::SNLInstTerm::Direction::Input || - !term1.getInstTerm() - ->getInstance() - ->getModel() - ->getInstances() - .empty()) { - continue; - } - logger->info("Diff 1 inst term {} with direction {}", - term1.getString(), - term1.getInstTerm()->getDirection().getString()); + logger->info("Diff 1 inst term {}", + term1); } } - logger->debug("size of intersection of terms: {}", termsCommon.size()); - logger->debug("size of diff of terms: {}", termsDiff.size()); - logger->debug("size of intersection of inst terms: {}", + logger->info("size of intersection of terms: {}", termsCommon.size()); + logger->info("size of diff of terms: {}", termsDiff.size()); + logger->info("size of intersection of inst terms: {}", insTermsCommon.size()); - logger->debug("size of diff of inst terms: {}", insTermsDiff.size()); + logger->info("size of diff of inst terms: {}", insTermsDiff.size()); } } } @@ -841,15 +896,34 @@ BoolExpr* MiterStrategy::buildMiter( } // Start with the first XOR - auto miter = BoolExpr::Xor(A[0], B[0]); + auto miter = BoolExpr::createFalse(); // OR in the rest - for (size_t i = 1; i < A.size(); ++i) { + for (size_t i = 0; i < A.size(); ++i) { if (B.size() <= i) { logger->warn("Miter different number of outputs: {} vs {}", A.size(), B.size()); break; } + // bool unSupportedVar = false; + // const auto&varSupportA = A[i]->getSupportVars(); + // for (const auto&var : varSupportA) { + // if (lastCommonVarID_ < var) { + // logger->warn("Unsupported var: {}", var); + // unSupportedVar = true; + // } + // } + // const auto&varSupportB = B[i]->getSupportVars(); + // for (const auto&var : varSupportB) { + // if (lastCommonVarID_ < var) { + // logger->warn("Unsupported var: {}", var); + // unSupportedVar = true; + // } + // } + // if (unSupportedVar) { + // logger->warn("buildMiter skipping output index {} due to unsupported variable", i); + // continue; + // } auto diff = BoolExpr::Xor(A[i], B[i]); miter = BoolExpr::Or(miter, diff); } diff --git a/src/strategies/miter/MiterStrategy.h b/src/strategies/miter/MiterStrategy.h index c3083d9b..20ce3aeb 100644 --- a/src/strategies/miter/MiterStrategy.h +++ b/src/strategies/miter/MiterStrategy.h @@ -5,6 +5,7 @@ #include "BoolExpr.h" #include "DNL.h" #include +#include "BuildPrimaryOutputClauses.h" #pragma once @@ -20,31 +21,41 @@ class MiterStrategy { public: MiterStrategy(naja::NL::SNLDesign* top0, naja::NL::SNLDesign* top1, const std::string& logFileName = "", const std::string& prefix = ""); + void init(); + bool run(); - void normalizeInputs(std::vector& inputs0, + size_t normalizeInputs(std::vector& inputs0, std::vector& inputs1, - const std::map, std::vector>, naja::DNL::DNLID>& inputs0Map, - const std::map, std::vector>, naja::DNL::DNLID>& inputs1Map); + const std::unordered_map, std::vector>, naja::DNL::DNLID, KEPLER_FORMAL::BuildPrimaryOutputClauses::KeyHash>& inputs0Map, + const std::unordered_map, std::vector>, naja::DNL::DNLID, KEPLER_FORMAL::BuildPrimaryOutputClauses::KeyHash>& inputs1Map); void normalizeOutputs(std::vector& outputs0, std::vector& outputs1, - const std::map, std::vector>, naja::DNL::DNLID>& outputs0Map, - const std::map, std::vector>, naja::DNL::DNLID>& outputs1Map); + const std::unordered_map, std::vector>, naja::DNL::DNLID, KEPLER_FORMAL::BuildPrimaryOutputClauses::KeyHash>& outputs0Map, + const std::unordered_map, std::vector>, naja::DNL::DNLID, KEPLER_FORMAL::BuildPrimaryOutputClauses::KeyHash>& outputs1Map); static std::string logFileName_; + const std::vector& getPIs0() const { return PIs0_; } + const std::vector& getPIs1() const { return PIs1_; } private: BoolExpr* buildMiter( const tbb::concurrent_vector& A, const tbb::concurrent_vector& B) const; - + BuildPrimaryOutputClauses builder0_; + BuildPrimaryOutputClauses builder1_; static naja::NL::SNLDesign* top0_; static naja::NL::SNLDesign* top1_; + std::vector PIs0_; + std::vector PIs1_; + tbb::concurrent_vector POs0_; + tbb::concurrent_vector POs1_; std::vector failedPOs_; BoolExpr miterClause_; std::string prefix_; naja::NL::SNLDesign* topInit_ = nullptr; std::vector dnls_; + size_t lastCommonVarID_ = 1; }; } // namespace KEPLER_FORMAL \ No newline at end of file diff --git a/src/utils/SNLLogicCone.cpp b/src/utils/SNLLogicCone.cpp index 5c37f1cf..6447179c 100644 --- a/src/utils/SNLLogicCone.cpp +++ b/src/utils/SNLLogicCone.cpp @@ -10,35 +10,40 @@ using namespace naja::DNL; void SNLLogicCone::run() { std::vector currentIterationDrivers; std::vector newIterationIsos; - newIterationIsos.push_back( - dnl_->getDNLTerminalFromID(seedOutputTerm_).getIsoID()); + for (const auto& seedOutputTerm : seedOutputTerms_) { + newIterationIsos.push_back( + dnl_->getDNLTerminalFromID(seedOutputTerm).getIsoID()); + } while (!newIterationIsos.empty()) { currentIterationDrivers.clear(); for (const auto& isoID : newIterationIsos) { if (isoID != naja::DNL::DNLID_MAX) { - coneIsos_.push_back(isoID); + coneIsos_.insert(isoID); for (auto driver : dnl_->getDNLIsoDB().getIsoFromIsoIDconst(isoID).getDrivers()) { + collectedTerms_.insert(driver); currentIterationDrivers.push_back(driver); } } } newIterationIsos.clear(); for (auto driver : currentIterationDrivers) { - if (std::find(PIs_.begin(), PIs_.end(), driver) != PIs_.end()) { + if (isPIs_[driver]) { continue; // Skip PIs and loops(?) } - DNLInstanceFull inst = + collectedTerms_.insert(driver); + const DNLInstanceFull& inst = dnl_->getDNLTerminalFromID(driver).getDNLInstance(); for (DNLID termID = inst.getTermIndexes().first; termID <= inst.getTermIndexes().second && termID != DNLID_MAX; termID++) { const DNLTerminalFull& term = dnl_->getDNLTerminalFromID(termID); if (term.getSnlBitTerm()->getDirection() != - SNLBitTerm::Direction::Output) { - if (std::find(coneIsos_.begin(), coneIsos_.end(), term.getIsoID()) == + SNLBitTerm::Direction::Output && term.getIsoID() != naja::DNL::DNLID_MAX) { + if (coneIsos_.find(term.getIsoID()) == coneIsos_.end()) { newIterationIsos.push_back(term.getIsoID()); + collectedTerms_.insert(termID); } } } diff --git a/src/utils/SNLLogicCone.h b/src/utils/SNLLogicCone.h index b6d72850..7d86ce95 100644 --- a/src/utils/SNLLogicCone.h +++ b/src/utils/SNLLogicCone.h @@ -4,6 +4,7 @@ #pragma once #include "DNL.h" +#include namespace naja { namespace NL { @@ -16,25 +17,58 @@ namespace KEPLER_FORMAL { class SNLLogicCone { public: SNLLogicCone(naja::DNL::DNLID seedOutputTerm, - std::vector pis) - : seedOutputTerm_(seedOutputTerm), PIs_(pis) { - naja::DNL::destroy(); + std::vector pis) { + //naja::DNL::destroy(); + seedOutputTerms_.push_back(seedOutputTerm); dnl_ = naja::DNL::get(); + isPIs_.resize(dnl_->getDNLTerms().size(), false); + for (const auto& term : pis) { + isPIs_[term] = true; + } + } + SNLLogicCone(std::vector seedOutputTerms, + std::vector pis) { + //naja::DNL::destroy(); + for (const auto& term : seedOutputTerms) { + seedOutputTerms_.push_back(term); + } + dnl_ = naja::DNL::get(); + isPIs_.resize(dnl_->getDNLTerms().size(), false); + for (const auto& term : pis) { + isPIs_[term] = true; + } } SNLLogicCone(naja::DNL::DNLID seedOutputTerm, std::vector pis, - naja::DNL::DNLFull* dnl) - : seedOutputTerm_(seedOutputTerm), PIs_(pis) { - naja::DNL::destroy(); + naja::DNL::DNLFull* dnl) { + //naja::DNL::destroy(); + seedOutputTerms_.push_back(seedOutputTerm); dnl_ = dnl; + isPIs_.resize(dnl_->getDNLTerms().size(), false); + for (const auto& term : pis) { + isPIs_[term] = true; + } } void run(); std::vector getEquipotentials() const; + const tbb::concurrent_unordered_set& getConeIsoIDs() const { + return coneIsos_; + } + + void initConeIsos(const tbb::concurrent_unordered_set& isoIDs) { + coneIsos_ = isoIDs; + } + + const std::set& getCollectedTerms() const { + return collectedTerms_; + } + private: - naja::DNL::DNLID seedOutputTerm_; - std::vector coneIsos_; - std::vector PIs_; + std::vector seedOutputTerms_; + tbb::concurrent_unordered_set coneIsos_; + std::set collectedTerms_; + std::vector isPIs_; naja::DNL::DNLFull* dnl_; }; diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 8eeca07c..a66009e2 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -4,4 +4,5 @@ include(GoogleTest) add_subdirectory(strategies) -add_subdirectory(utils) \ No newline at end of file +add_subdirectory(utils) +add_subdirectory(scope) \ No newline at end of file diff --git a/test/scope/CMakeLists.txt b/test/scope/CMakeLists.txt new file mode 100644 index 00000000..e1db0554 --- /dev/null +++ b/test/scope/CMakeLists.txt @@ -0,0 +1,33 @@ +# Copyright 2024-2025 keplertech.io +# SPDX-License-Identifier: GPL-3.0-only + +include(GoogleTest) + +cmake_minimum_required(VERSION 3.10) +project(ScopeExtractionTests) + +# Enable testing +enable_testing() + +# Google Test setup +find_package(GTest REQUIRED) +include_directories(${GTEST_INCLUDE_DIRS}) + +# Add main and test files +add_executable(scopeExtractionTests ScopeExtractionTests.cpp) + +target_link_libraries(scopeExtractionTests + naja_nl + ${GTEST_LIBRARIES} + naja_opt + naja_snl_visual + kepler_clauses # 👈 place first + formal_strategies # 👈 after its dependencies + formal_structures + naja_dnl + pthread + naja_snl_pyloader + scope_extraction +) + +GTEST_DISCOVER_TESTS(scopeExtractionTests) \ No newline at end of file diff --git a/test/scope/ScopeExtractionTests.cpp b/test/scope/ScopeExtractionTests.cpp new file mode 100644 index 00000000..efa28b24 --- /dev/null +++ b/test/scope/ScopeExtractionTests.cpp @@ -0,0 +1,330 @@ +// Copyright 2024-2025 keplertech.io +// SPDX-License-Identifier: GPL-3.0-only +// +// Unit tests for ScopeExtraction::collectVerificationScopes() +// Adjusted to avoid duplicate SNLDesign/SNLInstance name collisions and +// double-destroy. Made tests deterministic by ensuring differences are explicit +// (net wiring or model reuse). + +#include +#include +#include +#include + +#include "ScopeExtraction.h" + +#include "BuildPrimaryOutputClauses.h" +#include "ConstantPropagation.h" +#include "DNL.h" +#include "MiterStrategy.h" +#include "NLLibraryTruthTables.h" +#include "NLUniverse.h" +#include "NetlistGraph.h" +#include "SNLCapnP.h" +#include "SNLDesign.h" +#include "SNLDesignModeling.h" +#include "SNLInstance.h" +#include "SNLPath.h" +#include "SNLScalarNet.h" +#include "SNLScalarTerm.h" + +using namespace naja; +using namespace naja::NL; +using namespace naja::NAJA_OPT; +using namespace KEPLER_FORMAL; + +// Helper to run shell commands (used by the original test for dot->svg). +static void executeCommand(const std::string& command) { + int result = system(command.c_str()); + if (result != 0) { + std::cerr << "Command execution failed: " << command << std::endl; + } +} + +// Test helper derived from ScopeExtraction to expose internals for assertions. +class TestScopeExtraction : public ScopeExtraction { + public: + TestScopeExtraction() : ScopeExtraction() {} + void setTop0(naja::NL::SNLDesign* d) { top0_ = d; } + void setTop1(naja::NL::SNLDesign* d) { top1_ = d; } + + const std::set>& + getDesignsToVerify() const { + return designsToVerify_; + } + + void runCollect() { collectVerificationScopes(); } +}; + +namespace { + +// Utility: create a minimal library + universe and return the created library. +// Caller is responsible for calling naja::DNL::destroy() and +// NLUniverse::get()->destroy() in test teardown if needed. +static NLLibrary* createUniverseAndLibrary(NLUniverse*& outUniv) { + outUniv = NLUniverse::create(); + NLDB* db = NLDB::create(outUniv); + NLLibrary* lib = + NLLibrary::create(db, NLLibrary::Type::Primitives, NLName("nangate45")); + return lib; +} + +// Build a simple top design with two child instances and two outputs. +// The function returns the top design pointer and also fills the instance +// pointers and term pointers so tests can wire nets differently to create +// mismatches. +// +// IMPORTANT: to avoid duplicate-name collisions in the shared NLLibrary, this +// function appends a unique suffix to created names. +struct TopDesignBundle { + SNLDesign* top = nullptr; + SNLScalarTerm* topOutA = nullptr; + SNLScalarTerm* topOutB = nullptr; + SNLDesign* childA_model = nullptr; + SNLDesign* childB_model = nullptr; + SNLInstance* childA_inst = nullptr; + SNLInstance* childB_inst = nullptr; + SNLScalarTerm* childA_out = nullptr; + SNLScalarTerm* childB_out = nullptr; +}; + +static TopDesignBundle buildSimpleTop(NLLibrary* lib, + const std::string& topBaseName, + const std::string& childANameBase, + const std::string& childBNameBase) { + static unsigned uniqueCounter = 0; + const unsigned id = ++uniqueCounter; + const std::string topName = topBaseName + "_" + std::to_string(id); + const std::string childAName = childANameBase + "_" + std::to_string(id); + const std::string childBName = childBNameBase + "_" + std::to_string(id); + + TopDesignBundle b; + // Create top + b.top = SNLDesign::create(lib, SNLDesign::Type::Primitive, NLName(topName)); + // two top outputs + b.topOutA = + SNLScalarTerm::create(b.top, SNLTerm::Direction::Output, NLName("outA")); + b.topOutB = + SNLScalarTerm::create(b.top, SNLTerm::Direction::Output, NLName("outB")); + + // child A: a primitive with one output + b.childA_model = + SNLDesign::create(lib, SNLDesign::Type::Primitive, NLName(childAName)); + b.childA_out = SNLScalarTerm::create( + b.childA_model, SNLTerm::Direction::Output, NLName("out")); + + // child B: another primitive with one output + b.childB_model = + SNLDesign::create(lib, SNLDesign::Type::Primitive, NLName(childBName)); + b.childB_out = SNLScalarTerm::create( + b.childB_model, SNLTerm::Direction::Output, NLName("out")); + + // instantiate both in top with unique instance names + const std::string instAName = std::string("instA_") + std::to_string(id); + const std::string instBName = std::string("instB_") + std::to_string(id); + b.childA_inst = SNLInstance::create(b.top, b.childA_model, NLName(instAName)); + b.childB_inst = SNLInstance::create(b.top, b.childB_model, NLName(instBName)); + + return b; +} + +} // namespace + +class ScopeExtractionUnitTests : public ::testing::Test { + protected: + void SetUp() override { + // create universe + library for each test + lib_ = createUniverseAndLibrary(univ_); + } + + void TearDown() override { + // Clean up global singletons used by the SNL framework + NLUniverse::get()->destroy(); + univ_ = nullptr; + lib_ = nullptr; + } + + NLUniverse* univ_ = nullptr; + NLLibrary* lib_ = nullptr; +}; + +// Test case: identical designs should not be added to designsToVerify_ at the +// top level, and the algorithm should recurse into children (which are also +// identical). +TEST_F(ScopeExtractionUnitTests, IdenticalDesigns_NoVerificationNeeded) { + // Build two top designs with identical structure (unique names internally) + TopDesignBundle a = buildSimpleTop(lib_, "topA", "LOGIC0", "LOGIC1"); + TopDesignBundle b = buildSimpleTop(lib_, "topB", "LOGIC0", "LOGIC1"); + + // Make the child models have deterministic truth tables so library tables + // exist + SNLDesignModeling::setTruthTable(a.childA_model, SNLTruthTable(0, 0)); + SNLDesignModeling::setTruthTable(a.childB_model, SNLTruthTable(0, 1)); + SNLDesignModeling::setTruthTable(b.childA_model, SNLTruthTable(0, 0)); + SNLDesignModeling::setTruthTable(b.childB_model, SNLTruthTable(0, 1)); + NLLibraryTruthTables::construct(lib_); + + // Wire nets identically for both tops + SNLNet* a_net0 = SNLScalarNet::create(a.top, NLName("net0")); + SNLNet* a_net1 = SNLScalarNet::create(a.top, NLName("net1")); + a.childA_inst->getInstTerm(a.childA_out)->setNet(a_net0); + a.childB_inst->getInstTerm(a.childB_out)->setNet(a_net1); + a.topOutA->setNet(a_net0); + a.topOutB->setNet(a_net1); + + SNLNet* b_net0 = SNLScalarNet::create(b.top, NLName("net0")); + SNLNet* b_net1 = SNLScalarNet::create(b.top, NLName("net1")); + b.childA_inst->getInstTerm(b.childA_out)->setNet(b_net0); + b.childB_inst->getInstTerm(b.childB_out)->setNet(b_net1); + b.topOutA->setNet(b_net0); + b.topOutB->setNet(b_net1); + + TestScopeExtraction se; + se.setTop0(a.top); + se.setTop1(b.top); + + se.runCollect(); + + const auto& toVerify = se.getDesignsToVerify(); + EXPECT_TRUE(toVerify.empty()); +} + +// Test case: different number of instances at top level -> top pair should be +// added +TEST_F(ScopeExtractionUnitTests, DifferentInstanceCount_TopAddedToVerify) { + // Build top A with two children + TopDesignBundle a = buildSimpleTop(lib_, "topA_diff", "LOGIC0", "LOGIC1"); + + // Build top B with only one child (simulate different instance count) + TopDesignBundle b; + static unsigned localCounter = 0; + ++localCounter; + const std::string topBName = + std::string("topB_diff_") + std::to_string(localCounter); + b.top = SNLDesign::create(lib_, SNLDesign::Type::Primitive, NLName(topBName)); + b.topOutA = + SNLScalarTerm::create(b.top, SNLTerm::Direction::Output, NLName("outA")); + // create only one child model and instance (unique name) + const std::string singleChildName = + std::string("LOGIC0_single_") + std::to_string(localCounter); + b.childA_model = SNLDesign::create(lib_, SNLDesign::Type::Primitive, + NLName(singleChildName)); + b.childA_out = SNLScalarTerm::create( + b.childA_model, SNLTerm::Direction::Output, NLName("out")); + const std::string instAName = + std::string("instA_single_") + std::to_string(localCounter); + b.childA_inst = SNLInstance::create(b.top, b.childA_model, NLName(instAName)); + + // Set truth tables and construct library tables + SNLDesignModeling::setTruthTable(a.childA_model, SNLTruthTable(0, 0)); + SNLDesignModeling::setTruthTable(a.childB_model, SNLTruthTable(0, 1)); + SNLDesignModeling::setTruthTable(b.childA_model, SNLTruthTable(0, 0)); + NLLibraryTruthTables::construct(lib_); + + // Wire nets for A + SNLNet* a_net0 = SNLScalarNet::create(a.top, NLName("net0")); + SNLNet* a_net1 = SNLScalarNet::create(a.top, NLName("net1")); + a.childA_inst->getInstTerm(a.childA_out)->setNet(a_net0); + a.childB_inst->getInstTerm(a.childB_out)->setNet(a_net1); + a.topOutA->setNet(a_net0); + a.topOutB->setNet(a_net1); + + // Wire nets for B (only one) + SNLNet* b_net0 = SNLScalarNet::create(b.top, NLName("net0")); + b.childA_inst->getInstTerm(b.childA_out)->setNet(b_net0); + b.topOutA->setNet(b_net0); + + TestScopeExtraction se; + se.setTop0(a.top); + se.setTop1(b.top); + + se.runCollect(); + + const auto& toVerify = se.getDesignsToVerify(); + EXPECT_FALSE(toVerify.empty()); + EXPECT_EQ(toVerify.size(), 1u); + auto pair = *toVerify.begin(); + EXPECT_EQ(pair.first, a.top); + EXPECT_EQ(pair.second, b.top); +} + +// Test case: same instance count but different child instance ordering/IDs -> +// added to verify Make the difference explicit by wiring nets differently in +// the second top as well. +TEST_F(ScopeExtractionUnitTests, SameCountDifferentChildIDs_AddedToVerify) { + // Build two tops with same number of instances but different child model IDs + TopDesignBundle a = buildSimpleTop(lib_, "topA_ids", "LOGIC_A", "LOGIC_B"); + TopDesignBundle b = buildSimpleTop(lib_, "topB_ids", "LOGIC_X", "LOGIC_Y"); + + // Set truth tables so nets/terms exist + SNLDesignModeling::setTruthTable(a.childA_model, SNLTruthTable(0, 0)); + SNLDesignModeling::setTruthTable(a.childB_model, SNLTruthTable(0, 1)); + SNLDesignModeling::setTruthTable(b.childA_model, SNLTruthTable(0, 0)); + SNLDesignModeling::setTruthTable(b.childB_model, SNLTruthTable(0, 1)); + NLLibraryTruthTables::construct(lib_); + + // Wire nets for A + SNLNet* a_net0 = SNLScalarNet::create(a.top, NLName("net0")); + SNLNet* a_net1 = SNLScalarNet::create(a.top, NLName("net1")); + a.childA_inst->getInstTerm(a.childA_out)->setNet(a_net0); + a.childB_inst->getInstTerm(a.childB_out)->setNet(a_net1); + a.topOutA->setNet(a_net0); + a.topOutB->setNet(a_net1); + + // Wire nets for B differently (explicit difference) + SNLNet* b_net0 = SNLScalarNet::create(b.top, NLName("net0")); + SNLNet* b_net1 = SNLScalarNet::create(b.top, NLName("net1")); + // swap wiring in B to ensure mismatch is detected + b.childA_inst->getInstTerm(b.childA_out)->setNet(b_net1); + b.childB_inst->getInstTerm(b.childB_out)->setNet(b_net0); + b.topOutA->setNet(b_net1); + b.topOutB->setNet(b_net0); + + TestScopeExtraction se; + se.setTop0(a.top); + se.setTop1(b.top); + + se.runCollect(); + + const auto& toVerify = se.getDesignsToVerify(); + EXPECT_FALSE(toVerify.empty()); + EXPECT_EQ(toVerify.size(), 1u); + auto pair = *toVerify.begin(); + EXPECT_EQ(pair.first, a.top); + EXPECT_EQ(pair.second, b.top); +} + +// Test case: same child instances but nets differ in bit terms / inst terms -> +// added to verify +TEST_F(ScopeExtractionUnitTests, SameChildrenDifferentNets_AddedToVerify) { + // Build two tops that will share the same child models (so child model + // pointers match) Build the first top without helper function + TopDesignBundle a; + const std::string aTopName = "topA_nets_reuse"; + a.top = SNLDesign::create(lib_, SNLDesign::Type::Primitive, NLName(aTopName)); + TopDesignBundle b; + const std::string bTopName = + std::string("topB_nets_reuse_") + std::to_string(1); + b.top = SNLDesign::create(lib_, SNLDesign::Type::Primitive, NLName(bTopName)); + // create one net on second top + SNLNet* b_net0 = SNLScalarNet::create(b.top, NLName("net0")); + + TestScopeExtraction se; + se.setTop0(a.top); + se.setTop1(b.top); + + se.runCollect(); + + const auto& toVerify = se.getDesignsToVerify(); + EXPECT_FALSE(toVerify.empty()); + EXPECT_EQ(toVerify.size(), 1u); + auto pair = *toVerify.begin(); + EXPECT_EQ(pair.first, a.top); + EXPECT_EQ(pair.second, b.top); +} + +// Required main function for Google Test +int main(int argc, char** argv) { + ::testing::InitGoogleTest(&argc, argv); + return RUN_ALL_TESTS(); +} diff --git a/test/strategies/miter/MiterTests.cpp b/test/strategies/miter/MiterTests.cpp index dc9def3a..8928d533 100644 --- a/test/strategies/miter/MiterTests.cpp +++ b/test/strategies/miter/MiterTests.cpp @@ -308,7 +308,8 @@ TEST_F(MiterTests, TestMiterANDNonConstantWithSequentialElements) { SNLScalarTerm::create(top, SNLTerm::Direction::Input, NLName("In1")); auto topIn2 = SNLScalarTerm::create(top, SNLTerm::Direction::Input, NLName("In2")); - NLLibraryTruthTables::construct(library); + + // 7. create a and model SNLDesign* andModel = SNLDesign::create(library, SNLDesign::Type::Primitive, NLName("AND")); @@ -470,7 +471,7 @@ TEST_F(MiterTests, TestMiterAndWithChainedInverter) { SNLScalarTerm::create(top, SNLTerm::Direction::Input, NLName("In3")); auto topIn4 = SNLScalarTerm::create(top, SNLTerm::Direction::Input, NLName("In4")); - NLLibraryTruthTables::construct(library); + //NLLibraryTruthTables::construct(library); // 7. create a and model SNLDesign* andModel = SNLDesign::create(library, SNLDesign::Type::Primitive, NLName("AND")); @@ -488,13 +489,16 @@ TEST_F(MiterTests, TestMiterAndWithChainedInverter) { // 8. create an inverter model SNLDesign* inverterModel = SNLDesign::create(library, SNLDesign::Type::Primitive, NLName("INV")); - // set truth table for inverter model - auto invIn = + + auto invIn = SNLScalarTerm::create(inverterModel, SNLTerm::Direction::Input, NLName("in")); auto invOut = SNLScalarTerm::create(inverterModel, SNLTerm::Direction::Output, NLName("out")); SNLDesignModeling::setTruthTable(inverterModel, SNLTruthTable(1, 1)); - + NLLibraryTruthTables::construct(library); + // set truth table for inverter model + + // create and instance in top SNLInstance* instAnd = SNLInstance::create(top, andModel, NLName("and")); @@ -579,6 +583,7 @@ TEST_F(MiterTests, TestMiterAndWithChainedInverter) { // test the miter strategy { MiterStrategy MiterS(top, topClone, "CaseC"); + MiterS.init(); EXPECT_FALSE(MiterS.run()); } { @@ -618,6 +623,7 @@ TEST_F(MiterTests, TestMiterAndWithChainedInverter) { // test the miter strategy again { MiterStrategy MiterS(top, topClone, "CaseD"); + MiterS.init(); EXPECT_TRUE(MiterS.run()); } { @@ -647,12 +653,6 @@ TEST_F(MiterTests, TestMiterAndWithChainedInverter) { } -// Required main function for Google Test -int main(int argc, char** argv) { - ::testing::InitGoogleTest(&argc, argv); - return RUN_ALL_TESTS(); -} - // ---------------------- Tests appended for coverage (subprocess approach, tolerant) ---------------------- // Append this block at the end of the file (after main). @@ -900,6 +900,14 @@ TEST_F(MiterTests, CoverDiff) { SNLScalarTerm::create(logic1, SNLTerm::Direction::Output, NLName("out")); SNLDesignModeling::setTruthTable(logic0, SNLTruthTable(0, 0)); SNLDesignModeling::setTruthTable(logic1, SNLTruthTable(0, 1)); + SNLDesign* inverterModel = + SNLDesign::create(library, SNLDesign::Type::Primitive, NLName("INV")); + // set truth table for inverter model + auto invIn = + SNLScalarTerm::create(inverterModel, SNLTerm::Direction::Input, NLName("in")); + auto invOut = + SNLScalarTerm::create(inverterModel, SNLTerm::Direction::Output, NLName("out")); + SNLDesignModeling::setTruthTable(inverterModel, SNLTruthTable(1, 1)); NLLibraryTruthTables::construct(library); // 5. create a logic_0 instace in top SNLInstance* inst1 = SNLInstance::create(top, logic0, NLName("logic0")); @@ -960,14 +968,8 @@ TEST_F(MiterTests, CoverDiff) { andC1->getInstTerm(andIn1->getID())->setNet(netC1a); andC1->getInstTerm(andIn2->getID())->setNet(netC1b); SNLInstance* constC1 = SNLInstance::create(topClone1, logic0, NLName("logic0C1")); - SNLDesign* inverterModel = - SNLDesign::create(library, SNLDesign::Type::Primitive, NLName("INV")); - // set truth table for inverter model - auto invIn = - SNLScalarTerm::create(inverterModel, SNLTerm::Direction::Input, NLName("in")); - auto invOut = - SNLScalarTerm::create(inverterModel, SNLTerm::Direction::Output, NLName("out")); - SNLDesignModeling::setTruthTable(inverterModel, SNLTruthTable(1, 1)); + + auto inverterC1 = SNLInstance::create(topClone1, inverterModel, NLName("inverterC1")); constC1->getInstTerm(logic0Out->getID())->setNet(netC1a); auto netC1invOut = SNLScalarNet::create(topClone1, NLName("netC1invOut")); @@ -980,6 +982,7 @@ TEST_F(MiterTests, CoverDiff) { get(); naja::DNL::destroy(); MiterStrategy MiterS(topClone0, topClone1, "CaseD"); + MiterS.init(); EXPECT_FALSE(MiterS.run()); } @@ -1014,7 +1017,7 @@ TEST_F(MiterTests, multiDriver) { SNLScalarTerm::create(logic1, SNLTerm::Direction::Output, NLName("out")); SNLDesignModeling::setTruthTable(logic0, SNLTruthTable(0, 0)); SNLDesignModeling::setTruthTable(logic1, SNLTruthTable(0, 1)); - NLLibraryTruthTables::construct(library); + //NLLibraryTruthTables::construct(library); // 5. create a logic_0 instace in top SNLInstance* inst1 = SNLInstance::create(top, logic0, NLName("logic0")); // 6. create a logic_1 instace in top @@ -1035,6 +1038,7 @@ TEST_F(MiterTests, multiDriver) { SNLInstance* inst4 = SNLInstance::create(top, andModel, NLName("and2")); // set truth table for and model SNLDesignModeling::setTruthTable(andModel, SNLTruthTable(2, 8)); + NLLibraryTruthTables::construct(library); // 9. connect all instances inputs SNLNet* net1 = SNLScalarNet::create(top, NLName("net1")); SNLNet* net2 = SNLScalarNet::create(top, NLName("net2")); @@ -1056,6 +1060,7 @@ TEST_F(MiterTests, multiDriver) { auto topClone = top->clone(NLName("topClone")); // 11. create DNL MiterStrategy MiterS(top, topClone, "MultiDriver"); + MiterS.init(); // Expect throw in run EXPECT_THROW(MiterS.run(), std::runtime_error); naja::DNL::destroy(); @@ -1094,6 +1099,7 @@ TEST_F(MiterTests, tt65In) { SNLScalarTerm::create(logic1, SNLTerm::Direction::Output, NLName("out")); SNLDesignModeling::setTruthTable(logic0, SNLTruthTable(0, 0)); SNLDesignModeling::setTruthTable(logic1, SNLTruthTable(0, 1)); + //NLLibraryTruthTables::construct(library); // Create a model with 65 inputs and 1 output and set the truth table so // output is 1 only when all inputs are 0 SNLDesign* tt65InModel = @@ -1122,6 +1128,7 @@ TEST_F(MiterTests, tt65In) { tt65InTables.push_back(SNLTruthTable(2, 8)); } SNLDesignModeling::setTruthTables(tt65InModel,tt65InTables); + //NLLibraryTruthTables::construct(library); // create the instance of the model in top auto tt65InInst = SNLInstance::create(top, tt65InModel, NLName("tt65in")); // 5. create a logic_0 instace in top @@ -1153,6 +1160,7 @@ TEST_F(MiterTests, tt65In) { SNLInstance* inst4 = SNLInstance::create(top, andModel, NLName("and2")); // set truth table for and model SNLDesignModeling::setTruthTable(andModel, SNLTruthTable(2, 8)); + //NLLibraryTruthTables::construct(library); // 9. connect all instances inputs SNLNet* net1 = SNLScalarNet::create(top, NLName("net1")); SNLNet* net2 = SNLScalarNet::create(top, NLName("net2")); @@ -1181,6 +1189,7 @@ TEST_F(MiterTests, tt65In) { auto topClone = top->clone(NLName("topClone")); // 11. create DNL MiterStrategy MiterS(top, topClone, "MultiDriver"); + MiterS.init(); // Expect throw in run EXPECT_THROW(MiterS.run(), std::runtime_error); naja::DNL::destroy(); @@ -1198,4 +1207,19 @@ TEST(KeplerCliSubprocessTests, ExampleTestRun) { EXPECT_EQ(rc, EXIT_SUCCESS); } +TEST(KeplerCliSubprocessTests, ExampleTestRunNajaIFWithScopeExtraction) { + std::filesystem::path p(KEPLER_BIN); + if (!std::filesystem::exists(p)) GTEST_SKIP() << "kepler-formal binary missing"; + + int rc = run_kepler_cli_with_args({"--config", "../../../../test/strategies/miter/test_config_naja_if_with_se.yaml"}); + EXPECT_EQ(rc, EXIT_SUCCESS); +} + + +// Required main function for Google Test +int main(int argc, char** argv) { + ::testing::InitGoogleTest(&argc, argv); + return RUN_ALL_TESTS(); +} + // End of appended tests diff --git a/test/strategies/miter/test_config_naja_if_with_se.yaml b/test/strategies/miter/test_config_naja_if_with_se.yaml new file mode 100644 index 00000000..4c00db9d --- /dev/null +++ b/test/strategies/miter/test_config_naja_if_with_se.yaml @@ -0,0 +1,15 @@ +# Copyright 2024-2025 keplertech.io +# SPDX-License-Identifier: GPL-3.0-only +# tinyrocket_config.yaml +format: naja_if +input_paths: + - ../../../../example/tinyrocket_naja.if + - ../../../../example/tinyrocket_naja_edited.if +liberty_files: + - ../../../../example/NangateOpenCellLibrary_typical.lib + - ../../../../example/fakeram45_1024x32.lib + - ../../../../example/fakeram45_64x32.lib +log_level: info +use_scopes: true +clean_scopes: true +