Repository navigation
SEC skips every output in a cone containing an x/z literal #214
Description
Activity
Three corrections to the above.
1. Suggestion 1 is wrong. A free variable is universally quantified, so it
would demand equality for every value of the don't-care, while synthesis
resolved it to one. A correct design would come back inequivalent. Don't-care
needs the implication instead:forall inputs: defined_rtl(inputs) -> rtl_out(inputs) == gate_out(inputs)i.e. definedness carried alongside the value (3-valued or care-set), which is
real work. Suggestions 2 and 3 stand on their own.2. The closing note is wrong.
Unknown literal bits in always_comb assignment RHS lowered as 0 in SNLisalways_comb-specific and does not
appear for the reproducer, which uses a continuous assign — its diagnostics
report is empty. I took that quote from a larger design's log.3. It is not only the ternary arm. Each of these is 0% coverage compared
against itself;1'b0is 100%:expression coverage assign y = en ? a : 1'b0;100.00% assign y = en ? a : 1'bx;0.00% assign y = a & 1'bx;0.00% assign y = a | 1'bx;0.00% assign y = 1'bx;0.00% a & 1'bxis defined wheneverais 0, and still costs the whole cone.Hello @ovebryne,
There was some additional issue with assigns that was fixed in latest, but on top of that we have now support for rest boot based on user input. Can you please check: https://github.com/keplertech/kepler-formal/blob/main/docs/sec-reset-bootstrap.md?
Checked main at
27cf7906ec4bf5caaa1026e333e580f6eb7202b1(contains fix6).
The x/z behaviour is unchanged — each design compared against itself:design coverage assign y = en ? a : 1'b0;100.00% assign y = en ? a : 1'bx;0.00% assign y = en ? a : 1'bz;0.00% assign y = a & 1'bx;0.00% assign y = 1'bx;0.00% assign R0_data = R0_en ? Memory[R0_addr] : 46'b0;100.00% assign R0_data = R0_en ? Memory[R0_addr] : 46'bx;0.00% The 0% rows still end with
... not collected as a primary input. So whichever
assign issue was fixed in latest, it is a different one — I did confirm the
sv2v collision fix separately on #212.Reset bootstrap does not apply here. Both flags are present, and on a
sequential variant with a real reset port:plain --sec-reset-cycles 10 --sec-reset-port reset=1reset ? 0 : (en ? a : 1'b0)100.00% 100.00% reset ? 0 : (en ? a : 1'bx)0.00% 0.00% I gave it the shape the doc targets — real state, a real reset port — rather
than a combinational case, so this is not an unfair test. It matches the doc's
description: reset bootstrap constrains top-level reset inputs so state is
initialized by a reset sequence instead of by initial values. Here thexis in
the flop's next-state expression, not in its initial value, so it recurs every
cycle and there is nothing for the bootstrap to constrain. The feature looks
useful for x-initialized state; this is a different problem.What would still help, unchanged from the two asks in the issue above that do
not depend on modellingx:- Name the unknown literal and its location rather than reporting an
unmapped frontier term. The current message sends the reader looking for a
connectivity problem that does not exist — it cost me a while. - If X handling is deliberately out of scope, reject the input up front,
which is far cheaper than extracting both designs and then skipping every
output.
- Name the unknown literal and its location rather than reporting an
I prototyped the obvious cheap fix and it does not work — reporting the negative
result so nobody spends time on it.What I tried. In
BuildPrimaryOutputClauses, where an unmapped frontier
term currently drops the whole observed output, allocate a fresh variable for
that term instead of skipping. The intent was the combinational analogue of the
boundary abstraction you already do for uncomputable sequentials
(--no-sec-uncomputable-seq-boundary).It builds and it lifts coverage, but the verdict is wrong. Each design
compared against itself:design stock with the free variable y = en ? a : 1'b0100.00%, no difference 100.00%, no difference y = en ? a : 1'bx0.00%, cannot run 100.00%, Difference was foundy = en ? a : 1'bz0.00%, cannot run 100.00%, Difference was foundThe
1'b0row is the control: self-comparison still proves, so the patch has
not simply broken the checker.A design is not equivalent to itself. Each side's unknown becomes its own free
variable, so the property checked isforall x0, x1. out(x0) == out(x1), which
fails whenever the output depends on the unknown at all. Coverage rises and
every answer is a false difference.Aligning the two sides onto one shared variable would fix the self-comparison
case, but not the one I care about: in RTL vs gate-level the unknown exists only
on the RTL side — synthesis has already resolved it — so there is nothing to
align it to. The strict readingforall x. rtl(i, x) == gate(i)then fails for
every cone where the unknown is observable.So the free-variable route is not merely formally wrong, it is useless in
practice, and I would not take a flag that did this. It confirms what the issue
already says: the useful semantics is the implication — compare only where the
RTL is defined,defined_rtl(i) -> rtl_out(i) == gate_out(i)— which needs
definedness carried alongside the value.The two asks from my previous comment are unchanged.
Hello @ovebryne
If I understand correctly, the demended fix is mainly:
-
Name the unknown literal and its location rather than reporting an
unmapped frontier term. The current message sends the reader looking for a
connectivity problem that does not exist — it cost me a while. -
If X handling is deliberately out of scope, reject the input up front,
which is far cheaper than extracting both designs and then skipping every
output.
Am I right?
If yes, (1) sounds excellent and I will get to it. Regarding (2) it is a bit complicated as the existence of X still demends that analysis of the cones to determain which outputs are affected by it. In worse case it is indeed will to filter it one by one.
So (1) is great and I will fix it but even though I can look at how to optimize the process, (2) might be more complicated to acheive.
Sounds right for you?
-
Yes, both as written.
(1) — good. That is the one that cost me the time.
(2) — withdraw it. It was conditional on X being out of scope. You do per-cone
analysis anyway, and partial coverage beats a refusal.Best fix stays the issue itself: compare where the RTL is defined,
defined_rtl(i) -> rtl_out(i) == gate_out(i). Not a free variable per unknown
— prototype above, a design stops being equivalent to itself.Can't say yet whether that alone unblocks my design: another frontend problem
sat under the x/z skips. Yourmain's naja pin clears it (per #231). I'll
measure againstmainand report Friday.Tried it. (1) is in and works — every skip now names the literal and the site:
design0 unknown-constant: unsupported X constant (1'bx) used at <path>The old
not collected as a primary inputmessage is gone entirely.On what I owed you: with the other frontend problem fixed, the remaining skips
on the RTL side are all X constants — directly, or cascading from a sequential
skipped for one. But X is not the only thing holding coverage: every one of
those outputs also skips on the gate side, on an opaque macro with no usable
model, independent of X. So this issue is necessary but not sufficient to lift
coverage on my design.Correcting my 2026-09-11 comment. Runs on
mainat4b6b1bf5cc.I said "an opaque macro with no usable model". Wrong on both counts. It is a
stock ASAP7 standard cell, and it was already identified — in my own notes from
August. Every gate-side skip names the same model:design1 opaque-internal: opaque internal cell `_4014_` (model `ICGx1_ASAP7_75t_R`) pin `GCLK[0]`: no initialized combinational truth table or usable sequential modelICGx1_ASAP7_75t_R— the integrated clock gate, from
asap7sc7p5t_SEQ_RVT_FF_nldm_220123.lib. Reproducible without my design: any
ASAP7 netlist synthesised with clock gating contains these.Not a new bug — it is najaeda/naja#432's fix behaving as designed. naja does
not act onstatetable/state_function, the ICG's only functional description,
so the cell used to come back constant-zero. #432 marks such cells opaque
instead (testStateTableFunctionIsOpaque); SEC then skips cones containing one.
Strictly better than a wrong truth table. Not asking for a revert.Consequence worth flagging: an ICG sits on the clock path of nearly every
flop, so "skip cones containing an opaque cell" is close to "skip everything".Control, since I owed you one. Same design, same liberty, resynthesised with
clock gating disabled — every ICG gone. Coverage did not move: the same single
output. The next opaque cell is one of my own hardened blocks, shipped as a
Liberty timing abstract with nofunction. That part is mine, not yours.So #214 and the gate side are independent. My "necessary but not sufficient"
note stands, for a more specific reason than I gave.Which cases in the package are still worth your time:
case design1 vs design2 status self-xRTL vs itself, X present yours — X skips only, no gate side self-0X replaced by 0, vs itself yours — control, no extraction skips left x-vs-0the two against each other yours — unknown on one side only gate-xRTL vs gate netlist ignore — gate side blocked by the above gate-0X removed, vs gate netlist ignore — same x-vs-0is the one with an unambiguous expected answer. Both sides are RTL —
identical except for the X literals — so wherever the X side is defined the two
are the same by construction:defined(i) -> out_x(i) == out_0(i). Every output
must prove; no modelling judgement involved. Same shape as RTL-vs-gate, where
one side has resolved the unknown, but with nothing else in the way. It is where
a fix to this issue shows up.Separately: there is no way to abstract an opaque cell symmetrically, so a
netlist does not prove equivalent to itself. Unrelated to X semantics — filed as #245
rather than here.Hello @ovebryne ,
Following our disucssion, we added a new feature:
set_as_boundary - accepts pairs of leaf-instance paths, one from each design.
Their input pins become compared outputs, and their output pins become shared inputs.
The selected instances’ behavior is excluded without modifying netlists; default behavior is unchanged when omitted.Can you please give it a try and see if it matches your requirements?
Tested
set_as_boundaryonmain@c7b8fe6d. It works, and it is sound.Test: a structural netlist with an opaque cell (pins only, no
function), real
logic both feeding it and downstream of it, compared against itself and against
variants with a deliberate difference.case boundary result self-compare none 50.00% (1/2)— the opaque cone is skippedself-compare u uproves (rc=0) real difference downstream of the cell u uDifference was found(rc=3)real difference feeding the cell u uDifference was found(rc=3)real difference downstream none 50.00% (1/2)— not reported as a differencereal difference feeding none 50.00% (1/2)— not reported as a differenceTwo things worth separating out.
1. The feature does what we needed (this is the #245 ask): the opaque cone
becomes provable, and excluding the cell's behaviour does not mask differences
on either side of it. The "input pins become compared outputs" half is what
catches a difference in what feeds the cell — we verified both directions.2. The last two rows are the stronger result. Without a boundary, a real
functional difference inside an opaque cone is silently not checked: exit 1
with partial coverage, never exit 3. So the opaque-cell skip does not merely
reduce coverage, it can hide a real mismatch. That is a better argument for the
feature than the one we made in #245.Limitation that blocks our main case
The pair must resolve on both sides:
--set-as-boundary u does_not_exist -> SEC workflow failed: boundary instance path `does_not_exist` does not resolve at `does_not_exist`That is correct behaviour, but it means
set_as_boundarycannot reach a cell
that exists on only one side — which is exactly our blocking case. The gate-side
opaque cell isICGx1_ASAP7_75t_R, inserted by synthesis; there is no
corresponding instance in the RTL to pair it with.So for us:
our blocker covered by set_as_boundary?hardened blocks shipped as Liberty timing abstracts (no function)yes synthesis-inserted ASAP7 ICG (gate side only) no — nothing to pair Is a one-sided form conceivable — naming an instance in one design and letting
its output become a free input on both sides? That would be unsound in general,
so we are not asking for it lightly; it may be that clock-gate-aware handling is
the better answer for this specific shape.Addressing notes (may be worth a line in the docs)
form result sub/u— top-relative,/-separatedresolves bare leaf name when nested does not resolve escaped identifier passed without the backslash ( esc.inst)resolves escaped identifier passed as written in the netlist ( \esc.inst)does not resolve The last one is easy to trip over: a synthesised netlist writes
\name, but the
boundary path must drop the backslash.Scale
A real design needs one pair per macro instance, which is a lot of repeated
flags. Is there a bulk form — a wildcard, a cell-name match, or a file of pairs?
We have not yet tried a large boundary list; if useful we can report how it
behaves on the design you already have from us.
Summary
An
x(orz) literal anywhere in an expression makes SEC skip every output inthat cone, with a message about an "internal frontier term" that never mentions
the unknown value. Replacing the literal with
1'b0makes the same design pass.Don't-care assignment is ordinary RTL practice, and generators emit it heavily,
so on a real design this caps coverage near zero.
Reproducer
min_x.sv:min_0.sv— identical but for the else-arm:Compare each design against itself:
min_0.svcoverage: 100.00%,No binary-defined difference was foundmin_x.svcoverage: 0.00%min_z.sv(1'bz)coverage: 0.00%The failure for the
xcase isNothing in that message points at the unknown literal.
The same thing at RTL scale
The shape that led me here is the read port of a generated memory model:
Swapping
46'bxfor46'b0takes that module from 0% to 100% coverage.Suggested
what SEC already calls an environment input. A don't-care means synthesis may
produce anything there, so the natural reading is "unconstrained", and
equivalence can still be established wherever the value is defined.
location instead of reporting an unmapped frontier term. The current message
sends the reader looking for a connectivity problem that does not exist.
would be far cheaper than extracting both designs and then skipping every
output.
Note that the loader already reports lowering these:
Unknown literal bits in always_comb assignment RHS lowered as 0 in SNL (X/Z distinction is not preserved). Whatever that lowering produces is not being collected.