From 203d0698532c27a897cefd448a442a36656ef5aa Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Mon, 5 Oct 2026 11:07:00 +0200 Subject: [PATCH 1/2] Model RTL X constant literals as permanently-X state in SEC An X literal such as `case ... default: y = 'x;` reaches the cone compiler as an X-constant net, which had no leaf representation: the cone was dropped as unknown-constant and every output depending on it went unproved, although the dual-rail encoding can represent X. Give each X-constant net its own variable when SEC asks for it, and make SEC publish that variable as 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 binary-defined difference, which is the usual don't-care reading. Unused X states are pruned, the structured memory control-pin path keeps treating an X write enable as a disabled write, LEC is unchanged, and Z literals remain unsupported. --- docs/sec-sequential-models.md | 11 +++ src/sec/model/SequentialDesignModel.cpp | 78 +++++++++++++++++- .../miter/BuildPrimaryOutputClauses.cpp | 22 +++++ .../miter/BuildPrimaryOutputClauses.h | 11 +++ .../SequentialEquivalenceStrategyTests.cpp | 81 +++++++++++++++++++ .../strategies/miter/KeplerFormalCliTests.cpp | 9 ++- 6 files changed, 205 insertions(+), 7 deletions(-) diff --git a/docs/sec-sequential-models.md b/docs/sec-sequential-models.md index b8f69023..e06f4d0e 100644 --- a/docs/sec-sequential-models.md +++ b/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 diff --git a/src/sec/model/SequentialDesignModel.cpp b/src/sec/model/SequentialDesignModel.cpp index 2b7a4d47..eef63e70 100644 --- a/src/sec/model/SequentialDesignModel.cpp +++ b/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 normalizedRoots; normalizedRoots.reserve(requestedOutputs.size()); std::unordered_map> 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(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 xKeys; + for (const auto& key : model.stateBits) { + if (isXConstantStateKey(key)) { + xKeys.push_back(key); + } + } + if (xKeys.empty()) { + return; + } + std::unordered_set 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 builderOutputs = ctx.builder.getOutputs(); std::vector termDNLID2varID = ctx.builder.getTermDNLID2VarID(); recordBoundaryInputVars(ctx, builderInputs, termDNLID2varID, model); + assignXConstantStateVars(ctx, model); std::unordered_map 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); diff --git a/src/strategies/miter/BuildPrimaryOutputClauses.cpp b/src/strategies/miter/BuildPrimaryOutputClauses.cpp index 1c71e3be..bec0d15f 100644 --- a/src/strategies/miter/BuildPrimaryOutputClauses.cpp +++ b/src/strategies/miter/BuildPrimaryOutputClauses.cpp @@ -715,6 +715,7 @@ std::vector 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 && diff --git a/src/strategies/miter/BuildPrimaryOutputClauses.h b/src/strategies/miter/BuildPrimaryOutputClauses.h index 49403250..548c4c4c 100644 --- a/src/strategies/miter/BuildPrimaryOutputClauses.h +++ b/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>& getXConstantVars() + const { + return xConstantVars_; + } const std::unordered_map& getInputsMap() const { return inputsMap_; @@ -155,6 +164,8 @@ class BuildPrimaryOutputClauses { // LCOV_EXCL_LINE size_t lastCommonID = 1; std::unordered_map skippedOutputs_; bool stopAtOpaqueInternalOutputs_ = false; + bool modelXConstants_ = false; + std::vector> xConstantVars_; mutable std::mutex skippedOutputsMutex_; struct hash { diff --git a/test/sec/SequentialEquivalenceStrategyTests.cpp b/test/sec/SequentialEquivalenceStrategyTests.cpp index 08e4f6e9..47922ce2 100644 --- a/test/sec/SequentialEquivalenceStrategyTests.cpp +++ b/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(); diff --git a/test/strategies/miter/KeplerFormalCliTests.cpp b/test/strategies/miter/KeplerFormalCliTests.cpp index 66ae30c2..955272be 100644 --- a/test/strategies/miter/KeplerFormalCliTests.cpp +++ b/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}, }; From 6f29764e8cd8ffaae1cf80cb463296a67a545207 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Mon, 12 Oct 2026 00:04:03 +0200 Subject: [PATCH 2/2] Reduce the X literal SEC test to a single-bit module Exercise the two shapes the fix covers, an x literal in a register's next state and in a combinational output, with one-bit ports and no surrounding mux logic. --- .../SequentialEquivalenceStrategyTests.cpp | 53 ++++++++----------- 1 file changed, 23 insertions(+), 30 deletions(-) diff --git a/test/sec/SequentialEquivalenceStrategyTests.cpp b/test/sec/SequentialEquivalenceStrategyTests.cpp index 47922ce2..e137fb81 100644 --- a/test/sec/SequentialEquivalenceStrategyTests.cpp +++ b/test/sec/SequentialEquivalenceStrategyTests.cpp @@ -16530,26 +16530,19 @@ TEST_F( 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) { +// The two smallest shapes an `x` literal takes in RTL: one branch of a +// register's next state, and one branch of a combinational output. +std::string xLiteralModuleSource(const std::string& name, + const std::string& literal) { 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 + input logic clk, + input logic s, + input logic a, + output logic q, + output logic y ); - 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; + always_ff @(posedge clk) q <= s ? a : )" + literal + R"(; + assign y = s ? a : )" + literal + R"(; endmodule )"; } @@ -16557,26 +16550,24 @@ endmodule } // namespace TEST_F(SequentialEquivalenceStrategyTests, - DualRailSecModelsCaseDefaultXLiteralAsPermanentX) { + DualRailSecModelsXLiteralAsPermanentX) { 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")); + library, "x_literal", xLiteralModuleSource("x_literal", "1'bx")); auto* xCopy = loadSystemVerilogTopFromSource( - library, "case_default_x_copy", - caseDefaultModuleSource("case_default_x_copy", "8'bx")); + library, "x_literal_copy", xLiteralModuleSource("x_literal_copy", "1'bx")); auto* zeroTop = loadSystemVerilogTopFromSource( - library, "case_default_zero", - caseDefaultModuleSource("case_default_zero", "8'b0")); + library, "zero_literal", xLiteralModuleSource("zero_literal", "1'b0")); - // The X literal is modeled, not skipped: every output stays covered and the - // model carries one uninitialized self-looping state bit for it. + // The X literal is modeled, not skipped: both outputs stay covered and the + // model carries uninitialized self-looping state for the literal. const auto extracted = SequentialDesignModel::extract(xTop); EXPECT_FALSE(extracted.hasUnsupportedFeatures()); EXPECT_TRUE(extracted.skippedObservedOutputs.empty()); - EXPECT_EQ(extracted.observedOutputs.size(), 8u); + EXPECT_EQ(extracted.observedOutputs.size(), 2u); size_t xStates = 0; for (const auto& [key, name] : extracted.displayNameByKey) { if (name.rfind("1'bx#", 0) != 0) { @@ -16588,7 +16579,9 @@ TEST_F(SequentialEquivalenceStrategyTests, ASSERT_NE(nextIt, extracted.nextStateExprByStateKey.end()); EXPECT_EQ(nextIt->second, BoolExpr::Var(extracted.inputVarByKey.at(key))); } - EXPECT_EQ(xStates, 1u); + // The frontend may share one constant net between the two literals. + EXPECT_GE(xStates, 1u); + EXPECT_LE(xStates, 2u); // X on both sides, and X against a synthesized don't-care value, are both // "no binary-defined difference" under the dual-rail encoding. @@ -16599,8 +16592,8 @@ TEST_F(SequentialEquivalenceStrategyTests, const auto result = strategy.run(4); EXPECT_EQ(result.status, SequentialEquivalenceStatus::Equivalent) << result.reason; - EXPECT_EQ(result.totalOutputs, 8u); - EXPECT_EQ(result.coveredOutputs, 8u); + EXPECT_EQ(result.totalOutputs, 2u); + EXPECT_EQ(result.coveredOutputs, 2u); } // The binary encoding has no X value: the bit is an uninitialized register