From 5a105ee997c59de552014ce9e61c8375416a1305 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C3=98yvind=20Harboe?= Date: Wed, 7 Oct 2026 14:46:24 +0200 Subject: [PATCH] Experimental --skip-gated-clock-flops: check a clock-gated netlist, minus its gated flops MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A flop clocked through an integrated clock gate cannot be compared: the gate's latch is opaque, so the write enable that moved onto the clock is invisible to the combinational check, and every gated flop differs. With --skip-gated-clock-flops (skip_gated_clock_flops in a config), the inputs of a sequential instance whose clock pin is driven by a cell output with no truth table but a combinational dependency (an ICG's GCLK as a liberty statetable gives it) are left out with the new reason GatedClock, decided per output before isos share a representative. A warning gives the count; --report-skipped-pos lists them in skipped_gated_clock_pos.txt. Everything else is compared. Experimental and off by default: a strong signal for automated loops, not a production clock-gating check. Co-Authored-By: Claude Opus 5.5 Signed-off-by: Øyvind Harboe --- src/bin/KeplerFormal.cpp | 22 ++- src/config/Config.h | 13 ++ .../miter/BuildPrimaryOutputClauses.cpp | 90 +++++++++++ .../miter/BuildPrimaryOutputClauses.h | 1 + test/strategies/miter/MiterTests.cpp | 140 ++++++++++++++++++ 5 files changed, 264 insertions(+), 2 deletions(-) diff --git a/src/bin/KeplerFormal.cpp b/src/bin/KeplerFormal.cpp index 8e2c1038..d1c10293 100644 --- a/src/bin/KeplerFormal.cpp +++ b/src/bin/KeplerFormal.cpp @@ -76,13 +76,13 @@ static void print_usage(const char* prog) { " [--verilog_design1_top ] [--verilog_design2_top ] [--vhdl_design1_top ] [--vhdl_design2_top ] [--python_design1_top ] [--python_design2_top ] [--liberty ...] [-v ] [-k ] [--sec-engine ] [--sec-encoding ] [--learn-internal-relations ] [--allow-x-equality-in-internal-relations ] [--sec-reset-cycles ] [--sec-reset-port ...] " "[--allow-boundary-mismatch] [--compact] " "[--set-as-boundary ]... " - "[--report-skipped-pos] | " + "[--report-skipped-pos] [--skip-gated-clock-flops] | " "-systemverilog/-sv [--sv_design1_flist ] [--sv_design1_top ] " "[--sv_design2_flist ] [--sv_design2_top ] [-v ] [-k ] [--sec-engine ] [--sec-encoding ] [--learn-internal-relations ] [--allow-x-equality-in-internal-relations ] [--sec-reset-cycles ] [--sec-reset-port ...] " "[--design1 ] [--design2 ] " "[--allow-boundary-mismatch] [--compact] " "[--set-as-boundary ]... " - "[--report-skipped-pos] " + "[--report-skipped-pos] [--skip-gated-clock-flops] " "[--dump-btor2 ] [--dump-only] (BTOR2 export requires SEC)", prog); // LCOV_EXCL_START @@ -510,6 +510,7 @@ static bool validateConfigKeys(const YAML::Node& cfg) { "dump_cnf_path", "compact_mode", "report_skipped_pos", + "skip_gated_clock_flops", "solver", "sv_design1_flist", "sv_design2_flist", @@ -1342,6 +1343,7 @@ static int KeplerFormalMainImpl( std::string dumpPoCnfPath; KEPLER_FORMAL::Config::setReportSkippedPOs(false); + bool skipGatedClockFlops = false; for (int i = 1; i < argc; ++i) { std::string a = argv[i]; @@ -1598,6 +1600,12 @@ static int KeplerFormalMainImpl( } // LCOV_EXCL_STOP + // skip_gated_clock_flops (experimental) + if (cfg["skip_gated_clock_flops"] && + cfg["skip_gated_clock_flops"].IsScalar()) { + skipGatedClockFlops = cfg["skip_gated_clock_flops"].as(); + } + // verilog_preprocessing (optional) if (cfg["verilog_preprocessing"] && cfg["verilog_preprocessing"].IsScalar()) { // LCOV_EXCL_START @@ -2079,6 +2087,10 @@ static int KeplerFormalMainImpl( continue; // LCOV_EXCL_STOP } + if (arg == "--skip-gated-clock-flops") { + skipGatedClockFlops = true; + continue; + } // LCOV_EXCL_START if (arg == "--sv_design1_flist" || arg == "--sv_design2_flist" || arg == "--verilog_design1_top" || arg == "--verilog_design2_top" || @@ -2399,6 +2411,12 @@ static int KeplerFormalMainImpl( auto solverType = KEPLER_FORMAL::Config::getSolverType(); KEPLER_FORMAL::Config::setReportSkippedPOs(reportSkippedPOs); + KEPLER_FORMAL::Config::setSkipGatedClockFlops(skipGatedClockFlops); + if (skipGatedClockFlops) { + SPDLOG_WARN( + "skip_gated_clock_flops (experimental): the next state of a flop " + "clocked through a cell that cannot be modelled is not compared"); + } const char* solverName = solverType == KEPLER_FORMAL::Config::SolverType::KISSAT ? "KISSAT" diff --git a/src/config/Config.h b/src/config/Config.h index e62f46af..58075537 100644 --- a/src/config/Config.h +++ b/src/config/Config.h @@ -69,12 +69,25 @@ class Config { return reportSkippedPOs_; } + // Experimental: leave out the next-state comparison of every flop whose + // clock pin is driven by a cell the tool cannot model (an integrated + // clock gate's latch), with a warning that lists them, and compare the + // rest. Off by default. + static void setSkipGatedClockFlops(bool enabled) { + skipGatedClockFlops_ = enabled; + } + + static bool getSkipGatedClockFlops() { + return skipGatedClockFlops_; + } + private: Config() = default; ~Config() = default; inline static SolverType solverType_ = KISSAT; inline static bool reportSkippedPOs_ = false; + inline static bool skipGatedClockFlops_ = false; inline static std::atomic nextVerificationGeneration_{1}; inline static std::atomic verificationGeneration_{0}; }; diff --git a/src/strategies/miter/BuildPrimaryOutputClauses.cpp b/src/strategies/miter/BuildPrimaryOutputClauses.cpp index 1c71e3be..8633da1d 100644 --- a/src/strategies/miter/BuildPrimaryOutputClauses.cpp +++ b/src/strategies/miter/BuildPrimaryOutputClauses.cpp @@ -12,6 +12,7 @@ #include "NajaProperty.h" #include "../../config/Config.h" #include +#include #include #include #include @@ -79,6 +80,7 @@ bool shouldReportSkippedPOs() { const char* kSkippedMultiDriverPOReport = "skipped_multi_driver_pos.txt"; const char* kSkippedNoDriverPOReport = "skipped_no_driver_pos.txt"; +const char* kSkippedGatedClockPOReport = "skipped_gated_clock_pos.txt"; struct SparseReportedIDs { bool mark(const DNLFull* dnl, size_t nBits, DNLID id) { @@ -259,6 +261,51 @@ BuildPrimaryOutputClauses::SkippedOutputInfo makeSkippedOutputInfo( return {reason, std::move(detail), opaqueTerm}; } +// The cell output driving a clock pin of the sequential instance that +// input `termID` belongs to, when the tool cannot model it: no truth +// table, yet a combinational dependency on the cell's inputs, which is how +// an integrated clock gate's GCLK (CLK & latched enable) comes out of the +// liberty. DNLID_MAX otherwise: not a sequential cell's input, or a clock +// from a port, a buffer (it has a truth table) or a clock divider's flop +// (no combinational inputs). A clock pin is an input with clock-related +// inputs of its own. +DNLID gatedClockDriver(DNLID termID) { + const DNLFull* dnl = naja::DNL::get(); + const auto& term = dnl->getDNLTerminalFromID(termID); + if (term.isNull() || term.isTopPort() || + term.getSnlBitTerm()->getDirection() == SNLBitTerm::Direction::Output) { + return DNLID_MAX; + } + const auto& instance = term.getDNLInstance(); + for (DNLID t = instance.getTermIndexes().first; + t != DNLID_MAX && t <= instance.getTermIndexes().second; ++t) { + const auto& clockTerm = dnl->getDNLTerminalFromID(t); + if (clockTerm.getSnlBitTerm()->getDirection() == + SNLBitTerm::Direction::Output || + SNLDesignModeling::getClockRelatedInputs(clockTerm.getSnlBitTerm()) + .empty() || + clockTerm.getIsoID() == DNLID_MAX) { + continue; + } + const auto& iso = + dnl->getDNLIsoDB().getIsoFromIsoIDconst(clockTerm.getIsoID()); + for (DNLID d : iso.getDrivers()) { + const auto& driver = dnl->getDNLTerminalFromID(d); + if (driver.isNull() || driver.isTopPort()) { + continue; + } + auto* bitTerm = driver.getSnlBitTerm(); + const auto tt = SNLDesignModeling::getTruthTable(bitTerm->getDesign(), + bitTerm->getOrderID()); + if (!tt.isInitialized() && + !SNLDesignModeling::getCombinatorialInputs(bitTerm).empty()) { + return d; + } + } + } + return DNLID_MAX; +} + void reportSkippedPO(const DNLFull* dnl, const DNLTerminalFull& term, const char* reason, @@ -872,12 +919,55 @@ void BuildPrimaryOutputClauses::build() { // LCOV_EXCL_STOP IsPOs_[po] = true; } + // Experimental (skip_gated_clock_flops): a flop's data input is a + // compared output, its next state; with the clock gated by a cell the + // tool cannot model, the enable lives on the clock and the data input + // alone is not the next state. Those are left out, each one decided + // here, before outputs on one iso share a representative, so a skip + // never reaches an output that is not a gated flop's. + std::vector gatedClockOutput(outputs_.size(), false); + if (Config::getSkipGatedClockFlops()) { + size_t gatedCount = 0; + for (size_t i = 0; i < outputs_.size(); ++i) { + const DNLID gate = gatedClockDriver(outputs_[i]); + if (gate == DNLID_MAX) { + continue; + } + const auto& gateTerm = get()->getDNLTerminalFromID(gate); + const std::string detail = + "experimental skip_gated_clock_flops: the flop is clocked through " + + gateTerm.getDNLInstance().getSNLModel()->getName().getString() + + "/" + gateTerm.getSnlBitTerm()->getName().getString() + + ", which cannot be modelled; its next state is not compared"; + gatedClockOutput[i] = true; + POs_[i] = BoolExpr::createInvalid(); + skippedOutputs_[outputs_[i]] = + makeSkippedOutputInfo(SkippedOutputReason::GatedClock, detail, gate); + reportSkippedPO(get(), get()->getDNLTerminalFromID(outputs_[i]), + detail.c_str(), kSkippedGatedClockPOReport); + ++gatedCount; + } + if (gatedCount > 0) { + std::fprintf(stderr, + "WARNING: skip_gated_clock_flops (experimental): %zu flop " + "input(s) clocked through a cell that cannot be modelled " + "were not compared%s\n", + gatedCount, + shouldReportSkippedPOs() + ? "; listed in skipped_gated_clock_pos.txt" + : "; report_skipped_pos lists them"); + } + } std::vector representativeForOutput(outputs_.size()); std::vector representativeOutputs; representativeOutputs.reserve(outputs_.size()); std::unordered_map firstOutputForIso; firstOutputForIso.reserve(outputs_.size()); for (size_t i = 0; i < outputs_.size(); ++i) { + if (gatedClockOutput[i]) { + representativeForOutput[i] = i; + continue; + } const DNLID isoID = get()->getDNLTerminalFromID(outputs_[i]).getIsoID(); if (isoID != DNLID_MAX) { auto [it, inserted] = firstOutputForIso.emplace(isoID, i); diff --git a/src/strategies/miter/BuildPrimaryOutputClauses.h b/src/strategies/miter/BuildPrimaryOutputClauses.h index 49403250..3fe51461 100644 --- a/src/strategies/miter/BuildPrimaryOutputClauses.h +++ b/src/strategies/miter/BuildPrimaryOutputClauses.h @@ -46,6 +46,7 @@ class BuildPrimaryOutputClauses { // LCOV_EXCL_LINE LogicalLoop, OpaqueInternal, UnknownConstant, + GatedClock, }; struct SkippedOutputInfo { // LCOV_EXCL_LINE diff --git a/test/strategies/miter/MiterTests.cpp b/test/strategies/miter/MiterTests.cpp index 628c2266..69ec150b 100644 --- a/test/strategies/miter/MiterTests.cpp +++ b/test/strategies/miter/MiterTests.cpp @@ -9,6 +9,7 @@ #include #include #include +#include #include #include #include @@ -3914,6 +3915,145 @@ TEST(KeplerCliSubprocessTests, ExampleRunWritesConfiguredLogFile) { } // Required main function for Google Test +TEST_F(MiterTests, SkipGatedClockFlopsLeavesOutOnlyFlopsClockedThroughAnIcg) { + // An integrated clock gate as asap7's liberty writes it (opaque: a + // statetable latch) gating one flop; a second flop on the free clock. + const auto libertyPath = testTempPath("gated_clock.lib"); + { + std::ofstream liberty(libertyPath); + ASSERT_TRUE(liberty.good()); + liberty << R"liberty( +library (gated_clock) { + cell (ICG) { + clock_gating_integrated_cell : latch_posedge_precontrol; + statetable ("CLK ENA SE", "IQ") { + table : "L L L : - : L, + L L H : - : H, + L H L : - : H, + L H H : - : H, + H - - : - : N"; + } + pin (IQ) { + direction : internal; + internal_node : "IQ"; + } + pin (GCLK) { + direction : output; + state_function : "CLK & IQ"; + } + pin (CLK) { + direction : input; + clock : true; + } + pin (ENA) { + direction : input; + } + pin (SE) { + direction : input; + } + } + cell (DFF) { + ff (IQ, IQN) { + clocked_on : "CLK"; + next_state : "D"; + } + pin (D) { + direction : input; + } + pin (CLK) { + direction : input; + clock : true; + } + pin (Q) { + direction : output; + function : "IQ"; + } + } +} +)liberty"; + } + auto* universe = NLUniverse::create(); + auto* db = NLDB::create(universe); + auto* cells = + NLLibrary::create(db, NLLibrary::Type::Primitives, NLName("gated_clock")); + SNLLibertyConstructor constructor(cells); + constructor.construct(libertyPath); + auto* icg = cells->getSNLDesign(NLName("ICG")); + auto* dff = cells->getSNLDesign(NLName("DFF")); + ASSERT_NE(nullptr, icg); + ASSERT_NE(nullptr, dff); + + auto* designs = + NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs")); + auto* top = + SNLDesign::create(designs, SNLDesign::Type::Standard, NLName("top")); + universe->setTopDesign(top); + auto port = [&](const char* name, SNLTerm::Direction direction) { + auto* term = SNLScalarTerm::create(top, direction, NLName(name)); + auto* net = SNLScalarNet::create(top, NLName(std::string("net_") + name)); + term->setNet(net); + return net; + }; + auto* clk = port("clk", SNLTerm::Direction::Input); + auto* en = port("en", SNLTerm::Direction::Input); + auto* d0 = port("d0", SNLTerm::Direction::Input); + auto* d1 = port("d1", SNLTerm::Direction::Input); + auto* q0 = port("q0", SNLTerm::Direction::Output); + auto* q1 = port("q1", SNLTerm::Direction::Output); + auto* gclk = SNLScalarNet::create(top, NLName("gclk")); + auto connect = [](SNLInstance* instance, const char* pin, SNLNet* net) { + instance->getInstTerm(instance->getModel()->getScalarTerm(NLName(pin))) + ->setNet(net); + }; + auto* gate = SNLInstance::create(top, icg, NLName("gate")); + connect(gate, "CLK", clk); + connect(gate, "ENA", en); + connect(gate, "SE", en); + connect(gate, "GCLK", gclk); + auto* gated = SNLInstance::create(top, dff, NLName("gated")); + connect(gated, "CLK", gclk); + connect(gated, "D", d0); + connect(gated, "Q", q0); + auto* ungated = SNLInstance::create(top, dff, NLName("ungated")); + connect(ungated, "CLK", clk); + connect(ungated, "D", d1); + connect(ungated, "Q", q1); + + using Reason = BuildPrimaryOutputClauses::SkippedOutputReason; + // Every skipped output, by /. + auto skipped = [&](bool skipGatedClockFlops) { + KEPLER_FORMAL::Config::setSkipGatedClockFlops(skipGatedClockFlops); + naja::DNL::destroy(); + naja::DNL::get(); + BuildPrimaryOutputClauses builder; + builder.setRetainDnl(true); + builder.collect(); + builder.build(); + std::map out; + for (const auto& [id, info] : builder.getSkippedOutputs()) { + const auto& term = naja::DNL::get()->getDNLTerminalFromID(id); + out[term.getDNLInstance().getSNLInstance()->getName().getString() + "/" + + term.getSnlBitTerm()->getName().getString()] = info.reason; + } + KEPLER_FORMAL::Config::setSkipGatedClockFlops(false); + return out; + }; + + const auto on = skipped(true); + ASSERT_EQ(1u, on.count("gated/D")); + EXPECT_EQ(Reason::GatedClock, on.at("gated/D")); + for (const auto& [name, reason] : on) { + if (name.rfind("gated/", 0) != 0) { + EXPECT_NE(Reason::GatedClock, reason) << name; + } + } + EXPECT_EQ(0u, on.count("ungated/D")); + + for (const auto& [name, reason] : skipped(false)) { + EXPECT_NE(Reason::GatedClock, reason) << name; + } +} + int main(int argc, char** argv) { ::testing::InitGoogleTest(&argc, argv); return RUN_ALL_TESTS();