Experimental: --skip-gated-clock-flops, so a clock-gated netlist can be checked, minus its gated flops

src/bin/KeplerFormal.cpp

@@ -76,13 +76,13 @@ static void print_usage(const char* prog) {
       "<file...> [--verilog_design1_top <name>] [--verilog_design2_top <name>] [--vhdl_design1_top <name>] [--vhdl_design2_top <name>] [--python_design1_top <name>] [--python_design2_top <name>] [--liberty <library-file>...] [-v <lec|sec>] [-k <max-k>] [--sec-engine <k_induction|imc|pdr>] [--sec-encoding <binary|dual_rail_steady>] [--learn-internal-relations <true|false>] [--allow-x-equality-in-internal-relations <true|false>] [--sec-reset-cycles <n>] [--sec-reset-port <name=0|1>...] "
       "[--allow-boundary-mismatch] [--compact] "
       "[--set-as-boundary <design1-path> <design2-path>]... "
-      "[--report-skipped-pos] | "
+      "[--report-skipped-pos] [--skip-gated-clock-flops] | "
       "-systemverilog/-sv [--sv_design1_flist <file>] [--sv_design1_top <name>] "
       "[--sv_design2_flist <file>] [--sv_design2_top <name>] [-v <lec|sec>] [-k <max-k>] [--sec-engine <k_induction|imc|pdr>] [--sec-encoding <binary|dual_rail_steady>] [--learn-internal-relations <true|false>] [--allow-x-equality-in-internal-relations <true|false>] [--sec-reset-cycles <n>] [--sec-reset-port <name=0|1>...] "
       "[--design1 <file...>] [--design2 <file...>] "
       "[--allow-boundary-mismatch] [--compact] "
       "[--set-as-boundary <design1-path> <design2-path>]... "
-      "[--report-skipped-pos] "
+      "[--report-skipped-pos] [--skip-gated-clock-flops] "
       "[--dump-btor2 <file>] [--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<bool>();
+        }
+
         // 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"

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<uint64_t> nextVerificationGeneration_{1};
   inline static std::atomic<uint64_t> verificationGeneration_{0};
 };

src/strategies/miter/BuildPrimaryOutputClauses.cpp

@@ -12,6 +12,7 @@
 #include "NajaProperty.h"
 #include "../../config/Config.h"
 #include <algorithm>
+#include <cstdio>
 #include <fstream>
 #include <mutex>
 #include <ostream>
@@ -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<bool> 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<size_t> representativeForOutput(outputs_.size());
   std::vector<size_t> representativeOutputs;
   representativeOutputs.reserve(outputs_.size());
   std::unordered_map<DNLID, size_t> 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);

src/strategies/miter/BuildPrimaryOutputClauses.h

@@ -46,6 +46,7 @@ class BuildPrimaryOutputClauses {  // LCOV_EXCL_LINE
     LogicalLoop,
     OpaqueInternal,
     UnknownConstant,
+    GatedClock,
   };
 
   struct SkippedOutputInfo {  // LCOV_EXCL_LINE

test/strategies/miter/MiterTests.cpp

@@ -9,6 +9,7 @@
 #include <filesystem>
 #include <fstream>
 #include <functional>
+#include <map>
 #include <set>
 #include <sstream>
 #include <string>
@@ -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 <instance>/<pin>.
+  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<std::string, Reason> 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();