From 683bd551591f52d61a45b58b94b9370b90c46bd1 Mon Sep 17 00:00:00 2001
From: Emin <me@emin.chat>
Date: Tue, 22 Sep 2026 12:06:40 +0800
Subject: [PATCH 01/14] Harvest DFF INIT parameters as SEC initial state values

---
 src/sec/model/SequentialDesignModel.cpp       |  95 ++++++++
 .../SequentialEquivalenceStrategyTests.cpp    | 213 ++++++++++++++++++
 2 files changed, 308 insertions(+)

diff --git a/src/sec/model/SequentialDesignModel.cpp b/src/sec/model/SequentialDesignModel.cpp
index 2b7a4d47..9cad5965 100644
--- a/src/sec/model/SequentialDesignModel.cpp
+++ b/src/sec/model/SequentialDesignModel.cpp
@@ -27,7 +27,11 @@
 #include "NLDB0.h"
 #include "NLName.h"
 #include "NLUniverse.h"
+#include "SNLBusTerm.h"
+#include "SNLBusTermBit.h"
 #include "SNLDesignModeling.h"
+#include "SNLInstParameter.h"
+#include "SNLInstance.h"
 #include "SNLPath.h"
 #include "../../clauses/SNLLogicCloud.h"
 #include "../../clauses/Tree2BoolExpr.h"
@@ -3157,6 +3161,96 @@ void appendPendingTransitionsForInstance(
   }
 }
 
+// Reads the DFF INIT instance parameter (written by the slang frontend when a
+// constant initial block or declaration initializer sets a register's
+// power-on value) for the given state output terminal. Returns the stored
+// digit for the terminal's bit in the storage element's own polarity, or
+// nullopt when the instance carries no explicit INIT or the digit is x/z.
+std::optional<bool> readDFFInitDigitForStateTerm(
+    const naja::DNL::DNLTerminalFull& term) {
+  if (term.isNull() || term.isTopPort()) {
+    return std::nullopt;  // LCOV_EXCL_LINE
+  }
+  const auto* snlInstance = term.getDNLInstance().getSNLInstance();
+  if (snlInstance == nullptr) {
+    return std::nullopt;  // LCOV_EXCL_LINE
+  }
+  const auto* initParam =
+      snlInstance->getInstParameter(naja::NL::NLName("INIT"));
+  if (initParam == nullptr) {
+    return std::nullopt;
+  }
+  const std::string value = initParam->getValue();
+  const auto basePos = value.find('\'');
+  if (basePos == std::string::npos || basePos + 2 >= value.size()) {
+    return std::nullopt;  // LCOV_EXCL_LINE
+  }
+  if (value[basePos + 1] != 'b' && value[basePos + 1] != 'B') {
+    return std::nullopt;  // LCOV_EXCL_LINE
+  }
+  size_t width = 0;
+  try {
+    width = std::stoul(value.substr(0, basePos));
+  } catch (...) {
+    return std::nullopt;  // LCOV_EXCL_LINE
+  }
+  const std::string digits = value.substr(basePos + 2);
+  if (width == 0 || digits.size() != width) {
+    return std::nullopt;  // LCOV_EXCL_LINE
+  }
+  // INIT digits are written MSB first (NLDB0::formatDFFInitValue), so the
+  // digit for bus bit b of a Q[msb:lsb] output sits at index msb-b.
+  size_t digitIndex = 0;
+  const auto* bitTerm = term.getSnlBitTerm();
+  if (const auto* busBit =
+          dynamic_cast<const naja::NL::SNLBusTermBit*>(bitTerm)) {
+    const auto* bus = busBit->getBus();
+    const auto offset =
+        static_cast<int64_t>(bus->getMSB()) - busBit->getBit();
+    if (offset < 0 || static_cast<size_t>(offset) >= width) {
+      return std::nullopt;  // LCOV_EXCL_LINE
+    }
+    digitIndex = static_cast<size_t>(offset);
+  } else if (width != 1) {
+    return std::nullopt;  // LCOV_EXCL_LINE
+  }
+  switch (std::tolower(static_cast<unsigned char>(digits[digitIndex]))) {
+    case '0':
+      return false;
+    case '1':
+      return true;
+    default:
+      return std::nullopt;  // x/z leave the state unconstrained
+  }
+}
+
+// Transfers DFF INIT metadata onto the extracted model. Each state key holds
+// values in its own observed pin polarity: the primary key follows
+// stateOutputIsComplemented (mirroring the next-state build) and complemented
+// keys get the opposite value.
+void harvestInitialStateValues(ExtractContext& ctx, SequentialDesignModel& model) {
+  size_t harvested = 0;
+  for (const auto& pending : ctx.pendingTransitions) {
+    const auto& term = ctx.dnl->getDNLTerminalFromID(pending.stateTermID);
+    const auto digit = readDFFInitDigitForStateTerm(term);
+    if (!digit.has_value()) {
+      continue;
+    }
+    const bool value = pending.stateOutputIsComplemented ? !*digit : *digit;
+    model.initialStateValueByKey.emplace(pending.stateKey, value);
+    for (const auto& complementedKey : pending.complementedStateKeys) {
+      model.initialStateValueByKey.emplace(complementedKey, !value);
+    }
+    ++harvested;
+  }
+  if (ctx.secDiagEnabled && harvested > 0) {
+    fprintf(stderr,
+            "SEC diag: extract(%s) harvested initial state values=%zu\n",
+            ctx.topName.c_str(), harvested);
+    fflush(stderr);
+  }
+}
+
 void collectSequentialTransitions(ExtractContext& ctx, SequentialDesignModel& model) {
   // Record enough pin information to reconstruct Q' after the combinational
   // Boolean expressions have been built.
@@ -3179,6 +3273,7 @@ void collectSequentialTransitions(ExtractContext& ctx, SequentialDesignModel& mo
     }
     appendPendingTransitionsForInstance(ctx, model, *scan);
   }
+  harvestInitialStateValues(ctx, model);
 }
 
 std::vector<naja::DNL::DNLID> collectInitialObservedTerms(const ExtractContext& ctx) {
diff --git a/test/sec/SequentialEquivalenceStrategyTests.cpp b/test/sec/SequentialEquivalenceStrategyTests.cpp
index 08e4f6e9..24fbc7c9 100644
--- a/test/sec/SequentialEquivalenceStrategyTests.cpp
+++ b/test/sec/SequentialEquivalenceStrategyTests.cpp
@@ -37,6 +37,8 @@
 #include "SNLBusTerm.h"
 #include "SNLBusTermBit.h"
 #include "SNLInstance.h"
+#include "SNLInstParameter.h"
+#include "SNLParameter.h"
 #include "SNLScalarNet.h"
 #include "SNLScalarTerm.h"
 #include "common/AlignedSignals.h"
@@ -15896,6 +15898,217 @@ TEST_F(SequentialEquivalenceStrategyTests,
   EXPECT_TRUE(model.initialStateValueByKey.empty());
 }
 
+TEST_F(SequentialEquivalenceStrategyTests,
+       SequentialDesignModelExtractHarvestsDFFInitParameter) {
+  NLUniverse::create();
+  auto* db = NLDB::create(NLUniverse::get());
+  auto* primitives =
+      NLLibrary::create(db, NLLibrary::Type::Primitives, NLName("prims"));
+  auto* library =
+      NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs"));
+  auto* invModel = createInvModel(primitives);
+  auto* top = createDffTop(library, "top", invModel, false, false);
+  auto* ff = top->getInstance(NLName("ff0"));
+  ASSERT_NE(ff, nullptr);
+  auto* initParam = ff->getModel()->getParameter(NLName("INIT"));
+  ASSERT_NE(initParam, nullptr);
+  SNLInstParameter::create(ff, initParam, "1'b1");
+
+  const auto extracted = SequentialDesignModel::extract(top);
+
+  EXPECT_FALSE(extracted.hasUnsupportedFeatures());
+  ASSERT_EQ(extracted.initialStateValueByKey.size(), 1u);
+  EXPECT_TRUE(extracted.initialStateValueByKey.begin()->second);
+}
+
+TEST_F(SequentialEquivalenceStrategyTests,
+       SequentialDesignModelExtractHarvestsDFFInitParameterZero) {
+  NLUniverse::create();
+  auto* db = NLDB::create(NLUniverse::get());
+  auto* primitives =
+      NLLibrary::create(db, NLLibrary::Type::Primitives, NLName("prims"));
+  auto* library =
+      NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs"));
+  auto* invModel = createInvModel(primitives);
+  auto* top = createDffTop(library, "top", invModel, false, false);
+  auto* ff = top->getInstance(NLName("ff0"));
+  ASSERT_NE(ff, nullptr);
+  auto* initParam = ff->getModel()->getParameter(NLName("INIT"));
+  ASSERT_NE(initParam, nullptr);
+  SNLInstParameter::create(ff, initParam, "1'b0");
+
+  const auto extracted = SequentialDesignModel::extract(top);
+
+  EXPECT_FALSE(extracted.hasUnsupportedFeatures());
+  ASSERT_EQ(extracted.initialStateValueByKey.size(), 1u);
+  EXPECT_FALSE(extracted.initialStateValueByKey.begin()->second);
+}
+
+TEST_F(SequentialEquivalenceStrategyTests,
+       SequentialDesignModelExtractLeavesUnknownDFFInitUnconstrained) {
+  NLUniverse::create();
+  auto* db = NLDB::create(NLUniverse::get());
+  auto* primitives =
+      NLLibrary::create(db, NLLibrary::Type::Primitives, NLName("prims"));
+  auto* library =
+      NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs"));
+  auto* invModel = createInvModel(primitives);
+  auto* top = createDffTop(library, "top", invModel, false, false);
+  auto* ff = top->getInstance(NLName("ff0"));
+  ASSERT_NE(ff, nullptr);
+  auto* initParam = ff->getModel()->getParameter(NLName("INIT"));
+  ASSERT_NE(initParam, nullptr);
+  // An explicit all-x INIT (the NLDB0 default) must not constrain the state.
+  SNLInstParameter::create(ff, initParam, "1'bx");
+
+  const auto extracted = SequentialDesignModel::extract(top);
+
+  EXPECT_FALSE(extracted.hasUnsupportedFeatures());
+  EXPECT_TRUE(extracted.initialStateValueByKey.empty());
+}
+
+TEST_F(SequentialEquivalenceStrategyTests,
+       SequentialDesignModelExtractHarvestsWideDFFInitParameter) {
+  NLUniverse::create();
+  auto* db = NLDB::create(NLUniverse::get());
+  auto* library =
+      NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs"));
+  auto* top =
+      SNLDesign::create(library, SNLDesign::Type::Standard, NLName("top"));
+  auto* topIn = SNLBusTerm::create(
+      top, SNLTerm::Direction::Input, 3, 0, NLName("in"));
+  auto* topClock = SNLScalarTerm::create(
+      top, SNLTerm::Direction::Input, NLName("clk"));
+  auto* topOut = SNLBusTerm::create(
+      top, SNLTerm::Direction::Output, 3, 0, NLName("out"));
+
+  auto* dffModel = NLDB0::getOrCreateDFF(4);
+  ASSERT_NE(dffModel, nullptr);
+  auto* ff = SNLInstance::create(top, dffModel, NLName("ff0"));
+  auto* netIn = SNLBusNet::create(top, 3, 0, NLName("net_in"));
+  auto* netClock = SNLScalarNet::create(top, NLName("net_clk"));
+  auto* netQ = SNLBusNet::create(top, 3, 0, NLName("net_q"));
+
+  auto* dataTerm = dffModel->getBusTerm(NLName("D"));
+  auto* outputTerm = dffModel->getBusTerm(NLName("Q"));
+  ASSERT_NE(dataTerm, nullptr);
+  ASSERT_NE(outputTerm, nullptr);
+  topClock->setNet(netClock);
+  ff->getInstTerm(dffModel->getScalarTerm(NLName("C")))->setNet(netClock);
+  for (int bit = 0; bit <= 3; ++bit) {
+    topIn->getBit(bit)->setNet(netIn->getBit(bit));
+    ff->getInstTerm(dataTerm->getBit(bit))->setNet(netIn->getBit(bit));
+    ff->getInstTerm(outputTerm->getBit(bit))->setNet(netQ->getBit(bit));
+    topOut->getBit(bit)->setNet(netQ->getBit(bit));
+  }
+  auto* initParam = dffModel->getParameter(NLName("INIT"));
+  ASSERT_NE(initParam, nullptr);
+  // INIT digits are MSB first: bit3=0, bit2=1, bit1=x (unconstrained), bit0=0.
+  SNLInstParameter::create(ff, initParam, "4'b01x0");
+
+  const auto extracted = SequentialDesignModel::extract(top);
+
+  EXPECT_FALSE(extracted.hasUnsupportedFeatures());
+  ASSERT_EQ(extracted.stateBits.size(), 4u);
+  EXPECT_EQ(extracted.initialStateValueByKey.size(), 3u);
+  EXPECT_FALSE(extracted.initialStateValueByKey.at(
+      findKeyByDisplayName(extracted, "ff0.Q[3]")));
+  EXPECT_TRUE(extracted.initialStateValueByKey.at(
+      findKeyByDisplayName(extracted, "ff0.Q[2]")));
+  EXPECT_EQ(
+      extracted.initialStateValueByKey.find(
+          findKeyByDisplayName(extracted, "ff0.Q[1]")),
+      extracted.initialStateValueByKey.end());
+  EXPECT_FALSE(extracted.initialStateValueByKey.at(
+      findKeyByDisplayName(extracted, "ff0.Q[0]")));
+}
+
+TEST_F(SequentialEquivalenceStrategyTests,
+       SequentialDesignModelExtractHarvestsComplementedDFFInitParameter) {
+  NLUniverse::create();
+  auto* db = NLDB::create(NLUniverse::get());
+  auto* primitives =
+      NLLibrary::create(db, NLLibrary::Type::Primitives, NLName("prims"));
+  auto* library =
+      NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs"));
+  auto* model = createNamedComplementSequentialModel(
+      primitives, "DFF_Q_QN_INIT", "Q", "QN");
+  SNLParameter::create(
+      model, NLName("INIT"), SNLParameter::Type::Binary, "1'bx");
+  auto* top = createSequentialOutputPairTop(library, "top", model, "Q", "QN");
+  auto* ff = top->getInstance(NLName("ff0"));
+  ASSERT_NE(ff, nullptr);
+  SNLInstParameter::create(
+      ff, model->getParameter(NLName("INIT")), "1'b1");
+
+  const auto extracted = SequentialDesignModel::extract(top);
+
+  EXPECT_FALSE(extracted.hasUnsupportedFeatures());
+  ASSERT_EQ(extracted.complementedStateRelations.size(), 1u);
+  // State keys hold values in their own pin polarity: the Q key stores the
+  // INIT digit, the QN key stores its complement.
+  const auto primaryKey = findKeyByDisplayName(extracted, "ff0.Q[0]");
+  const auto complementKey = findKeyByDisplayName(extracted, "ff0.QN[0]");
+  ASSERT_EQ(extracted.initialStateValueByKey.size(), 2u);
+  EXPECT_TRUE(extracted.initialStateValueByKey.at(primaryKey));
+  EXPECT_FALSE(extracted.initialStateValueByKey.at(complementKey));
+}
+
+TEST_F(SequentialEquivalenceStrategyTests,
+       SequentialDesignModelExtractHarvestsSlangInitialBlock) {
+  NLUniverse::create();
+  auto* db = NLDB::create(NLUniverse::get());
+  auto* library =
+      NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs"));
+  auto* top = loadSystemVerilogTopFromSource(
+      library,
+      "sec_slang_initial_block",
+      R"(module sec_slang_initial_block(
+  input  logic clk,
+  input  logic d,
+  output logic q
+);
+  logic r;
+  initial r = 1'b1;
+  always_ff @(posedge clk) r <= d;
+  assign q = r;
+endmodule
+)");
+
+  const auto extracted = SequentialDesignModel::extract(top);
+
+  EXPECT_FALSE(extracted.hasUnsupportedFeatures());
+  ASSERT_EQ(extracted.initialStateValueByKey.size(), 1u);
+  EXPECT_TRUE(extracted.initialStateValueByKey.begin()->second);
+}
+
+TEST_F(SequentialEquivalenceStrategyTests,
+       SequentialDesignModelExtractHarvestsSlangDeclarationInitializer) {
+  NLUniverse::create();
+  auto* db = NLDB::create(NLUniverse::get());
+  auto* library =
+      NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs"));
+  auto* top = loadSystemVerilogTopFromSource(
+      library,
+      "sec_slang_decl_init",
+      R"(module sec_slang_decl_init(
+  input  logic clk,
+  input  logic d,
+  output logic q
+);
+  logic r = 1'b0;
+  always_ff @(posedge clk) r <= d;
+  assign q = r;
+endmodule
+)");
+
+  const auto extracted = SequentialDesignModel::extract(top);
+
+  EXPECT_FALSE(extracted.hasUnsupportedFeatures());
+  ASSERT_EQ(extracted.initialStateValueByKey.size(), 1u);
+  EXPECT_FALSE(extracted.initialStateValueByKey.begin()->second);
+}
+
 TEST_F(SequentialEquivalenceStrategyTests,
        SequentialDesignModelExtractSupportsGenericComplementedStateNames) {
   NLUniverse::create();

From 419f2b5d94adc100db48a86be3cc5da57e8c6938 Mon Sep 17 00:00:00 2001
From: Emin <me@emin.chat>
Date: Tue, 22 Sep 2026 12:29:32 +0800
Subject: [PATCH 02/14] Accept all sized Verilog literal bases in DFF INIT
 parsing

---
 src/sec/model/SequentialDesignModel.cpp       | 132 ++++++++++++++----
 .../SequentialEquivalenceStrategyTests.cpp    |  79 +++++++++++
 2 files changed, 185 insertions(+), 26 deletions(-)

diff --git a/src/sec/model/SequentialDesignModel.cpp b/src/sec/model/SequentialDesignModel.cpp
index 9cad5965..4d636301 100644
--- a/src/sec/model/SequentialDesignModel.cpp
+++ b/src/sec/model/SequentialDesignModel.cpp
@@ -3161,6 +3161,102 @@ void appendPendingTransitionsForInstance(
   }
 }
 
+// Expands a sized Verilog literal ("<width>'<base><digits>", base b/d/o/h)
+// into width digit chars indexed LSB first ('0','1','x','z'). Shorter digit
+// strings are extended per Verilog rules: with 'x'/'z' when the leftmost
+// digit is x/z, with '0' otherwise; longer strings lose their upper bits.
+std::optional<std::string> expandSizedLiteralDigits(const std::string& value) {
+  const auto basePos = value.find('\'');
+  if (basePos == std::string::npos || basePos + 2 >= value.size()) {
+    return std::nullopt;  // LCOV_EXCL_LINE
+  }
+  size_t width = 0;
+  try {
+    width = std::stoul(value.substr(0, basePos));
+  } catch (...) {
+    return std::nullopt;  // LCOV_EXCL_LINE
+  }
+  if (width == 0) {
+    return std::nullopt;  // LCOV_EXCL_LINE
+  }
+  const char base =
+      static_cast<char>(std::tolower(static_cast<unsigned char>(value[basePos + 1])));
+  const std::string digits = value.substr(basePos + 2);
+  if (digits.empty()) {
+    return std::nullopt;  // LCOV_EXCL_LINE
+  }
+  std::string bits;  // LSB first
+  switch (base) {
+    case 'b':
+      for (auto it = digits.rbegin(); it != digits.rend(); ++it) {
+        bits.push_back(
+            static_cast<char>(std::tolower(static_cast<unsigned char>(*it))));
+      }
+      break;
+    case 'o':
+    case 'h': {
+      const size_t bitsPerDigit = base == 'h' ? 4 : 3;
+      for (auto it = digits.rbegin(); it != digits.rend(); ++it) {
+        const char digit =
+            static_cast<char>(std::tolower(static_cast<unsigned char>(*it)));
+        if (digit == 'x' || digit == 'z') {
+          bits.append(bitsPerDigit, digit);
+          continue;
+        }
+        int digitValue = -1;
+        if (digit >= '0' && digit <= '9') {
+          digitValue = digit - '0';
+        } else if (base == 'h' && digit >= 'a' && digit <= 'f') {
+          digitValue = 10 + digit - 'a';
+        }
+        if (digitValue < 0 || digitValue >= (1 << bitsPerDigit)) {
+          return std::nullopt;  // LCOV_EXCL_LINE
+        }
+        for (size_t i = 0; i < bitsPerDigit; ++i) {
+          bits.push_back((digitValue >> i) & 1 ? '1' : '0');
+        }
+      }
+      break;
+    }
+    case 'd': {
+      std::string remaining = digits;
+      for (char c : remaining) {
+        if (!std::isdigit(static_cast<unsigned char>(c))) {
+          return std::nullopt;  // LCOV_EXCL_LINE
+        }
+      }
+      bits.assign(width, '0');
+      for (size_t i = 0; i < width && remaining != "0"; ++i) {
+        int carry = 0;
+        std::string quotient;
+        for (char c : remaining) {
+          const int current = carry * 10 + (c - '0');
+          carry = current % 2;
+          if (!quotient.empty() || current >= 2) {
+            quotient.push_back(static_cast<char>('0' + current / 2));
+          }
+        }
+        bits[i] = carry ? '1' : '0';
+        remaining = quotient.empty() ? "0" : quotient;
+      }
+      break;
+    }
+    default:
+      return std::nullopt;  // LCOV_EXCL_LINE
+  }
+  if (base != 'd') {
+    const char front =
+        static_cast<char>(std::tolower(static_cast<unsigned char>(digits.front())));
+    const char pad = front == 'x' || front == 'z' ? front : '0';
+    if (bits.size() < width) {
+      bits.append(width - bits.size(), pad);
+    } else if (bits.size() > width) {
+      bits.resize(width);
+    }
+  }
+  return bits;
+}
+
 // Reads the DFF INIT instance parameter (written by the slang frontend when a
 // constant initial block or declaration initializer sets a register's
 // power-on value) for the given state output terminal. Returns the stored
@@ -3180,41 +3276,25 @@ std::optional<bool> readDFFInitDigitForStateTerm(
   if (initParam == nullptr) {
     return std::nullopt;
   }
-  const std::string value = initParam->getValue();
-  const auto basePos = value.find('\'');
-  if (basePos == std::string::npos || basePos + 2 >= value.size()) {
-    return std::nullopt;  // LCOV_EXCL_LINE
-  }
-  if (value[basePos + 1] != 'b' && value[basePos + 1] != 'B') {
+  const auto digits = expandSizedLiteralDigits(initParam->getValue());
+  if (!digits.has_value()) {
     return std::nullopt;  // LCOV_EXCL_LINE
   }
-  size_t width = 0;
-  try {
-    width = std::stoul(value.substr(0, basePos));
-  } catch (...) {
-    return std::nullopt;  // LCOV_EXCL_LINE
-  }
-  const std::string digits = value.substr(basePos + 2);
-  if (width == 0 || digits.size() != width) {
-    return std::nullopt;  // LCOV_EXCL_LINE
-  }
-  // INIT digits are written MSB first (NLDB0::formatDFFInitValue), so the
-  // digit for bus bit b of a Q[msb:lsb] output sits at index msb-b.
-  size_t digitIndex = 0;
+  // Bit 0 of the literal is the LSB of the Q[msb:lsb] output.
+  size_t bitIndex = 0;
   const auto* bitTerm = term.getSnlBitTerm();
   if (const auto* busBit =
           dynamic_cast<const naja::NL::SNLBusTermBit*>(bitTerm)) {
-    const auto* bus = busBit->getBus();
-    const auto offset =
-        static_cast<int64_t>(bus->getMSB()) - busBit->getBit();
-    if (offset < 0 || static_cast<size_t>(offset) >= width) {
+    const auto offset = static_cast<int64_t>(busBit->getBit()) -
+                        busBit->getBus()->getLSB();
+    if (offset < 0 || static_cast<size_t>(offset) >= digits->size()) {
       return std::nullopt;  // LCOV_EXCL_LINE
     }
-    digitIndex = static_cast<size_t>(offset);
-  } else if (width != 1) {
+    bitIndex = static_cast<size_t>(offset);
+  } else if (digits->size() != 1) {
     return std::nullopt;  // LCOV_EXCL_LINE
   }
-  switch (std::tolower(static_cast<unsigned char>(digits[digitIndex]))) {
+  switch (digits->at(bitIndex)) {
     case '0':
       return false;
     case '1':
diff --git a/test/sec/SequentialEquivalenceStrategyTests.cpp b/test/sec/SequentialEquivalenceStrategyTests.cpp
index 24fbc7c9..a2ca21c7 100644
--- a/test/sec/SequentialEquivalenceStrategyTests.cpp
+++ b/test/sec/SequentialEquivalenceStrategyTests.cpp
@@ -16023,6 +16023,85 @@ TEST_F(SequentialEquivalenceStrategyTests,
       findKeyByDisplayName(extracted, "ff0.Q[0]")));
 }
 
+TEST_F(SequentialEquivalenceStrategyTests,
+       SequentialDesignModelExtractExpandsNonBinaryDFFInitLiterals) {
+  NLUniverse::create();
+  auto* db = NLDB::create(NLUniverse::get());
+  auto* library =
+      NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs"));
+
+  int designCounter = 0;
+  auto extractWideDFFInit = [&](const char* initValue) {
+    auto* top = SNLDesign::create(
+        library,
+        SNLDesign::Type::Standard,
+        NLName("top" + std::to_string(designCounter++)));
+    auto* topIn = SNLBusTerm::create(
+        top, SNLTerm::Direction::Input, 3, 0, NLName("in"));
+    auto* topClock = SNLScalarTerm::create(
+        top, SNLTerm::Direction::Input, NLName("clk"));
+    auto* topOut = SNLBusTerm::create(
+        top, SNLTerm::Direction::Output, 3, 0, NLName("out"));
+    auto* dffModel = NLDB0::getOrCreateDFF(4);
+    auto* ff = SNLInstance::create(top, dffModel, NLName("ff0"));
+    auto* netIn = SNLBusNet::create(top, 3, 0, NLName("net_in"));
+    auto* netClock = SNLScalarNet::create(top, NLName("net_clk"));
+    auto* netQ = SNLBusNet::create(top, 3, 0, NLName("net_q"));
+    auto* dataTerm = dffModel->getBusTerm(NLName("D"));
+    auto* outputTerm = dffModel->getBusTerm(NLName("Q"));
+    topClock->setNet(netClock);
+    ff->getInstTerm(dffModel->getScalarTerm(NLName("C")))->setNet(netClock);
+    for (int bit = 0; bit <= 3; ++bit) {
+      topIn->getBit(bit)->setNet(netIn->getBit(bit));
+      ff->getInstTerm(dataTerm->getBit(bit))->setNet(netIn->getBit(bit));
+      ff->getInstTerm(outputTerm->getBit(bit))->setNet(netQ->getBit(bit));
+      topOut->getBit(bit)->setNet(netQ->getBit(bit));
+    }
+    SNLInstParameter::create(
+        ff, dffModel->getParameter(NLName("INIT")), initValue);
+    return SequentialDesignModel::extract(top);
+  };
+
+  // Hex digits expand to four bits each: 4'h6 = 4'b0110.
+  const auto hexModel = extractWideDFFInit("4'h6");
+  EXPECT_FALSE(hexModel.hasUnsupportedFeatures());
+  ASSERT_EQ(hexModel.initialStateValueByKey.size(), 4u);
+  EXPECT_FALSE(hexModel.initialStateValueByKey.at(
+      findKeyByDisplayName(hexModel, "ff0.Q[3]")));
+  EXPECT_TRUE(hexModel.initialStateValueByKey.at(
+      findKeyByDisplayName(hexModel, "ff0.Q[2]")));
+  EXPECT_TRUE(hexModel.initialStateValueByKey.at(
+      findKeyByDisplayName(hexModel, "ff0.Q[1]")));
+  EXPECT_FALSE(hexModel.initialStateValueByKey.at(
+      findKeyByDisplayName(hexModel, "ff0.Q[0]")));
+
+  // Short binary literals zero-extend: 4'b1 = 4'b0001.
+  const auto shortModel = extractWideDFFInit("4'b1");
+  EXPECT_FALSE(shortModel.hasUnsupportedFeatures());
+  ASSERT_EQ(shortModel.initialStateValueByKey.size(), 4u);
+  EXPECT_FALSE(shortModel.initialStateValueByKey.at(
+      findKeyByDisplayName(shortModel, "ff0.Q[3]")));
+  EXPECT_FALSE(shortModel.initialStateValueByKey.at(
+      findKeyByDisplayName(shortModel, "ff0.Q[2]")));
+  EXPECT_FALSE(shortModel.initialStateValueByKey.at(
+      findKeyByDisplayName(shortModel, "ff0.Q[1]")));
+  EXPECT_TRUE(shortModel.initialStateValueByKey.at(
+      findKeyByDisplayName(shortModel, "ff0.Q[0]")));
+
+  // Decimal literals convert to bits: 4'd5 = 4'b0101.
+  const auto decimalModel = extractWideDFFInit("4'd5");
+  EXPECT_FALSE(decimalModel.hasUnsupportedFeatures());
+  ASSERT_EQ(decimalModel.initialStateValueByKey.size(), 4u);
+  EXPECT_FALSE(decimalModel.initialStateValueByKey.at(
+      findKeyByDisplayName(decimalModel, "ff0.Q[3]")));
+  EXPECT_TRUE(decimalModel.initialStateValueByKey.at(
+      findKeyByDisplayName(decimalModel, "ff0.Q[2]")));
+  EXPECT_FALSE(decimalModel.initialStateValueByKey.at(
+      findKeyByDisplayName(decimalModel, "ff0.Q[1]")));
+  EXPECT_TRUE(decimalModel.initialStateValueByKey.at(
+      findKeyByDisplayName(decimalModel, "ff0.Q[0]")));
+}
+
 TEST_F(SequentialEquivalenceStrategyTests,
        SequentialDesignModelExtractHarvestsComplementedDFFInitParameter) {
   NLUniverse::create();

From 5459cda33a489b11520a33747e414e9730445540 Mon Sep 17 00:00:00 2001
From: Emin <me@emin.chat>
Date: Tue, 22 Sep 2026 12:35:17 +0800
Subject: [PATCH 03/14] Ignore INIT digit separators and cache expanded
 literals per instance

---
 src/sec/model/SequentialDesignModel.cpp       | 40 +++++++++++++------
 .../SequentialEquivalenceStrategyTests.cpp    | 26 ++++++++++++
 2 files changed, 54 insertions(+), 12 deletions(-)

diff --git a/src/sec/model/SequentialDesignModel.cpp b/src/sec/model/SequentialDesignModel.cpp
index 4d636301..8d13afb7 100644
--- a/src/sec/model/SequentialDesignModel.cpp
+++ b/src/sec/model/SequentialDesignModel.cpp
@@ -3162,9 +3162,10 @@ void appendPendingTransitionsForInstance(
 }
 
 // Expands a sized Verilog literal ("<width>'<base><digits>", base b/d/o/h)
-// into width digit chars indexed LSB first ('0','1','x','z'). Shorter digit
-// strings are extended per Verilog rules: with 'x'/'z' when the leftmost
-// digit is x/z, with '0' otherwise; longer strings lose their upper bits.
+// into width digit chars indexed LSB first ('0','1','x','z'). Digit
+// separators are ignored. Shorter digit strings are extended per Verilog
+// rules: with 'x'/'z' when the leftmost digit is x/z, with '0' otherwise;
+// longer strings lose their upper bits.
 std::optional<std::string> expandSizedLiteralDigits(const std::string& value) {
   const auto basePos = value.find('\'');
   if (basePos == std::string::npos || basePos + 2 >= value.size()) {
@@ -3181,7 +3182,12 @@ std::optional<std::string> expandSizedLiteralDigits(const std::string& value) {
   }
   const char base =
       static_cast<char>(std::tolower(static_cast<unsigned char>(value[basePos + 1])));
-  const std::string digits = value.substr(basePos + 2);
+  std::string digits;
+  for (const char c : value.substr(basePos + 2)) {
+    if (c != '_') {
+      digits.push_back(c);
+    }
+  }
   if (digits.empty()) {
     return std::nullopt;  // LCOV_EXCL_LINE
   }
@@ -3262,8 +3268,12 @@ std::optional<std::string> expandSizedLiteralDigits(const std::string& value) {
 // power-on value) for the given state output terminal. Returns the stored
 // digit for the terminal's bit in the storage element's own polarity, or
 // nullopt when the instance carries no explicit INIT or the digit is x/z.
+// initDigitsByInstance caches the expanded literal so a wide DFF converts it
+// once per instance instead of once per output bit.
 std::optional<bool> readDFFInitDigitForStateTerm(
-    const naja::DNL::DNLTerminalFull& term) {
+    const naja::DNL::DNLTerminalFull& term,
+    std::unordered_map<const naja::NL::SNLInstance*,
+                       std::optional<std::string>>& initDigitsByInstance) {
   if (term.isNull() || term.isTopPort()) {
     return std::nullopt;  // LCOV_EXCL_LINE
   }
@@ -3271,14 +3281,18 @@ std::optional<bool> readDFFInitDigitForStateTerm(
   if (snlInstance == nullptr) {
     return std::nullopt;  // LCOV_EXCL_LINE
   }
-  const auto* initParam =
-      snlInstance->getInstParameter(naja::NL::NLName("INIT"));
-  if (initParam == nullptr) {
-    return std::nullopt;
+  auto cached = initDigitsByInstance.find(snlInstance);
+  if (cached == initDigitsByInstance.end()) {
+    std::optional<std::string> expanded;
+    if (const auto* initParam =
+            snlInstance->getInstParameter(naja::NL::NLName("INIT"))) {
+      expanded = expandSizedLiteralDigits(initParam->getValue());
+    }
+    cached = initDigitsByInstance.emplace(snlInstance, std::move(expanded)).first;
   }
-  const auto digits = expandSizedLiteralDigits(initParam->getValue());
+  const auto& digits = cached->second;
   if (!digits.has_value()) {
-    return std::nullopt;  // LCOV_EXCL_LINE
+    return std::nullopt;
   }
   // Bit 0 of the literal is the LSB of the Q[msb:lsb] output.
   size_t bitIndex = 0;
@@ -3310,9 +3324,11 @@ std::optional<bool> readDFFInitDigitForStateTerm(
 // keys get the opposite value.
 void harvestInitialStateValues(ExtractContext& ctx, SequentialDesignModel& model) {
   size_t harvested = 0;
+  std::unordered_map<const naja::NL::SNLInstance*, std::optional<std::string>>
+      initDigitsByInstance;
   for (const auto& pending : ctx.pendingTransitions) {
     const auto& term = ctx.dnl->getDNLTerminalFromID(pending.stateTermID);
-    const auto digit = readDFFInitDigitForStateTerm(term);
+    const auto digit = readDFFInitDigitForStateTerm(term, initDigitsByInstance);
     if (!digit.has_value()) {
       continue;
     }
diff --git a/test/sec/SequentialEquivalenceStrategyTests.cpp b/test/sec/SequentialEquivalenceStrategyTests.cpp
index a2ca21c7..a13c0698 100644
--- a/test/sec/SequentialEquivalenceStrategyTests.cpp
+++ b/test/sec/SequentialEquivalenceStrategyTests.cpp
@@ -16100,6 +16100,32 @@ TEST_F(SequentialEquivalenceStrategyTests,
       findKeyByDisplayName(decimalModel, "ff0.Q[1]")));
   EXPECT_TRUE(decimalModel.initialStateValueByKey.at(
       findKeyByDisplayName(decimalModel, "ff0.Q[0]")));
+
+  // Digit separators are ignored: 4'b1_010 = 4'b1010.
+  const auto separatedModel = extractWideDFFInit("4'b1_010");
+  EXPECT_FALSE(separatedModel.hasUnsupportedFeatures());
+  ASSERT_EQ(separatedModel.initialStateValueByKey.size(), 4u);
+  EXPECT_TRUE(separatedModel.initialStateValueByKey.at(
+      findKeyByDisplayName(separatedModel, "ff0.Q[3]")));
+  EXPECT_FALSE(separatedModel.initialStateValueByKey.at(
+      findKeyByDisplayName(separatedModel, "ff0.Q[2]")));
+  EXPECT_TRUE(separatedModel.initialStateValueByKey.at(
+      findKeyByDisplayName(separatedModel, "ff0.Q[1]")));
+  EXPECT_FALSE(separatedModel.initialStateValueByKey.at(
+      findKeyByDisplayName(separatedModel, "ff0.Q[0]")));
+
+  // Separators in decimal literals: 4'd1_0 = 10 = 4'b1010.
+  const auto separatedDecimalModel = extractWideDFFInit("4'd1_0");
+  EXPECT_FALSE(separatedDecimalModel.hasUnsupportedFeatures());
+  ASSERT_EQ(separatedDecimalModel.initialStateValueByKey.size(), 4u);
+  EXPECT_TRUE(separatedDecimalModel.initialStateValueByKey.at(
+      findKeyByDisplayName(separatedDecimalModel, "ff0.Q[3]")));
+  EXPECT_FALSE(separatedDecimalModel.initialStateValueByKey.at(
+      findKeyByDisplayName(separatedDecimalModel, "ff0.Q[2]")));
+  EXPECT_TRUE(separatedDecimalModel.initialStateValueByKey.at(
+      findKeyByDisplayName(separatedDecimalModel, "ff0.Q[1]")));
+  EXPECT_FALSE(separatedDecimalModel.initialStateValueByKey.at(
+      findKeyByDisplayName(separatedDecimalModel, "ff0.Q[0]")));
 }
 
 TEST_F(SequentialEquivalenceStrategyTests,

From 6440d6f2798be1b627d7ed91f21b24e8cb03377e Mon Sep 17 00:00:00 2001
From: Emin <me@emin.chat>
Date: Tue, 22 Sep 2026 12:46:22 +0800
Subject: [PATCH 04/14] Ignore digit separators in the INIT literal width

---
 src/sec/model/SequentialDesignModel.cpp         |  8 +++++++-
 test/sec/SequentialEquivalenceStrategyTests.cpp | 13 +++++++++++++
 2 files changed, 20 insertions(+), 1 deletion(-)

diff --git a/src/sec/model/SequentialDesignModel.cpp b/src/sec/model/SequentialDesignModel.cpp
index 8d13afb7..0733a9b4 100644
--- a/src/sec/model/SequentialDesignModel.cpp
+++ b/src/sec/model/SequentialDesignModel.cpp
@@ -3173,7 +3173,13 @@ std::optional<std::string> expandSizedLiteralDigits(const std::string& value) {
   }
   size_t width = 0;
   try {
-    width = std::stoul(value.substr(0, basePos));
+    std::string widthText;
+    for (const char c : value.substr(0, basePos)) {
+      if (c != '_') {
+        widthText.push_back(c);
+      }
+    }
+    width = std::stoul(widthText);
   } catch (...) {
     return std::nullopt;  // LCOV_EXCL_LINE
   }
diff --git a/test/sec/SequentialEquivalenceStrategyTests.cpp b/test/sec/SequentialEquivalenceStrategyTests.cpp
index a13c0698..16112b87 100644
--- a/test/sec/SequentialEquivalenceStrategyTests.cpp
+++ b/test/sec/SequentialEquivalenceStrategyTests.cpp
@@ -16126,6 +16126,19 @@ TEST_F(SequentialEquivalenceStrategyTests,
       findKeyByDisplayName(separatedDecimalModel, "ff0.Q[1]")));
   EXPECT_FALSE(separatedDecimalModel.initialStateValueByKey.at(
       findKeyByDisplayName(separatedDecimalModel, "ff0.Q[0]")));
+
+  // Separators in the width field are ignored too: 0_4'h6 = 4'b0110.
+  const auto separatedWidthModel = extractWideDFFInit("0_4'h6");
+  EXPECT_FALSE(separatedWidthModel.hasUnsupportedFeatures());
+  ASSERT_EQ(separatedWidthModel.initialStateValueByKey.size(), 4u);
+  EXPECT_FALSE(separatedWidthModel.initialStateValueByKey.at(
+      findKeyByDisplayName(separatedWidthModel, "ff0.Q[3]")));
+  EXPECT_TRUE(separatedWidthModel.initialStateValueByKey.at(
+      findKeyByDisplayName(separatedWidthModel, "ff0.Q[2]")));
+  EXPECT_TRUE(separatedWidthModel.initialStateValueByKey.at(
+      findKeyByDisplayName(separatedWidthModel, "ff0.Q[1]")));
+  EXPECT_FALSE(separatedWidthModel.initialStateValueByKey.at(
+      findKeyByDisplayName(separatedWidthModel, "ff0.Q[0]")));
 }
 
 TEST_F(SequentialEquivalenceStrategyTests,

From e53f5e465ef9beb376822ea7124a3763e83d47ce Mon Sep 17 00:00:00 2001
From: Emin <me@emin.chat>
Date: Tue, 22 Sep 2026 12:59:16 +0800
Subject: [PATCH 05/14] Document SystemVerilog initial value support in SEC

---
 docs/systemverilog/README.md | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/docs/systemverilog/README.md b/docs/systemverilog/README.md
index b17cfe4f..fbd314f6 100644
--- a/docs/systemverilog/README.md
+++ b/docs/systemverilog/README.md
@@ -58,6 +58,30 @@ build/src/bin/kepler-formal -sv2v -v sec \
 
 The preprocessing flag is spelled `--verilog_preprocessing`.
 
+## Initial values
+
+The slang frontend lowers constant register initialization to DFF `INIT`
+metadata, and SEC extraction adopts it as an exact initial-state constraint:
+
+- `initial q = 1'b0;` — an initial block holding a single blocking constant
+  assignment to a register
+- `logic q = 1'b0;` — a declaration initializer (semantically an implicit
+  initial block)
+
+`x`/`z` digits leave the corresponding state bit unconstrained. Registers
+without an explicit initializer keep a free initial state, so designs that
+initialize state through a reset sequence still need
+[sec-reset-bootstrap](../sec-reset-bootstrap.md).
+
+Limitations:
+
+- Initial blocks with multiple statements, non-blocking assignments, or
+  non-constant right-hand sides are rejected by the frontend at load time.
+- Memory initialization (`$readmemh`/`$readmemb`, memory `INIT` parameters) is
+  not adopted by SEC extraction yet.
+- The `-verilog` flow uses a structural Verilog parser and does not process
+  initial blocks; use `-systemverilog`/`-sv` for designs that rely on them.
+
 ## Flist mode
 
 For SystemVerilog designs that are already driven by a slang command file or flist, use:

From b0bca7ed78b425aa0bc30158048acc6ed5795f7e Mon Sep 17 00:00:00 2001
From: Emin <me@emin.chat>
Date: Tue, 22 Sep 2026 13:12:41 +0800
Subject: [PATCH 06/14] Clarify sv2v initial value support is design-1 only

---
 docs/systemverilog/README.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/docs/systemverilog/README.md b/docs/systemverilog/README.md
index fbd314f6..ecc876e7 100644
--- a/docs/systemverilog/README.md
+++ b/docs/systemverilog/README.md
@@ -81,6 +81,8 @@ Limitations:
   not adopted by SEC extraction yet.
 - The `-verilog` flow uses a structural Verilog parser and does not process
   initial blocks; use `-systemverilog`/`-sv` for designs that rely on them.
+  In `-sv2v` comparisons, design 1 is parsed by the slang frontend and supports
+  these initializers, while design 2 (Verilog) does not.
 
 ## Flist mode
 

From 4e20357fe95dfd5f9f13b20a1697e1925afa7afd Mon Sep 17 00:00:00 2001
From: Emin <me@emin.chat>
Date: Tue, 22 Sep 2026 15:00:59 +0800
Subject: [PATCH 07/14] Accept signed and negative DFF INIT literals

---
 src/sec/model/SequentialDesignModel.cpp       | 43 ++++++++++++++++---
 .../SequentialEquivalenceStrategyTests.cpp    | 26 +++++++++++
 2 files changed, 62 insertions(+), 7 deletions(-)

diff --git a/src/sec/model/SequentialDesignModel.cpp b/src/sec/model/SequentialDesignModel.cpp
index 0733a9b4..1f07b98c 100644
--- a/src/sec/model/SequentialDesignModel.cpp
+++ b/src/sec/model/SequentialDesignModel.cpp
@@ -3161,21 +3161,24 @@ void appendPendingTransitionsForInstance(
   }
 }
 
-// Expands a sized Verilog literal ("<width>'<base><digits>", base b/d/o/h)
-// into width digit chars indexed LSB first ('0','1','x','z'). Digit
+// Expands a sized Verilog literal ("[-]<width>'[s]<base><digits>", base
+// b/d/o/h) into width digit chars indexed LSB first ('0','1','x','z'). Digit
 // separators are ignored. Shorter digit strings are extended per Verilog
 // rules: with 'x'/'z' when the leftmost digit is x/z, with '0' otherwise;
-// longer strings lose their upper bits.
+// longer strings lose their upper bits. Negative literals are converted to
+// two's complement; the signed marker only affects that decimal value.
 std::optional<std::string> expandSizedLiteralDigits(const std::string& value) {
   const auto basePos = value.find('\'');
   if (basePos == std::string::npos || basePos + 2 >= value.size()) {
     return std::nullopt;  // LCOV_EXCL_LINE
   }
+  const std::string widthField = value.substr(0, basePos);
+  const bool negative = widthField.find('-') != std::string::npos;
   size_t width = 0;
   try {
     std::string widthText;
-    for (const char c : value.substr(0, basePos)) {
-      if (c != '_') {
+    for (const char c : widthField) {
+      if (c != '_' && c != '-') {
         widthText.push_back(c);
       }
     }
@@ -3186,10 +3189,17 @@ std::optional<std::string> expandSizedLiteralDigits(const std::string& value) {
   if (width == 0) {
     return std::nullopt;  // LCOV_EXCL_LINE
   }
+  size_t baseIndex = basePos + 1;
+  if (value[baseIndex] == 's' || value[baseIndex] == 'S') {
+    ++baseIndex;  // signed marker: bits are unchanged, only interpretation
+  }
+  if (baseIndex >= value.size()) {
+    return std::nullopt;  // LCOV_EXCL_LINE
+  }
   const char base =
-      static_cast<char>(std::tolower(static_cast<unsigned char>(value[basePos + 1])));
+      static_cast<char>(std::tolower(static_cast<unsigned char>(value[baseIndex])));
   std::string digits;
-  for (const char c : value.substr(basePos + 2)) {
+  for (const char c : value.substr(baseIndex + 1)) {
     if (c != '_') {
       digits.push_back(c);
     }
@@ -3266,6 +3276,25 @@ std::optional<std::string> expandSizedLiteralDigits(const std::string& value) {
       bits.resize(width);
     }
   }
+  if (negative) {
+    // Two's complement: invert every bit, then add one starting from the LSB.
+    for (auto& c : bits) {
+      if (c == '0') {
+        c = '1';
+      } else if (c == '1') {
+        c = '0';
+      }
+    }
+    bool carry = true;
+    for (size_t i = 0; i < bits.size() && carry; ++i) {
+      if (bits[i] == '0') {
+        bits[i] = '1';
+        carry = false;
+      } else if (bits[i] == '1') {
+        bits[i] = '0';
+      }
+    }
+  }
   return bits;
 }
 
diff --git a/test/sec/SequentialEquivalenceStrategyTests.cpp b/test/sec/SequentialEquivalenceStrategyTests.cpp
index 16112b87..c8504065 100644
--- a/test/sec/SequentialEquivalenceStrategyTests.cpp
+++ b/test/sec/SequentialEquivalenceStrategyTests.cpp
@@ -16139,6 +16139,32 @@ TEST_F(SequentialEquivalenceStrategyTests,
       findKeyByDisplayName(separatedWidthModel, "ff0.Q[1]")));
   EXPECT_FALSE(separatedWidthModel.initialStateValueByKey.at(
       findKeyByDisplayName(separatedWidthModel, "ff0.Q[0]")));
+
+  // The signed marker does not change the bit pattern: 4'sh6 = 4'b0110.
+  const auto signedHexModel = extractWideDFFInit("4'sh6");
+  EXPECT_FALSE(signedHexModel.hasUnsupportedFeatures());
+  ASSERT_EQ(signedHexModel.initialStateValueByKey.size(), 4u);
+  EXPECT_FALSE(signedHexModel.initialStateValueByKey.at(
+      findKeyByDisplayName(signedHexModel, "ff0.Q[3]")));
+  EXPECT_TRUE(signedHexModel.initialStateValueByKey.at(
+      findKeyByDisplayName(signedHexModel, "ff0.Q[2]")));
+  EXPECT_TRUE(signedHexModel.initialStateValueByKey.at(
+      findKeyByDisplayName(signedHexModel, "ff0.Q[1]")));
+  EXPECT_FALSE(signedHexModel.initialStateValueByKey.at(
+      findKeyByDisplayName(signedHexModel, "ff0.Q[0]")));
+
+  // Negative decimals are stored as two's complement: -4'd3 = 4'b1101.
+  const auto negativeDecimalModel = extractWideDFFInit("-4'd3");
+  EXPECT_FALSE(negativeDecimalModel.hasUnsupportedFeatures());
+  ASSERT_EQ(negativeDecimalModel.initialStateValueByKey.size(), 4u);
+  EXPECT_TRUE(negativeDecimalModel.initialStateValueByKey.at(
+      findKeyByDisplayName(negativeDecimalModel, "ff0.Q[3]")));
+  EXPECT_TRUE(negativeDecimalModel.initialStateValueByKey.at(
+      findKeyByDisplayName(negativeDecimalModel, "ff0.Q[2]")));
+  EXPECT_FALSE(negativeDecimalModel.initialStateValueByKey.at(
+      findKeyByDisplayName(negativeDecimalModel, "ff0.Q[1]")));
+  EXPECT_TRUE(negativeDecimalModel.initialStateValueByKey.at(
+      findKeyByDisplayName(negativeDecimalModel, "ff0.Q[0]")));
 }
 
 TEST_F(SequentialEquivalenceStrategyTests,

From ae792440a03c2dd7dd4291591ef6b826ba3933ae Mon Sep 17 00:00:00 2001
From: Emin <me@emin.chat>
Date: Tue, 22 Sep 2026 15:11:53 +0800
Subject: [PATCH 08/14] Propagate unknown carry when negating INIT literals

---
 src/sec/model/SequentialDesignModel.cpp        |  8 ++++++++
 .../sec/SequentialEquivalenceStrategyTests.cpp | 18 ++++++++++++++++++
 2 files changed, 26 insertions(+)

diff --git a/src/sec/model/SequentialDesignModel.cpp b/src/sec/model/SequentialDesignModel.cpp
index 1f07b98c..646e0544 100644
--- a/src/sec/model/SequentialDesignModel.cpp
+++ b/src/sec/model/SequentialDesignModel.cpp
@@ -3292,6 +3292,14 @@ std::optional<std::string> expandSizedLiteralDigits(const std::string& value) {
         carry = false;
       } else if (bits[i] == '1') {
         bits[i] = '0';
+      } else {
+        // An unknown digit with an incoming carry makes the carry unknown, so
+        // every more-significant result bit is unknown as well.
+        bits[i] = 'x';
+        for (size_t j = i + 1; j < bits.size(); ++j) {
+          bits[j] = 'x';
+        }
+        break;
       }
     }
   }
diff --git a/test/sec/SequentialEquivalenceStrategyTests.cpp b/test/sec/SequentialEquivalenceStrategyTests.cpp
index c8504065..8e56b911 100644
--- a/test/sec/SequentialEquivalenceStrategyTests.cpp
+++ b/test/sec/SequentialEquivalenceStrategyTests.cpp
@@ -16165,6 +16165,24 @@ TEST_F(SequentialEquivalenceStrategyTests,
       findKeyByDisplayName(negativeDecimalModel, "ff0.Q[1]")));
   EXPECT_TRUE(negativeDecimalModel.initialStateValueByKey.at(
       findKeyByDisplayName(negativeDecimalModel, "ff0.Q[0]")));
+
+  // An unknown digit under the negation carry makes the carry and all higher
+  // bits unknown: -4'b0x00 = 4'bxx00, so only the low two bits constrain.
+  const auto negativeUnknownModel = extractWideDFFInit("-4'b0x00");
+  EXPECT_FALSE(negativeUnknownModel.hasUnsupportedFeatures());
+  ASSERT_EQ(negativeUnknownModel.initialStateValueByKey.size(), 2u);
+  EXPECT_EQ(
+      negativeUnknownModel.initialStateValueByKey.find(
+          findKeyByDisplayName(negativeUnknownModel, "ff0.Q[3]")),
+      negativeUnknownModel.initialStateValueByKey.end());
+  EXPECT_EQ(
+      negativeUnknownModel.initialStateValueByKey.find(
+          findKeyByDisplayName(negativeUnknownModel, "ff0.Q[2]")),
+      negativeUnknownModel.initialStateValueByKey.end());
+  EXPECT_FALSE(negativeUnknownModel.initialStateValueByKey.at(
+      findKeyByDisplayName(negativeUnknownModel, "ff0.Q[1]")));
+  EXPECT_FALSE(negativeUnknownModel.initialStateValueByKey.at(
+      findKeyByDisplayName(negativeUnknownModel, "ff0.Q[0]")));
 }
 
 TEST_F(SequentialEquivalenceStrategyTests,

From 765c4d572249e860a120a370413e1abbd2e808bf Mon Sep 17 00:00:00 2001
From: Emin <me@emin.chat>
Date: Tue, 22 Sep 2026 16:01:06 +0800
Subject: [PATCH 09/14] Sign-extend signed DFF INIT literals

---
 src/sec/model/SequentialDesignModel.cpp         | 16 +++++++++++++---
 test/sec/SequentialEquivalenceStrategyTests.cpp | 10 ++++++++++
 2 files changed, 23 insertions(+), 3 deletions(-)

diff --git a/src/sec/model/SequentialDesignModel.cpp b/src/sec/model/SequentialDesignModel.cpp
index 646e0544..455bc76c 100644
--- a/src/sec/model/SequentialDesignModel.cpp
+++ b/src/sec/model/SequentialDesignModel.cpp
@@ -3190,8 +3190,10 @@ std::optional<std::string> expandSizedLiteralDigits(const std::string& value) {
     return std::nullopt;  // LCOV_EXCL_LINE
   }
   size_t baseIndex = basePos + 1;
-  if (value[baseIndex] == 's' || value[baseIndex] == 'S') {
-    ++baseIndex;  // signed marker: bits are unchanged, only interpretation
+  const bool signedLiteral =
+      value[baseIndex] == 's' || value[baseIndex] == 'S';
+  if (signedLiteral) {
+    ++baseIndex;
   }
   if (baseIndex >= value.size()) {
     return std::nullopt;  // LCOV_EXCL_LINE
@@ -3269,7 +3271,15 @@ std::optional<std::string> expandSizedLiteralDigits(const std::string& value) {
   if (base != 'd') {
     const char front =
         static_cast<char>(std::tolower(static_cast<unsigned char>(digits.front())));
-    const char pad = front == 'x' || front == 'z' ? front : '0';
+    // Unsigned literals zero-extend; signed literals sign-extend from the MSB
+    // of the given digits (bits.back(), since bits is LSB first); a leftmost
+    // x/z digit always extends with x/z regardless of signedness.
+    char pad = '0';
+    if (front == 'x' || front == 'z') {
+      pad = front;
+    } else if (signedLiteral && !bits.empty()) {
+      pad = bits.back();
+    }
     if (bits.size() < width) {
       bits.append(width - bits.size(), pad);
     } else if (bits.size() > width) {
diff --git a/test/sec/SequentialEquivalenceStrategyTests.cpp b/test/sec/SequentialEquivalenceStrategyTests.cpp
index 8e56b911..4e4940ec 100644
--- a/test/sec/SequentialEquivalenceStrategyTests.cpp
+++ b/test/sec/SequentialEquivalenceStrategyTests.cpp
@@ -16183,6 +16183,16 @@ TEST_F(SequentialEquivalenceStrategyTests,
       findKeyByDisplayName(negativeUnknownModel, "ff0.Q[1]")));
   EXPECT_FALSE(negativeUnknownModel.initialStateValueByKey.at(
       findKeyByDisplayName(negativeUnknownModel, "ff0.Q[0]")));
+
+  // Signed literals sign-extend: 4'sb1 = 4'b1111 (contrast with 4'b1 = 0001).
+  const auto signedShortModel = extractWideDFFInit("4'sb1");
+  EXPECT_FALSE(signedShortModel.hasUnsupportedFeatures());
+  ASSERT_EQ(signedShortModel.initialStateValueByKey.size(), 4u);
+  for (int bit = 0; bit <= 3; ++bit) {
+    EXPECT_TRUE(signedShortModel.initialStateValueByKey.at(
+        findKeyByDisplayName(
+            signedShortModel, "ff0.Q[" + std::to_string(bit) + "]")));
+  }
 }
 
 TEST_F(SequentialEquivalenceStrategyTests,

From 63ea1db94c83ac753e5d326d4203b8ca722cce2a Mon Sep 17 00:00:00 2001
From: Emin <me@emin.chat>
Date: Tue, 22 Sep 2026 16:13:40 +0800
Subject: [PATCH 10/14] Keep declared-width zero extension for signed DFF INIT
 literals

---
 src/sec/model/SequentialDesignModel.cpp       | 26 +++++++------------
 .../SequentialEquivalenceStrategyTests.cpp    | 17 +++++++-----
 2 files changed, 21 insertions(+), 22 deletions(-)

diff --git a/src/sec/model/SequentialDesignModel.cpp b/src/sec/model/SequentialDesignModel.cpp
index 455bc76c..01ffbc3c 100644
--- a/src/sec/model/SequentialDesignModel.cpp
+++ b/src/sec/model/SequentialDesignModel.cpp
@@ -3163,10 +3163,11 @@ void appendPendingTransitionsForInstance(
 
 // Expands a sized Verilog literal ("[-]<width>'[s]<base><digits>", base
 // b/d/o/h) into width digit chars indexed LSB first ('0','1','x','z'). Digit
-// separators are ignored. Shorter digit strings are extended per Verilog
-// rules: with 'x'/'z' when the leftmost digit is x/z, with '0' otherwise;
-// longer strings lose their upper bits. Negative literals are converted to
-// two's complement; the signed marker only affects that decimal value.
+// separators are ignored. Shorter digit strings are zero-extended ('x'/'z'
+// extended when the leftmost digit is x/z) up to the declared width; longer
+// strings lose their upper bits. A leading '-' negates the value (two's
+// complement); the optional signed marker only governs later expression
+// context extension and does not change the literal's own bit pattern.
 std::optional<std::string> expandSizedLiteralDigits(const std::string& value) {
   const auto basePos = value.find('\'');
   if (basePos == std::string::npos || basePos + 2 >= value.size()) {
@@ -3190,9 +3191,10 @@ std::optional<std::string> expandSizedLiteralDigits(const std::string& value) {
     return std::nullopt;  // LCOV_EXCL_LINE
   }
   size_t baseIndex = basePos + 1;
-  const bool signedLiteral =
-      value[baseIndex] == 's' || value[baseIndex] == 'S';
-  if (signedLiteral) {
+  // The signed marker only affects how the value is interpreted and extended
+  // in a wider expression context; the literal's own bit pattern is fixed by
+  // the declared width, so it is accepted and ignored here.
+  if (value[baseIndex] == 's' || value[baseIndex] == 'S') {
     ++baseIndex;
   }
   if (baseIndex >= value.size()) {
@@ -3271,15 +3273,7 @@ std::optional<std::string> expandSizedLiteralDigits(const std::string& value) {
   if (base != 'd') {
     const char front =
         static_cast<char>(std::tolower(static_cast<unsigned char>(digits.front())));
-    // Unsigned literals zero-extend; signed literals sign-extend from the MSB
-    // of the given digits (bits.back(), since bits is LSB first); a leftmost
-    // x/z digit always extends with x/z regardless of signedness.
-    char pad = '0';
-    if (front == 'x' || front == 'z') {
-      pad = front;
-    } else if (signedLiteral && !bits.empty()) {
-      pad = bits.back();
-    }
+    const char pad = front == 'x' || front == 'z' ? front : '0';
     if (bits.size() < width) {
       bits.append(width - bits.size(), pad);
     } else if (bits.size() > width) {
diff --git a/test/sec/SequentialEquivalenceStrategyTests.cpp b/test/sec/SequentialEquivalenceStrategyTests.cpp
index 4e4940ec..53b62d55 100644
--- a/test/sec/SequentialEquivalenceStrategyTests.cpp
+++ b/test/sec/SequentialEquivalenceStrategyTests.cpp
@@ -16184,15 +16184,20 @@ TEST_F(SequentialEquivalenceStrategyTests,
   EXPECT_FALSE(negativeUnknownModel.initialStateValueByKey.at(
       findKeyByDisplayName(negativeUnknownModel, "ff0.Q[0]")));
 
-  // Signed literals sign-extend: 4'sb1 = 4'b1111 (contrast with 4'b1 = 0001).
+  // The signed marker does not change the literal's own bit pattern:
+  // 4'sb1 = 4'b0001 (extension is per literal width, sign extension only
+  // applies when a later context widens the value).
   const auto signedShortModel = extractWideDFFInit("4'sb1");
   EXPECT_FALSE(signedShortModel.hasUnsupportedFeatures());
   ASSERT_EQ(signedShortModel.initialStateValueByKey.size(), 4u);
-  for (int bit = 0; bit <= 3; ++bit) {
-    EXPECT_TRUE(signedShortModel.initialStateValueByKey.at(
-        findKeyByDisplayName(
-            signedShortModel, "ff0.Q[" + std::to_string(bit) + "]")));
-  }
+  EXPECT_FALSE(signedShortModel.initialStateValueByKey.at(
+      findKeyByDisplayName(signedShortModel, "ff0.Q[3]")));
+  EXPECT_FALSE(signedShortModel.initialStateValueByKey.at(
+      findKeyByDisplayName(signedShortModel, "ff0.Q[2]")));
+  EXPECT_FALSE(signedShortModel.initialStateValueByKey.at(
+      findKeyByDisplayName(signedShortModel, "ff0.Q[1]")));
+  EXPECT_TRUE(signedShortModel.initialStateValueByKey.at(
+      findKeyByDisplayName(signedShortModel, "ff0.Q[0]")));
 }
 
 TEST_F(SequentialEquivalenceStrategyTests,

From aa5057dbdf711f1ab3b030cac654a7bb9bde32ba Mon Sep 17 00:00:00 2001
From: Emin <me@emin.chat>
Date: Tue, 22 Sep 2026 16:57:45 +0800
Subject: [PATCH 11/14] Narrow SEC INIT parsing to the canonical naja parameter
 form

---
 docs/systemverilog/README.md                  |   5 +
 src/sec/model/SequentialDesignModel.cpp       | 195 +++---------------
 .../SequentialEquivalenceStrategyTests.cpp    | 183 +++++-----------
 thirdparty/naja                               |   2 +-
 4 files changed, 82 insertions(+), 303 deletions(-)

diff --git a/docs/systemverilog/README.md b/docs/systemverilog/README.md
index ecc876e7..f06fb373 100644
--- a/docs/systemverilog/README.md
+++ b/docs/systemverilog/README.md
@@ -73,6 +73,11 @@ without an explicit initializer keep a free initial state, so designs that
 initialize state through a reset sequence still need
 [sec-reset-bootstrap](../sec-reset-bootstrap.md).
 
+Sized bit-literal parameters (such as `INIT`) are stored in SNL in a canonical
+form — `<width>'b<msb...lsb>` with lowercase `0`/`1`/`x`/`z` digits — produced
+by the naja frontends at load time. SEC extraction only consumes this canonical
+form; any other string form leaves the state unconstrained.
+
 Limitations:
 
 - Initial blocks with multiple statements, non-blocking assignments, or
diff --git a/src/sec/model/SequentialDesignModel.cpp b/src/sec/model/SequentialDesignModel.cpp
index 01ffbc3c..480f2e1c 100644
--- a/src/sec/model/SequentialDesignModel.cpp
+++ b/src/sec/model/SequentialDesignModel.cpp
@@ -3161,162 +3161,12 @@ void appendPendingTransitionsForInstance(
   }
 }
 
-// Expands a sized Verilog literal ("[-]<width>'[s]<base><digits>", base
-// b/d/o/h) into width digit chars indexed LSB first ('0','1','x','z'). Digit
-// separators are ignored. Shorter digit strings are zero-extended ('x'/'z'
-// extended when the leftmost digit is x/z) up to the declared width; longer
-// strings lose their upper bits. A leading '-' negates the value (two's
-// complement); the optional signed marker only governs later expression
-// context extension and does not change the literal's own bit pattern.
-std::optional<std::string> expandSizedLiteralDigits(const std::string& value) {
-  const auto basePos = value.find('\'');
-  if (basePos == std::string::npos || basePos + 2 >= value.size()) {
-    return std::nullopt;  // LCOV_EXCL_LINE
-  }
-  const std::string widthField = value.substr(0, basePos);
-  const bool negative = widthField.find('-') != std::string::npos;
-  size_t width = 0;
-  try {
-    std::string widthText;
-    for (const char c : widthField) {
-      if (c != '_' && c != '-') {
-        widthText.push_back(c);
-      }
-    }
-    width = std::stoul(widthText);
-  } catch (...) {
-    return std::nullopt;  // LCOV_EXCL_LINE
-  }
-  if (width == 0) {
-    return std::nullopt;  // LCOV_EXCL_LINE
-  }
-  size_t baseIndex = basePos + 1;
-  // The signed marker only affects how the value is interpreted and extended
-  // in a wider expression context; the literal's own bit pattern is fixed by
-  // the declared width, so it is accepted and ignored here.
-  if (value[baseIndex] == 's' || value[baseIndex] == 'S') {
-    ++baseIndex;
-  }
-  if (baseIndex >= value.size()) {
-    return std::nullopt;  // LCOV_EXCL_LINE
-  }
-  const char base =
-      static_cast<char>(std::tolower(static_cast<unsigned char>(value[baseIndex])));
-  std::string digits;
-  for (const char c : value.substr(baseIndex + 1)) {
-    if (c != '_') {
-      digits.push_back(c);
-    }
-  }
-  if (digits.empty()) {
-    return std::nullopt;  // LCOV_EXCL_LINE
-  }
-  std::string bits;  // LSB first
-  switch (base) {
-    case 'b':
-      for (auto it = digits.rbegin(); it != digits.rend(); ++it) {
-        bits.push_back(
-            static_cast<char>(std::tolower(static_cast<unsigned char>(*it))));
-      }
-      break;
-    case 'o':
-    case 'h': {
-      const size_t bitsPerDigit = base == 'h' ? 4 : 3;
-      for (auto it = digits.rbegin(); it != digits.rend(); ++it) {
-        const char digit =
-            static_cast<char>(std::tolower(static_cast<unsigned char>(*it)));
-        if (digit == 'x' || digit == 'z') {
-          bits.append(bitsPerDigit, digit);
-          continue;
-        }
-        int digitValue = -1;
-        if (digit >= '0' && digit <= '9') {
-          digitValue = digit - '0';
-        } else if (base == 'h' && digit >= 'a' && digit <= 'f') {
-          digitValue = 10 + digit - 'a';
-        }
-        if (digitValue < 0 || digitValue >= (1 << bitsPerDigit)) {
-          return std::nullopt;  // LCOV_EXCL_LINE
-        }
-        for (size_t i = 0; i < bitsPerDigit; ++i) {
-          bits.push_back((digitValue >> i) & 1 ? '1' : '0');
-        }
-      }
-      break;
-    }
-    case 'd': {
-      std::string remaining = digits;
-      for (char c : remaining) {
-        if (!std::isdigit(static_cast<unsigned char>(c))) {
-          return std::nullopt;  // LCOV_EXCL_LINE
-        }
-      }
-      bits.assign(width, '0');
-      for (size_t i = 0; i < width && remaining != "0"; ++i) {
-        int carry = 0;
-        std::string quotient;
-        for (char c : remaining) {
-          const int current = carry * 10 + (c - '0');
-          carry = current % 2;
-          if (!quotient.empty() || current >= 2) {
-            quotient.push_back(static_cast<char>('0' + current / 2));
-          }
-        }
-        bits[i] = carry ? '1' : '0';
-        remaining = quotient.empty() ? "0" : quotient;
-      }
-      break;
-    }
-    default:
-      return std::nullopt;  // LCOV_EXCL_LINE
-  }
-  if (base != 'd') {
-    const char front =
-        static_cast<char>(std::tolower(static_cast<unsigned char>(digits.front())));
-    const char pad = front == 'x' || front == 'z' ? front : '0';
-    if (bits.size() < width) {
-      bits.append(width - bits.size(), pad);
-    } else if (bits.size() > width) {
-      bits.resize(width);
-    }
-  }
-  if (negative) {
-    // Two's complement: invert every bit, then add one starting from the LSB.
-    for (auto& c : bits) {
-      if (c == '0') {
-        c = '1';
-      } else if (c == '1') {
-        c = '0';
-      }
-    }
-    bool carry = true;
-    for (size_t i = 0; i < bits.size() && carry; ++i) {
-      if (bits[i] == '0') {
-        bits[i] = '1';
-        carry = false;
-      } else if (bits[i] == '1') {
-        bits[i] = '0';
-      } else {
-        // An unknown digit with an incoming carry makes the carry unknown, so
-        // every more-significant result bit is unknown as well.
-        bits[i] = 'x';
-        for (size_t j = i + 1; j < bits.size(); ++j) {
-          bits[j] = 'x';
-        }
-        break;
-      }
-    }
-  }
-  return bits;
-}
-
-// Reads the DFF INIT instance parameter (written by the slang frontend when a
-// constant initial block or declaration initializer sets a register's
-// power-on value) for the given state output terminal. Returns the stored
-// digit for the terminal's bit in the storage element's own polarity, or
-// nullopt when the instance carries no explicit INIT or the digit is x/z.
-// initDigitsByInstance caches the expanded literal so a wide DFF converts it
-// once per instance instead of once per output bit.
+// Reads the DFF INIT instance parameter for the given state output terminal.
+// The naja frontends store INIT in a canonical form ("<width>'b<msb...lsb>",
+// lowercase digits in 0/1/x/z); anything else leaves the state unconstrained.
+// Returns the digit for the terminal's bit in the storage element's own
+// polarity. initDigitsByInstance caches the LSB-first digit string so a wide
+// DFF converts it once per instance instead of once per output bit.
 std::optional<bool> readDFFInitDigitForStateTerm(
     const naja::DNL::DNLTerminalFull& term,
     std::unordered_map<const naja::NL::SNLInstance*,
@@ -3330,32 +3180,47 @@ std::optional<bool> readDFFInitDigitForStateTerm(
   }
   auto cached = initDigitsByInstance.find(snlInstance);
   if (cached == initDigitsByInstance.end()) {
-    std::optional<std::string> expanded;
+    std::optional<std::string> digits;
     if (const auto* initParam =
             snlInstance->getInstParameter(naja::NL::NLName("INIT"))) {
-      expanded = expandSizedLiteralDigits(initParam->getValue());
+      const std::string value = initParam->getValue();
+      const auto basePos = value.find('\'');
+      if (basePos != std::string::npos && basePos + 2 < value.size() &&
+          (value[basePos + 1] == 'b' || value[basePos + 1] == 'B')) {
+        // Flip to LSB-first so bit i sits at index i.
+        std::string reversed(value.substr(basePos + 2));
+        std::reverse(reversed.begin(), reversed.end());
+        digits = std::move(reversed);
+      }
     }
-    cached = initDigitsByInstance.emplace(snlInstance, std::move(expanded)).first;
+    cached = initDigitsByInstance.emplace(snlInstance, std::move(digits)).first;
   }
   const auto& digits = cached->second;
-  if (!digits.has_value()) {
+  if (!digits.has_value() || digits->empty()) {
     return std::nullopt;
   }
-  // Bit 0 of the literal is the LSB of the Q[msb:lsb] output.
   size_t bitIndex = 0;
   const auto* bitTerm = term.getSnlBitTerm();
   if (const auto* busBit =
           dynamic_cast<const naja::NL::SNLBusTermBit*>(bitTerm)) {
     const auto offset = static_cast<int64_t>(busBit->getBit()) -
                         busBit->getBus()->getLSB();
-    if (offset < 0 || static_cast<size_t>(offset) >= digits->size()) {
+    if (offset < 0) {
       return std::nullopt;  // LCOV_EXCL_LINE
     }
     bitIndex = static_cast<size_t>(offset);
-  } else if (digits->size() != 1) {
-    return std::nullopt;  // LCOV_EXCL_LINE
   }
-  switch (digits->at(bitIndex)) {
+  if (bitIndex >= digits->size()) {
+    // A literal narrower than the Q bus extends per Verilog rules: with zero,
+    // or with x/z when its most-significant digit is unknown.
+    const char top = static_cast<char>(
+        std::tolower(static_cast<unsigned char>(digits->back())));
+    if (top == '0' || top == '1') {
+      return false;
+    }
+    return std::nullopt;
+  }
+  switch (std::tolower(static_cast<unsigned char>(digits->at(bitIndex)))) {
     case '0':
       return false;
     case '1':
diff --git a/test/sec/SequentialEquivalenceStrategyTests.cpp b/test/sec/SequentialEquivalenceStrategyTests.cpp
index 53b62d55..297b113e 100644
--- a/test/sec/SequentialEquivalenceStrategyTests.cpp
+++ b/test/sec/SequentialEquivalenceStrategyTests.cpp
@@ -16024,7 +16024,31 @@ TEST_F(SequentialEquivalenceStrategyTests,
 }
 
 TEST_F(SequentialEquivalenceStrategyTests,
-       SequentialDesignModelExtractExpandsNonBinaryDFFInitLiterals) {
+       SequentialDesignModelExtractIgnoresNonCanonicalDFFInit) {
+  NLUniverse::create();
+  auto* db = NLDB::create(NLUniverse::get());
+  auto* primitives =
+      NLLibrary::create(db, NLLibrary::Type::Primitives, NLName("prims"));
+  auto* library =
+      NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs"));
+  auto* invModel = createInvModel(primitives);
+  auto* top = createDffTop(library, "top", invModel, false, false);
+  auto* ff = top->getInstance(NLName("ff0"));
+  ASSERT_NE(ff, nullptr);
+  auto* initParam = ff->getModel()->getParameter(NLName("INIT"));
+  ASSERT_NE(initParam, nullptr);
+  // Only the canonical sized-binary form (written by the naja frontends) is
+  // harvested; anything else leaves the state unconstrained.
+  SNLInstParameter::create(ff, initParam, "1'h1");
+
+  const auto extracted = SequentialDesignModel::extract(top);
+
+  EXPECT_FALSE(extracted.hasUnsupportedFeatures());
+  EXPECT_TRUE(extracted.initialStateValueByKey.empty());
+}
+
+TEST_F(SequentialEquivalenceStrategyTests,
+       SequentialDesignModelExtractExtendsNarrowDFFInitLiterals) {
   NLUniverse::create();
   auto* db = NLDB::create(NLUniverse::get());
   auto* library =
@@ -16062,142 +16086,27 @@ TEST_F(SequentialEquivalenceStrategyTests,
     return SequentialDesignModel::extract(top);
   };
 
-  // Hex digits expand to four bits each: 4'h6 = 4'b0110.
-  const auto hexModel = extractWideDFFInit("4'h6");
-  EXPECT_FALSE(hexModel.hasUnsupportedFeatures());
-  ASSERT_EQ(hexModel.initialStateValueByKey.size(), 4u);
-  EXPECT_FALSE(hexModel.initialStateValueByKey.at(
-      findKeyByDisplayName(hexModel, "ff0.Q[3]")));
-  EXPECT_TRUE(hexModel.initialStateValueByKey.at(
-      findKeyByDisplayName(hexModel, "ff0.Q[2]")));
-  EXPECT_TRUE(hexModel.initialStateValueByKey.at(
-      findKeyByDisplayName(hexModel, "ff0.Q[1]")));
-  EXPECT_FALSE(hexModel.initialStateValueByKey.at(
-      findKeyByDisplayName(hexModel, "ff0.Q[0]")));
-
-  // Short binary literals zero-extend: 4'b1 = 4'b0001.
-  const auto shortModel = extractWideDFFInit("4'b1");
-  EXPECT_FALSE(shortModel.hasUnsupportedFeatures());
-  ASSERT_EQ(shortModel.initialStateValueByKey.size(), 4u);
-  EXPECT_FALSE(shortModel.initialStateValueByKey.at(
-      findKeyByDisplayName(shortModel, "ff0.Q[3]")));
-  EXPECT_FALSE(shortModel.initialStateValueByKey.at(
-      findKeyByDisplayName(shortModel, "ff0.Q[2]")));
-  EXPECT_FALSE(shortModel.initialStateValueByKey.at(
-      findKeyByDisplayName(shortModel, "ff0.Q[1]")));
-  EXPECT_TRUE(shortModel.initialStateValueByKey.at(
-      findKeyByDisplayName(shortModel, "ff0.Q[0]")));
-
-  // Decimal literals convert to bits: 4'd5 = 4'b0101.
-  const auto decimalModel = extractWideDFFInit("4'd5");
-  EXPECT_FALSE(decimalModel.hasUnsupportedFeatures());
-  ASSERT_EQ(decimalModel.initialStateValueByKey.size(), 4u);
-  EXPECT_FALSE(decimalModel.initialStateValueByKey.at(
-      findKeyByDisplayName(decimalModel, "ff0.Q[3]")));
-  EXPECT_TRUE(decimalModel.initialStateValueByKey.at(
-      findKeyByDisplayName(decimalModel, "ff0.Q[2]")));
-  EXPECT_FALSE(decimalModel.initialStateValueByKey.at(
-      findKeyByDisplayName(decimalModel, "ff0.Q[1]")));
-  EXPECT_TRUE(decimalModel.initialStateValueByKey.at(
-      findKeyByDisplayName(decimalModel, "ff0.Q[0]")));
-
-  // Digit separators are ignored: 4'b1_010 = 4'b1010.
-  const auto separatedModel = extractWideDFFInit("4'b1_010");
-  EXPECT_FALSE(separatedModel.hasUnsupportedFeatures());
-  ASSERT_EQ(separatedModel.initialStateValueByKey.size(), 4u);
-  EXPECT_TRUE(separatedModel.initialStateValueByKey.at(
-      findKeyByDisplayName(separatedModel, "ff0.Q[3]")));
-  EXPECT_FALSE(separatedModel.initialStateValueByKey.at(
-      findKeyByDisplayName(separatedModel, "ff0.Q[2]")));
-  EXPECT_TRUE(separatedModel.initialStateValueByKey.at(
-      findKeyByDisplayName(separatedModel, "ff0.Q[1]")));
-  EXPECT_FALSE(separatedModel.initialStateValueByKey.at(
-      findKeyByDisplayName(separatedModel, "ff0.Q[0]")));
-
-  // Separators in decimal literals: 4'd1_0 = 10 = 4'b1010.
-  const auto separatedDecimalModel = extractWideDFFInit("4'd1_0");
-  EXPECT_FALSE(separatedDecimalModel.hasUnsupportedFeatures());
-  ASSERT_EQ(separatedDecimalModel.initialStateValueByKey.size(), 4u);
-  EXPECT_TRUE(separatedDecimalModel.initialStateValueByKey.at(
-      findKeyByDisplayName(separatedDecimalModel, "ff0.Q[3]")));
-  EXPECT_FALSE(separatedDecimalModel.initialStateValueByKey.at(
-      findKeyByDisplayName(separatedDecimalModel, "ff0.Q[2]")));
-  EXPECT_TRUE(separatedDecimalModel.initialStateValueByKey.at(
-      findKeyByDisplayName(separatedDecimalModel, "ff0.Q[1]")));
-  EXPECT_FALSE(separatedDecimalModel.initialStateValueByKey.at(
-      findKeyByDisplayName(separatedDecimalModel, "ff0.Q[0]")));
-
-  // Separators in the width field are ignored too: 0_4'h6 = 4'b0110.
-  const auto separatedWidthModel = extractWideDFFInit("0_4'h6");
-  EXPECT_FALSE(separatedWidthModel.hasUnsupportedFeatures());
-  ASSERT_EQ(separatedWidthModel.initialStateValueByKey.size(), 4u);
-  EXPECT_FALSE(separatedWidthModel.initialStateValueByKey.at(
-      findKeyByDisplayName(separatedWidthModel, "ff0.Q[3]")));
-  EXPECT_TRUE(separatedWidthModel.initialStateValueByKey.at(
-      findKeyByDisplayName(separatedWidthModel, "ff0.Q[2]")));
-  EXPECT_TRUE(separatedWidthModel.initialStateValueByKey.at(
-      findKeyByDisplayName(separatedWidthModel, "ff0.Q[1]")));
-  EXPECT_FALSE(separatedWidthModel.initialStateValueByKey.at(
-      findKeyByDisplayName(separatedWidthModel, "ff0.Q[0]")));
-
-  // The signed marker does not change the bit pattern: 4'sh6 = 4'b0110.
-  const auto signedHexModel = extractWideDFFInit("4'sh6");
-  EXPECT_FALSE(signedHexModel.hasUnsupportedFeatures());
-  ASSERT_EQ(signedHexModel.initialStateValueByKey.size(), 4u);
-  EXPECT_FALSE(signedHexModel.initialStateValueByKey.at(
-      findKeyByDisplayName(signedHexModel, "ff0.Q[3]")));
-  EXPECT_TRUE(signedHexModel.initialStateValueByKey.at(
-      findKeyByDisplayName(signedHexModel, "ff0.Q[2]")));
-  EXPECT_TRUE(signedHexModel.initialStateValueByKey.at(
-      findKeyByDisplayName(signedHexModel, "ff0.Q[1]")));
-  EXPECT_FALSE(signedHexModel.initialStateValueByKey.at(
-      findKeyByDisplayName(signedHexModel, "ff0.Q[0]")));
-
-  // Negative decimals are stored as two's complement: -4'd3 = 4'b1101.
-  const auto negativeDecimalModel = extractWideDFFInit("-4'd3");
-  EXPECT_FALSE(negativeDecimalModel.hasUnsupportedFeatures());
-  ASSERT_EQ(negativeDecimalModel.initialStateValueByKey.size(), 4u);
-  EXPECT_TRUE(negativeDecimalModel.initialStateValueByKey.at(
-      findKeyByDisplayName(negativeDecimalModel, "ff0.Q[3]")));
-  EXPECT_TRUE(negativeDecimalModel.initialStateValueByKey.at(
-      findKeyByDisplayName(negativeDecimalModel, "ff0.Q[2]")));
-  EXPECT_FALSE(negativeDecimalModel.initialStateValueByKey.at(
-      findKeyByDisplayName(negativeDecimalModel, "ff0.Q[1]")));
-  EXPECT_TRUE(negativeDecimalModel.initialStateValueByKey.at(
-      findKeyByDisplayName(negativeDecimalModel, "ff0.Q[0]")));
-
-  // An unknown digit under the negation carry makes the carry and all higher
-  // bits unknown: -4'b0x00 = 4'bxx00, so only the low two bits constrain.
-  const auto negativeUnknownModel = extractWideDFFInit("-4'b0x00");
-  EXPECT_FALSE(negativeUnknownModel.hasUnsupportedFeatures());
-  ASSERT_EQ(negativeUnknownModel.initialStateValueByKey.size(), 2u);
-  EXPECT_EQ(
-      negativeUnknownModel.initialStateValueByKey.find(
-          findKeyByDisplayName(negativeUnknownModel, "ff0.Q[3]")),
-      negativeUnknownModel.initialStateValueByKey.end());
-  EXPECT_EQ(
-      negativeUnknownModel.initialStateValueByKey.find(
-          findKeyByDisplayName(negativeUnknownModel, "ff0.Q[2]")),
-      negativeUnknownModel.initialStateValueByKey.end());
-  EXPECT_FALSE(negativeUnknownModel.initialStateValueByKey.at(
-      findKeyByDisplayName(negativeUnknownModel, "ff0.Q[1]")));
-  EXPECT_FALSE(negativeUnknownModel.initialStateValueByKey.at(
-      findKeyByDisplayName(negativeUnknownModel, "ff0.Q[0]")));
-
-  // The signed marker does not change the literal's own bit pattern:
-  // 4'sb1 = 4'b0001 (extension is per literal width, sign extension only
-  // applies when a later context widens the value).
-  const auto signedShortModel = extractWideDFFInit("4'sb1");
-  EXPECT_FALSE(signedShortModel.hasUnsupportedFeatures());
-  ASSERT_EQ(signedShortModel.initialStateValueByKey.size(), 4u);
-  EXPECT_FALSE(signedShortModel.initialStateValueByKey.at(
-      findKeyByDisplayName(signedShortModel, "ff0.Q[3]")));
-  EXPECT_FALSE(signedShortModel.initialStateValueByKey.at(
-      findKeyByDisplayName(signedShortModel, "ff0.Q[2]")));
-  EXPECT_FALSE(signedShortModel.initialStateValueByKey.at(
-      findKeyByDisplayName(signedShortModel, "ff0.Q[1]")));
-  EXPECT_TRUE(signedShortModel.initialStateValueByKey.at(
-      findKeyByDisplayName(signedShortModel, "ff0.Q[0]")));
+  // A narrower literal zero-extends to the storage width: 2'b11 on a 4-bit
+  // register initializes Q[1:0] to 1 and Q[3:2] to 0.
+  const auto zeroExtended = extractWideDFFInit("2'b11");
+  EXPECT_FALSE(zeroExtended.hasUnsupportedFeatures());
+  ASSERT_EQ(zeroExtended.initialStateValueByKey.size(), 4u);
+  EXPECT_FALSE(zeroExtended.initialStateValueByKey.at(
+      findKeyByDisplayName(zeroExtended, "ff0.Q[3]")));
+  EXPECT_FALSE(zeroExtended.initialStateValueByKey.at(
+      findKeyByDisplayName(zeroExtended, "ff0.Q[2]")));
+  EXPECT_TRUE(zeroExtended.initialStateValueByKey.at(
+      findKeyByDisplayName(zeroExtended, "ff0.Q[1]")));
+  EXPECT_TRUE(zeroExtended.initialStateValueByKey.at(
+      findKeyByDisplayName(zeroExtended, "ff0.Q[0]")));
+
+  // A narrower literal whose top digit is unknown x-extends instead: 2'bx1
+  // initializes Q[0] and leaves Q[3:1] unconstrained.
+  const auto xExtended = extractWideDFFInit("2'bx1");
+  EXPECT_FALSE(xExtended.hasUnsupportedFeatures());
+  ASSERT_EQ(xExtended.initialStateValueByKey.size(), 1u);
+  EXPECT_TRUE(xExtended.initialStateValueByKey.at(
+      findKeyByDisplayName(xExtended, "ff0.Q[0]")));
 }
 
 TEST_F(SequentialEquivalenceStrategyTests,
diff --git a/thirdparty/naja b/thirdparty/naja
index 1d33c24c..6ee82cf6 160000
--- a/thirdparty/naja
+++ b/thirdparty/naja
@@ -1 +1 @@
-Subproject commit 1d33c24c408f975aac901dc91cf316e02fe6dc82
+Subproject commit 6ee82cf6f0f6625a7921a114d8f18d2844cf4964

From fe994a045152ab787614a209eb9735e944461395 Mon Sep 17 00:00:00 2001
From: Emin <me@emin.chat>
Date: Tue, 22 Sep 2026 17:11:22 +0800
Subject: [PATCH 12/14] Slim SEC INIT reading under the canonical parameter
 form

---
 src/sec/model/SequentialDesignModel.cpp       |  76 ++++-------
 .../SequentialEquivalenceStrategyTests.cpp    | 126 ++++++------------
 2 files changed, 68 insertions(+), 134 deletions(-)

diff --git a/src/sec/model/SequentialDesignModel.cpp b/src/sec/model/SequentialDesignModel.cpp
index 480f2e1c..69b65da2 100644
--- a/src/sec/model/SequentialDesignModel.cpp
+++ b/src/sec/model/SequentialDesignModel.cpp
@@ -3161,16 +3161,13 @@ void appendPendingTransitionsForInstance(
   }
 }
 
-// Reads the DFF INIT instance parameter for the given state output terminal.
-// The naja frontends store INIT in a canonical form ("<width>'b<msb...lsb>",
-// lowercase digits in 0/1/x/z); anything else leaves the state unconstrained.
-// Returns the digit for the terminal's bit in the storage element's own
-// polarity. initDigitsByInstance caches the LSB-first digit string so a wide
-// DFF converts it once per instance instead of once per output bit.
+// Reads the canonical INIT digit ("<width>'b<msb...lsb>", lowercase 0/1/x/z)
+// for the given state output terminal, in the storage element's own polarity.
+// The naja frontends always store INIT in this form with the width of the Q
+// output; anything else is treated as absent and leaves the state
+// unconstrained.
 std::optional<bool> readDFFInitDigitForStateTerm(
-    const naja::DNL::DNLTerminalFull& term,
-    std::unordered_map<const naja::NL::SNLInstance*,
-                       std::optional<std::string>>& initDigitsByInstance) {
+    const naja::DNL::DNLTerminalFull& term) {
   if (term.isNull() || term.isTopPort()) {
     return std::nullopt;  // LCOV_EXCL_LINE
   }
@@ -3178,49 +3175,30 @@ std::optional<bool> readDFFInitDigitForStateTerm(
   if (snlInstance == nullptr) {
     return std::nullopt;  // LCOV_EXCL_LINE
   }
-  auto cached = initDigitsByInstance.find(snlInstance);
-  if (cached == initDigitsByInstance.end()) {
-    std::optional<std::string> digits;
-    if (const auto* initParam =
-            snlInstance->getInstParameter(naja::NL::NLName("INIT"))) {
-      const std::string value = initParam->getValue();
-      const auto basePos = value.find('\'');
-      if (basePos != std::string::npos && basePos + 2 < value.size() &&
-          (value[basePos + 1] == 'b' || value[basePos + 1] == 'B')) {
-        // Flip to LSB-first so bit i sits at index i.
-        std::string reversed(value.substr(basePos + 2));
-        std::reverse(reversed.begin(), reversed.end());
-        digits = std::move(reversed);
-      }
-    }
-    cached = initDigitsByInstance.emplace(snlInstance, std::move(digits)).first;
-  }
-  const auto& digits = cached->second;
-  if (!digits.has_value() || digits->empty()) {
+  const auto* initParam =
+      snlInstance->getInstParameter(naja::NL::NLName("INIT"));
+  if (initParam == nullptr) {
     return std::nullopt;
   }
-  size_t bitIndex = 0;
-  const auto* bitTerm = term.getSnlBitTerm();
-  if (const auto* busBit =
-          dynamic_cast<const naja::NL::SNLBusTermBit*>(bitTerm)) {
-    const auto offset = static_cast<int64_t>(busBit->getBit()) -
-                        busBit->getBus()->getLSB();
-    if (offset < 0) {
-      return std::nullopt;  // LCOV_EXCL_LINE
-    }
-    bitIndex = static_cast<size_t>(offset);
+  const std::string value = initParam->getValue();
+  const auto basePos = value.find('\'');
+  if (basePos == std::string::npos || basePos + 2 >= value.size() ||
+      (value[basePos + 1] != 'b' && value[basePos + 1] != 'B')) {
+    return std::nullopt;  // non-canonical INIT
   }
-  if (bitIndex >= digits->size()) {
-    // A literal narrower than the Q bus extends per Verilog rules: with zero,
-    // or with x/z when its most-significant digit is unknown.
-    const char top = static_cast<char>(
-        std::tolower(static_cast<unsigned char>(digits->back())));
-    if (top == '0' || top == '1') {
-      return false;
+  const size_t width = value.size() - (basePos + 2);
+  size_t digitIndex = 0;  // into the MSB-first digit string
+  if (const auto* busBit =
+          dynamic_cast<const naja::NL::SNLBusTermBit*>(term.getSnlBitTerm())) {
+    const auto* bus = busBit->getBus();
+    if (width != static_cast<size_t>(bus->getWidth())) {
+      return std::nullopt;  // INIT width must match the Q output width
     }
-    return std::nullopt;
+    digitIndex = width - 1 - static_cast<size_t>(busBit->getBit() - bus->getLSB());
+  } else if (width != 1) {
+    return std::nullopt;  // LCOV_EXCL_LINE
   }
-  switch (std::tolower(static_cast<unsigned char>(digits->at(bitIndex)))) {
+  switch (std::tolower(static_cast<unsigned char>(value[basePos + 2 + digitIndex]))) {
     case '0':
       return false;
     case '1':
@@ -3236,11 +3214,9 @@ std::optional<bool> readDFFInitDigitForStateTerm(
 // keys get the opposite value.
 void harvestInitialStateValues(ExtractContext& ctx, SequentialDesignModel& model) {
   size_t harvested = 0;
-  std::unordered_map<const naja::NL::SNLInstance*, std::optional<std::string>>
-      initDigitsByInstance;
   for (const auto& pending : ctx.pendingTransitions) {
     const auto& term = ctx.dnl->getDNLTerminalFromID(pending.stateTermID);
-    const auto digit = readDFFInitDigitForStateTerm(term, initDigitsByInstance);
+    const auto digit = readDFFInitDigitForStateTerm(term);
     if (!digit.has_value()) {
       continue;
     }
diff --git a/test/sec/SequentialEquivalenceStrategyTests.cpp b/test/sec/SequentialEquivalenceStrategyTests.cpp
index 297b113e..55140994 100644
--- a/test/sec/SequentialEquivalenceStrategyTests.cpp
+++ b/test/sec/SequentialEquivalenceStrategyTests.cpp
@@ -15898,6 +15898,40 @@ TEST_F(SequentialEquivalenceStrategyTests,
   EXPECT_TRUE(model.initialStateValueByKey.empty());
 }
 
+SNLDesign* createWideDffTopWithInit(
+    NLLibrary* library,
+    const std::string& name,
+    const char* initValue) {
+  auto* top =
+      SNLDesign::create(library, SNLDesign::Type::Standard, NLName(name));
+  auto* topIn = SNLBusTerm::create(
+      top, SNLTerm::Direction::Input, 3, 0, NLName("in"));
+  auto* topClock = SNLScalarTerm::create(
+      top, SNLTerm::Direction::Input, NLName("clk"));
+  auto* topOut = SNLBusTerm::create(
+      top, SNLTerm::Direction::Output, 3, 0, NLName("out"));
+
+  auto* dffModel = NLDB0::getOrCreateDFF(4);
+  auto* ff = SNLInstance::create(top, dffModel, NLName("ff0"));
+  auto* netIn = SNLBusNet::create(top, 3, 0, NLName("net_in"));
+  auto* netClock = SNLScalarNet::create(top, NLName("net_clk"));
+  auto* netQ = SNLBusNet::create(top, 3, 0, NLName("net_q"));
+
+  auto* dataTerm = dffModel->getBusTerm(NLName("D"));
+  auto* outputTerm = dffModel->getBusTerm(NLName("Q"));
+  topClock->setNet(netClock);
+  ff->getInstTerm(dffModel->getScalarTerm(NLName("C")))->setNet(netClock);
+  for (int bit = 0; bit <= 3; ++bit) {
+    topIn->getBit(bit)->setNet(netIn->getBit(bit));
+    ff->getInstTerm(dataTerm->getBit(bit))->setNet(netIn->getBit(bit));
+    ff->getInstTerm(outputTerm->getBit(bit))->setNet(netQ->getBit(bit));
+    topOut->getBit(bit)->setNet(netQ->getBit(bit));
+  }
+  SNLInstParameter::create(
+      ff, dffModel->getParameter(NLName("INIT")), initValue);
+  return top;
+}
+
 TEST_F(SequentialEquivalenceStrategyTests,
        SequentialDesignModelExtractHarvestsDFFInitParameter) {
   NLUniverse::create();
@@ -15973,38 +16007,8 @@ TEST_F(SequentialEquivalenceStrategyTests,
   auto* db = NLDB::create(NLUniverse::get());
   auto* library =
       NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs"));
-  auto* top =
-      SNLDesign::create(library, SNLDesign::Type::Standard, NLName("top"));
-  auto* topIn = SNLBusTerm::create(
-      top, SNLTerm::Direction::Input, 3, 0, NLName("in"));
-  auto* topClock = SNLScalarTerm::create(
-      top, SNLTerm::Direction::Input, NLName("clk"));
-  auto* topOut = SNLBusTerm::create(
-      top, SNLTerm::Direction::Output, 3, 0, NLName("out"));
-
-  auto* dffModel = NLDB0::getOrCreateDFF(4);
-  ASSERT_NE(dffModel, nullptr);
-  auto* ff = SNLInstance::create(top, dffModel, NLName("ff0"));
-  auto* netIn = SNLBusNet::create(top, 3, 0, NLName("net_in"));
-  auto* netClock = SNLScalarNet::create(top, NLName("net_clk"));
-  auto* netQ = SNLBusNet::create(top, 3, 0, NLName("net_q"));
-
-  auto* dataTerm = dffModel->getBusTerm(NLName("D"));
-  auto* outputTerm = dffModel->getBusTerm(NLName("Q"));
-  ASSERT_NE(dataTerm, nullptr);
-  ASSERT_NE(outputTerm, nullptr);
-  topClock->setNet(netClock);
-  ff->getInstTerm(dffModel->getScalarTerm(NLName("C")))->setNet(netClock);
-  for (int bit = 0; bit <= 3; ++bit) {
-    topIn->getBit(bit)->setNet(netIn->getBit(bit));
-    ff->getInstTerm(dataTerm->getBit(bit))->setNet(netIn->getBit(bit));
-    ff->getInstTerm(outputTerm->getBit(bit))->setNet(netQ->getBit(bit));
-    topOut->getBit(bit)->setNet(netQ->getBit(bit));
-  }
-  auto* initParam = dffModel->getParameter(NLName("INIT"));
-  ASSERT_NE(initParam, nullptr);
   // INIT digits are MSB first: bit3=0, bit2=1, bit1=x (unconstrained), bit0=0.
-  SNLInstParameter::create(ff, initParam, "4'b01x0");
+  auto* top = createWideDffTopWithInit(library, "top", "4'b01x0");
 
   const auto extracted = SequentialDesignModel::extract(top);
 
@@ -16048,65 +16052,19 @@ TEST_F(SequentialEquivalenceStrategyTests,
 }
 
 TEST_F(SequentialEquivalenceStrategyTests,
-       SequentialDesignModelExtractExtendsNarrowDFFInitLiterals) {
+       SequentialDesignModelExtractIgnoresWidthMismatchedDFFInit) {
   NLUniverse::create();
   auto* db = NLDB::create(NLUniverse::get());
   auto* library =
       NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs"));
+  // The canonical form always covers the whole Q output; a width-mismatched
+  // INIT did not come from a naja frontend and leaves the state unconstrained.
+  auto* top = createWideDffTopWithInit(library, "top", "2'b11");
 
-  int designCounter = 0;
-  auto extractWideDFFInit = [&](const char* initValue) {
-    auto* top = SNLDesign::create(
-        library,
-        SNLDesign::Type::Standard,
-        NLName("top" + std::to_string(designCounter++)));
-    auto* topIn = SNLBusTerm::create(
-        top, SNLTerm::Direction::Input, 3, 0, NLName("in"));
-    auto* topClock = SNLScalarTerm::create(
-        top, SNLTerm::Direction::Input, NLName("clk"));
-    auto* topOut = SNLBusTerm::create(
-        top, SNLTerm::Direction::Output, 3, 0, NLName("out"));
-    auto* dffModel = NLDB0::getOrCreateDFF(4);
-    auto* ff = SNLInstance::create(top, dffModel, NLName("ff0"));
-    auto* netIn = SNLBusNet::create(top, 3, 0, NLName("net_in"));
-    auto* netClock = SNLScalarNet::create(top, NLName("net_clk"));
-    auto* netQ = SNLBusNet::create(top, 3, 0, NLName("net_q"));
-    auto* dataTerm = dffModel->getBusTerm(NLName("D"));
-    auto* outputTerm = dffModel->getBusTerm(NLName("Q"));
-    topClock->setNet(netClock);
-    ff->getInstTerm(dffModel->getScalarTerm(NLName("C")))->setNet(netClock);
-    for (int bit = 0; bit <= 3; ++bit) {
-      topIn->getBit(bit)->setNet(netIn->getBit(bit));
-      ff->getInstTerm(dataTerm->getBit(bit))->setNet(netIn->getBit(bit));
-      ff->getInstTerm(outputTerm->getBit(bit))->setNet(netQ->getBit(bit));
-      topOut->getBit(bit)->setNet(netQ->getBit(bit));
-    }
-    SNLInstParameter::create(
-        ff, dffModel->getParameter(NLName("INIT")), initValue);
-    return SequentialDesignModel::extract(top);
-  };
+  const auto extracted = SequentialDesignModel::extract(top);
 
-  // A narrower literal zero-extends to the storage width: 2'b11 on a 4-bit
-  // register initializes Q[1:0] to 1 and Q[3:2] to 0.
-  const auto zeroExtended = extractWideDFFInit("2'b11");
-  EXPECT_FALSE(zeroExtended.hasUnsupportedFeatures());
-  ASSERT_EQ(zeroExtended.initialStateValueByKey.size(), 4u);
-  EXPECT_FALSE(zeroExtended.initialStateValueByKey.at(
-      findKeyByDisplayName(zeroExtended, "ff0.Q[3]")));
-  EXPECT_FALSE(zeroExtended.initialStateValueByKey.at(
-      findKeyByDisplayName(zeroExtended, "ff0.Q[2]")));
-  EXPECT_TRUE(zeroExtended.initialStateValueByKey.at(
-      findKeyByDisplayName(zeroExtended, "ff0.Q[1]")));
-  EXPECT_TRUE(zeroExtended.initialStateValueByKey.at(
-      findKeyByDisplayName(zeroExtended, "ff0.Q[0]")));
-
-  // A narrower literal whose top digit is unknown x-extends instead: 2'bx1
-  // initializes Q[0] and leaves Q[3:1] unconstrained.
-  const auto xExtended = extractWideDFFInit("2'bx1");
-  EXPECT_FALSE(xExtended.hasUnsupportedFeatures());
-  ASSERT_EQ(xExtended.initialStateValueByKey.size(), 1u);
-  EXPECT_TRUE(xExtended.initialStateValueByKey.at(
-      findKeyByDisplayName(xExtended, "ff0.Q[0]")));
+  EXPECT_FALSE(extracted.hasUnsupportedFeatures());
+  EXPECT_TRUE(extracted.initialStateValueByKey.empty());
 }
 
 TEST_F(SequentialEquivalenceStrategyTests,

From 7c9ea3e6c100cfa939204a1ed0ab5bfdd761a72d Mon Sep 17 00:00:00 2001
From: Emin <me@emin.chat>
Date: Tue, 22 Sep 2026 17:44:30 +0800
Subject: [PATCH 13/14] Handle ascending buses when reading canonical DFF INIT
 digits

---
 src/sec/model/SequentialDesignModel.cpp       |  6 +-
 .../SequentialEquivalenceStrategyTests.cpp    | 81 +++++++++++++++++++
 2 files changed, 86 insertions(+), 1 deletion(-)

diff --git a/src/sec/model/SequentialDesignModel.cpp b/src/sec/model/SequentialDesignModel.cpp
index 69b65da2..ade76579 100644
--- a/src/sec/model/SequentialDesignModel.cpp
+++ b/src/sec/model/SequentialDesignModel.cpp
@@ -3194,7 +3194,11 @@ std::optional<bool> readDFFInitDigitForStateTerm(
     if (width != static_cast<size_t>(bus->getWidth())) {
       return std::nullopt;  // INIT width must match the Q output width
     }
-    digitIndex = width - 1 - static_cast<size_t>(busBit->getBit() - bus->getLSB());
+    // Digit 0 of the canonical form is the bus MSB, for either ascending or
+    // descending ranges.
+    const auto msb = bus->getMSB();
+    const auto bit = busBit->getBit();
+    digitIndex = static_cast<size_t>(msb >= bit ? msb - bit : bit - msb);
   } else if (width != 1) {
     return std::nullopt;  // LCOV_EXCL_LINE
   }
diff --git a/test/sec/SequentialEquivalenceStrategyTests.cpp b/test/sec/SequentialEquivalenceStrategyTests.cpp
index 55140994..a10f4d85 100644
--- a/test/sec/SequentialEquivalenceStrategyTests.cpp
+++ b/test/sec/SequentialEquivalenceStrategyTests.cpp
@@ -16027,6 +16027,87 @@ TEST_F(SequentialEquivalenceStrategyTests,
       findKeyByDisplayName(extracted, "ff0.Q[0]")));
 }
 
+TEST_F(SequentialEquivalenceStrategyTests,
+       SequentialDesignModelExtractHarvestsAscendingBusDFFInitParameter) {
+  NLUniverse::create();
+  auto* db = NLDB::create(NLUniverse::get());
+  auto* primitives =
+      NLLibrary::create(db, NLLibrary::Type::Primitives, NLName("prims"));
+  auto* library =
+      NLLibrary::create(db, NLLibrary::Type::Standard, NLName("designs"));
+
+  // A flip-flop primitive with ascending D/Q buses [0:3].
+  auto* model = SNLDesign::create(
+      primitives, SNLDesign::Type::Primitive, NLName("DFF_ASC"));
+  auto* clock =
+      SNLScalarTerm::create(model, SNLTerm::Direction::Input, NLName("C"));
+  auto* data =
+      SNLBusTerm::create(model, SNLTerm::Direction::Input, 0, 3, NLName("D"));
+  auto* output =
+      SNLBusTerm::create(model, SNLTerm::Direction::Output, 0, 3, NLName("Q"));
+  SNLParameter::create(
+      model, NLName("INIT"), SNLParameter::Type::Binary, "4'bxxxx");
+  SNLDesignModeling::BitTerms outputBits;
+  SNLDesignModeling::BitTerms dataBits;
+  for (int bit = 0; bit <= 3; ++bit) {
+    outputBits.push_back(output->getBit(bit));
+    dataBits.push_back(data->getBit(bit));
+  }
+  SNLDesignModeling::addClockToOutputsArcs(clock, outputBits);
+  SNLDesignModeling::addInputsToClockArcs(dataBits, clock);
+  SNLDesignModeling::SequentialModel sequentialModel;
+  sequentialModel.kind = SNLDesignModeling::SequentialModel::Kind::FlipFlop;
+  sequentialModel.clockedOn = makeSequentialTermExpression(clock);
+  for (int bit = 0; bit <= 3; ++bit) {
+    SNLDesignModeling::SequentialState state;
+    state.nextState = makeSequentialTermExpression(data->getBit(bit));
+    sequentialModel.states.push_back(std::move(state));
+    sequentialModel.outputs.push_back(
+        {output->getBit(bit), makeSequentialStateExpression(bit)});
+  }
+  SNLDesignModeling::setSequentialModel(model, sequentialModel);
+
+  auto* top =
+      SNLDesign::create(library, SNLDesign::Type::Standard, NLName("top"));
+  auto* topIn = SNLBusTerm::create(
+      top, SNLTerm::Direction::Input, 0, 3, NLName("in"));
+  auto* topClock = SNLScalarTerm::create(
+      top, SNLTerm::Direction::Input, NLName("clk"));
+  auto* topOut = SNLBusTerm::create(
+      top, SNLTerm::Direction::Output, 0, 3, NLName("out"));
+  auto* ff = SNLInstance::create(top, model, NLName("ff0"));
+  auto* netIn = SNLBusNet::create(top, 0, 3, NLName("net_in"));
+  auto* netClock = SNLScalarNet::create(top, NLName("net_clk"));
+  auto* netQ = SNLBusNet::create(top, 0, 3, NLName("net_q"));
+  topClock->setNet(netClock);
+  ff->getInstTerm(model->getScalarTerm(NLName("C")))->setNet(netClock);
+  for (int bit = 0; bit <= 3; ++bit) {
+    topIn->getBit(bit)->setNet(netIn->getBit(bit));
+    ff->getInstTerm(data->getBit(bit))->setNet(netIn->getBit(bit));
+    ff->getInstTerm(output->getBit(bit))->setNet(netQ->getBit(bit));
+    topOut->getBit(bit)->setNet(netQ->getBit(bit));
+  }
+  // Canonical digit 0 is the declared leftmost index (bit 0 for [0:3]).
+  SNLInstParameter::create(
+      ff, model->getParameter(NLName("INIT")), "4'b01x0");
+
+  const auto extracted = SequentialDesignModel::extract(top);
+
+  EXPECT_FALSE(extracted.hasUnsupportedFeatures());
+  ASSERT_EQ(extracted.stateBits.size(), 4u);
+  EXPECT_EQ(extracted.initialStateValueByKey.size(), 3u);
+  EXPECT_FALSE(extracted.initialStateValueByKey.at(
+      findKeyByDisplayName(extracted, "ff0.Q[0]")));
+  EXPECT_TRUE(extracted.initialStateValueByKey.at(
+      findKeyByDisplayName(extracted, "ff0.Q[1]")));
+  EXPECT_EQ(
+      extracted.initialStateValueByKey.find(
+          findKeyByDisplayName(extracted, "ff0.Q[2]")),
+      extracted.initialStateValueByKey.end());
+  EXPECT_FALSE(extracted.initialStateValueByKey.at(
+      findKeyByDisplayName(extracted, "ff0.Q[3]")));
+}
+
 TEST_F(SequentialEquivalenceStrategyTests,
        SequentialDesignModelExtractIgnoresNonCanonicalDFFInit) {
   NLUniverse::create();

From 628e5477ed886acf7547457cce0527b9febc919d Mon Sep 17 00:00:00 2001
From: Emin <me@emin.chat>
Date: Tue, 22 Sep 2026 17:45:15 +0800
Subject: [PATCH 14/14] Bump naja for type-gated parameter canonicalization

---
 thirdparty/naja | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/thirdparty/naja b/thirdparty/naja
index 6ee82cf6..0710aff6 160000
--- a/thirdparty/naja
+++ b/thirdparty/naja
@@ -1 +1 @@
-Subproject commit 6ee82cf6f0f6625a7921a114d8f18d2844cf4964
+Subproject commit 0710aff6918251315414fb55590c1ba6869958e0