Model RTL X constant literals as permanently-X state in SEC

docs/sec-sequential-models.md

@@ -46,6 +46,17 @@ state. Every latch output is opaque, including latches used in clock-gating
 structures, and any requested top-level output whose cone reaches it is
 skipped. SEC does not infer latch behavior from cell or pin names.
 
+## X Constant Literals
+
+An RTL `x` literal, typically a `case` default such as `default: y = 'x;`, is
+kept by the frontends as an X-constant net. SEC models each such net as a
+state bit with no initial value whose next state is itself: under the
+dual-rail encoding it is X forever, so a binary value on the other side is not
+a binary-defined difference. This is the usual don't-care reading of such
+literals. Under the binary encoding the bit behaves like any uninitialized
+register, and dependent outputs are skipped. Z literals remain unsupported and
+skip the cones that read them.
+
 ## Opaque Outputs
 
 Opacity is strict and local to an output terminal. During backward cone

src/sec/model/SequentialDesignModel.cpp

@@ -681,13 +681,15 @@ MaterializedBuilderOutputs materializeBuilderOutputs(
     bool secDiagEnabled,
     const char* topName,
     const char* phaseLabel,
-    const LeafBoundary* boundary) {
+    const LeafBoundary* boundary,
+    bool modelXConstants) {
   MaterializedBuilderOutputs result;
 
   KEPLER_FORMAL::BuildPrimaryOutputClauses builder;
   builder.setRetainDnl(true);
   builder.setLeafBoundary(boundary);
   builder.setStopAtOpaqueInternalOutputs(true);
+  builder.setModelXConstants(modelXConstants);
   std::vector<naja::DNL::DNLID> normalizedRoots;
   normalizedRoots.reserve(requestedOutputs.size());
   std::unordered_map<naja::DNL::DNLID, std::vector<naja::DNL::DNLID>> requestedByRoot;
@@ -3352,6 +3354,70 @@ size_t getNextSyntheticVarID(const SequentialDesignModel& model) {
   return nextVarID;
 }
 
+constexpr uint64_t kXConstantStateTag = uint64_t{1} << 61;
+
+SignalKey xConstantStateKey(naja::DNL::DNLID isoID) {
+  return {{kXConstantStateTag, static_cast<uint64_t>(isoID)}, {0}};
+}
+
+bool isXConstantStateKey(const SignalKey& key) {
+  return key.first.size() == 2 && key.first.front() == kXConstantStateTag;
+}
+
+// Drop the X-constant states no modeled cone reads, for example an X write
+// enable that the structured-memory rules handled instead.
+void pruneUnusedXConstantStates(SequentialDesignModel& model) {
+  std::vector<SignalKey> xKeys;
+  for (const auto& key : model.stateBits) {
+    if (isXConstantStateKey(key)) {
+      xKeys.push_back(key);
+    }
+  }
+  if (xKeys.empty()) {
+    return;
+  }
+  std::unordered_set<size_t> used;
+  const auto collect = [&used](BoolExpr* expr) {
+    if (expr != nullptr) {
+      const auto support = expr->getSupportVars();
+      used.insert(support.begin(), support.end());
+    }
+  };
+  for (const auto& [_, expr] : model.observedOutputExprByKey) {
+    collect(expr);
+  }
+  for (const auto& [key, expr] : model.nextStateExprByStateKey) {
+    if (!isXConstantStateKey(key)) {
+      collect(expr);
+    }
+  }
+  for (const auto& key : xKeys) {
+    if (used.contains(model.inputVarByKey.at(key))) {
+      continue;
+    }
+    std::erase(model.stateBits, key);
+    model.inputVarByKey.erase(key);
+    model.nextStateExprByStateKey.erase(key);
+    model.displayNameByKey.erase(key);
+  }
+}
+
+// An X-constant literal (`1'bx`) becomes a state bit with no initial value
+// whose next state is itself: permanently X under the dual-rail encoding, so a
+// binary value on the other side is not a difference. Register these before
+// other synthetic state so later variable IDs are allocated above them.
+void assignXConstantStateVars(
+    const ExtractContext& ctx,
+    SequentialDesignModel& model) {
+  for (const auto& [isoID, varID] : ctx.builder.getXConstantVars()) {
+    const SignalKey key = xConstantStateKey(isoID);
+    model.stateBits.push_back(key);
+    model.inputVarByKey.emplace(key, varID);
+    model.nextStateExprByStateKey.emplace(key, BoolExpr::Var(varID));
+    model.displayNameByKey.emplace(key, "1'bx#" + std::to_string(isoID));
+  }
+}
+
 void assignStructuredMemoryStateVars(
     const ExtractContext& ctx,
     SequentialDesignModel& model) {
@@ -4117,7 +4183,7 @@ RebuiltTransitionArtifacts rebuildRequiredStateTransitions(
       const auto dependencyOutputs = materializeBuilderOutputs(
           batchOutputTerms, builderInputs, termDNLID2varID,
           ctx.collectedSkippedOutputs, ctx.secDiagEnabled, ctx.topName.c_str(),
-          "dependency build", ctx.boundary);
+          "dependency build", ctx.boundary, /*modelXConstants=*/true);
       appendUniqueTermIDs(builderInputs, dependencyOutputs.inputs);
       appendUniqueTermIDs(builderOutputs, dependencyOutputs.outputs);
       mergeBuilderTermVarIDs(termDNLID2varID,
@@ -4869,6 +4935,7 @@ SequentialDesignModel SequentialDesignModel::extract(
   };
   ctx.builder.setRetainDnl(true);
   ctx.builder.setBoundaryPairs(pairs, side);
+  ctx.builder.setModelXConstants(true);
 
   // Phase 1: collect the raw boundary, classify top I/O vs sequential state,
   // and scan leaf sequentials so the later formula build knows what it must
@@ -4911,6 +4978,7 @@ SequentialDesignModel SequentialDesignModel::extract(
   std::vector<naja::DNL::DNLID> builderOutputs = ctx.builder.getOutputs();
   std::vector<size_t> termDNLID2varID = ctx.builder.getTermDNLID2VarID();
   recordBoundaryInputVars(ctx, builderInputs, termDNLID2varID, model);
+  assignXConstantStateVars(ctx, model);
 
   std::unordered_map<naja::DNL::DNLID, BoolExpr*> outputExprByTerm;
   const auto& outputTerms = builderOutputs;
@@ -4937,7 +5005,10 @@ SequentialDesignModel SequentialDesignModel::extract(
         ctx.collectedSkippedOutputs,
         ctx.secDiagEnabled,
         ctx.topName.c_str(),
-        "structured memory dependency build", ctx.boundary);
+        // Memory control pins keep their existing rules: an X write enable
+        // stays a disabled write rather than a modeled X.
+        "structured memory dependency build", ctx.boundary,
+        /*modelXConstants=*/false);
     appendUniqueTermIDs(builderInputs, dependencyOutputs.inputs);
     appendUniqueTermIDs(builderOutputs, dependencyOutputs.outputs);
     mergeBuilderTermVarIDs(termDNLID2varID, dependencyOutputs.termDNLID2varID);
@@ -4993,6 +5064,7 @@ SequentialDesignModel SequentialDesignModel::extract(
       outputExprByTerm,
       skippedOutputsByTerm);
   applyRebuiltTransitionArtifacts(rebuiltArtifacts, model);
+  pruneUnusedXConstantStates(model);
   filterUnsupportedAndUnmappedBoundary(ctx, model);
   composeSameDomainPhaseTransitions(model);
   markMultiClockDomainConesAsSkipped(model);

src/strategies/miter/BuildPrimaryOutputClauses.cpp

@@ -715,6 +715,7 @@ std::vector<DNLID> BuildPrimaryOutputClauses::collectOutputs() {
     const auto& iso =
         dnl->getDNLIsoDB().getIsoFromIsoIDconst(term.getIsoID());
     if (!iso.isConstant0() && !iso.isConstant1() &&
+        !(modelXConstants_ && iso.isConstantX()) &&
         iso.getDrivers().empty()) {
       const auto skip = describeUnmappedTerm(out, "its iso has no drivers");
       skippedOutputs_[out] = skip;
@@ -835,6 +836,23 @@ void BuildPrimaryOutputClauses::initVarNames() {
         termDNLID2varID_[termID] = 1;
     }
   }
+  xConstantVars_.clear();
+  if (modelXConstants_) {
+    // Number X variables past every terminal: input variables are numbered
+    // from 2 and never exceed the terminal count, so builders with different
+    // input lists still agree on each X variable (the iso set is ordered).
+    size_t nextVar = termDNLID2varID_.size() + 2;
+    for (DNLID isoID : naja::DNL::get()->getDNLIsoDB().getConstantXIsos()) {
+      const auto& iso = naja::DNL::get()->getDNLIsoDB().getIsoFromIsoIDconst(isoID);
+      for (auto termID : iso.getReaders()) {
+        termDNLID2varID_[termID] = nextVar;
+      }
+      for (auto termID : iso.getDrivers()) {
+        termDNLID2varID_[termID] = nextVar;
+      }
+      xConstantVars_.emplace_back(isoID, nextVar++);
+    }
+  }
 }
 
 void BuildPrimaryOutputClauses::build() {
@@ -915,6 +933,10 @@ void BuildPrimaryOutputClauses::build() {
         POs_[i] = BoolExpr::createTrue();
         return;
       }
+      if (modelXConstants_ && iso.isConstantX()) {
+        POs_[i] = BoolExpr::Var(termDNLID2varID_[out]);
+        return;
+      }
     }
     auto cachedIt = Tree2BoolExpr::iso2boolExpr_.find(isoID);
     if (isoID != DNLID_MAX &&

src/strategies/miter/BuildPrimaryOutputClauses.h

@@ -98,6 +98,15 @@ class BuildPrimaryOutputClauses {  // LCOV_EXCL_LINE
   void setStopAtOpaqueInternalOutputs(bool stop) {
     stopAtOpaqueInternalOutputs_ = stop;
   }
+  // Give every X-constant net (`1'bx`) its own variable instead of skipping
+  // the cones that read it. SEC models those variables as permanently-X
+  // state. Off by default: the binary LEC encoding has no X value.
+  void setModelXConstants(bool model) { modelXConstants_ = model; }
+  // (iso, variable) pairs assigned by build(); deterministic for one DNL.
+  const std::vector<std::pair<naja::DNL::DNLID, size_t>>& getXConstantVars()
+      const {
+    return xConstantVars_;
+  }
   const std::unordered_map<PathKey, naja::DNL::DNLID, KeyHash>&
   getInputsMap() const {
     return inputsMap_;
@@ -155,6 +164,8 @@ class BuildPrimaryOutputClauses {  // LCOV_EXCL_LINE
   size_t lastCommonID = 1;
   std::unordered_map<naja::DNL::DNLID, SkippedOutputInfo> skippedOutputs_;
   bool stopAtOpaqueInternalOutputs_ = false;
+  bool modelXConstants_ = false;
+  std::vector<std::pair<naja::DNL::DNLID, size_t>> xConstantVars_;
   mutable std::mutex skippedOutputsMutex_;
 
   struct hash {

test/sec/SequentialEquivalenceStrategyTests.cpp

@@ -16528,6 +16528,87 @@ TEST_F(
   EXPECT_FALSE(extracted.hasUnsupportedFeatures());
 }
 
+namespace {
+
+// A registered read mux whose `case` default is the given literal: `'x` is
+// the usual don't-care idiom for unlisted addresses.
+std::string caseDefaultModuleSource(const std::string& name,
+                                    const std::string& defaultValue) {
+  return "module " + name + R"((
+  input  logic       clk_i,
+  input  logic [1:0] addr_i,
+  input  logic [7:0] a_i,
+  input  logic [7:0] b_i,
+  output logic [7:0] dat_o
+);
+  logic [7:0] dat;
+  always_comb begin
+    case (addr_i)
+      2'd0:    dat = a_i;
+      2'd1:    dat = b_i;
+      default: dat = )" + defaultValue + R"(;
+    endcase
+  end
+  always_ff @(posedge clk_i) dat_o <= dat;
+endmodule
+)";
+}
+
+}  // namespace
+
+TEST_F(SequentialEquivalenceStrategyTests,
+       DualRailSecModelsCaseDefaultXLiteralAsPermanentX) {
+  NLUniverse::create();
+  auto* db = NLDB::create(NLUniverse::get());
+  auto* library =
+      NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs"));
+  auto* xTop = loadSystemVerilogTopFromSource(
+      library, "case_default_x", caseDefaultModuleSource("case_default_x", "8'bx"));
+  auto* xCopy = loadSystemVerilogTopFromSource(
+      library, "case_default_x_copy",
+      caseDefaultModuleSource("case_default_x_copy", "8'bx"));
+  auto* zeroTop = loadSystemVerilogTopFromSource(
+      library, "case_default_zero",
+      caseDefaultModuleSource("case_default_zero", "8'b0"));
+
+  // The X literal is modeled, not skipped: every output stays covered and the
+  // model carries one uninitialized self-looping state bit for it.
+  const auto extracted = SequentialDesignModel::extract(xTop);
+  EXPECT_FALSE(extracted.hasUnsupportedFeatures());
+  EXPECT_TRUE(extracted.skippedObservedOutputs.empty());
+  EXPECT_EQ(extracted.observedOutputs.size(), 8u);
+  size_t xStates = 0;
+  for (const auto& [key, name] : extracted.displayNameByKey) {
+    if (name.rfind("1'bx#", 0) != 0) {
+      continue;
+    }
+    ++xStates;
+    EXPECT_EQ(extracted.initialStateValueByKey.count(key), 0u);
+    const auto nextIt = extracted.nextStateExprByStateKey.find(key);
+    ASSERT_NE(nextIt, extracted.nextStateExprByStateKey.end());
+    EXPECT_EQ(nextIt->second, BoolExpr::Var(extracted.inputVarByKey.at(key)));
+  }
+  EXPECT_EQ(xStates, 1u);
+
+  // X on both sides, and X against a synthesized don't-care value, are both
+  // "no binary-defined difference" under the dual-rail encoding.
+  for (auto* other : {xCopy, zeroTop}) {
+    SequentialEquivalenceStrategy strategy(
+        xTop, other, KEPLER_FORMAL::Config::SolverType::KISSAT, SecEngine::Pdr,
+        SecEncoding::DualRailSteady);
+    const auto result = strategy.run(4);
+    EXPECT_EQ(result.status, SequentialEquivalenceStatus::Equivalent)
+        << result.reason;
+    EXPECT_EQ(result.totalOutputs, 8u);
+    EXPECT_EQ(result.coveredOutputs, 8u);
+  }
+
+  // The binary encoding has no X value: the bit is an uninitialized register
+  // there, so the dependent outputs are skipped rather than reported different.
+  const auto binary = makeBinarySecStrategy(xTop, xCopy).run(4);
+  EXPECT_NE(binary.status, SequentialEquivalenceStatus::Different);
+}
+
 TEST_F(SequentialEquivalenceStrategyTests,
        SequentialDesignModelExtractModelsInferredMemoryWithConstantFalseCommitGuard) {
   NLUniverse::create();

test/strategies/miter/KeplerFormalCliTests.cpp

@@ -4267,15 +4267,16 @@ TEST_F(KeplerFormalCliTests,
     const char* diagnostic;
     bool undriven = false;
   };
+  // SEC models X literals as permanently-X state (see
+  // docs/sec-sequential-models.md), so only Z literals are reported.
   const Case cases[] = {
-      {"x_ternary", "assign y = sel ? d : 1'bx;",
-       "unsupported X constant (1'bx)"},
+      {"x_ternary", "assign y = sel ? d : 1'bx;", nullptr},
       {"z_bitwise", "assign y = d & 1'bz;",
        "unsupported Z constant (1'bz)"},
-      {"x_direct", "assign y = 1'bx;", "unsupported X constant (1'bx)"},
+      {"x_direct", "assign y = 1'bx;", nullptr},
       {"z_direct", "assign y = 1'bz;", "unsupported Z constant (1'bz)"},
       {"x_next_state", "always_ff @(posedge clk) y <= sel ? d : 1'bx;",
-       "unsupported X constant (1'bx)"},
+       nullptr},
       {"known_zero", "assign y = sel ? d : 1'b0;", nullptr},
       {"undriven", "assign y = undriven;", nullptr, true},
   };