Summary
An x (or z) literal anywhere in an expression makes SEC skip every output in
that cone, with a message about an "internal frontier term" that never mentions
the unknown value. Replacing the literal with 1'b0 makes 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:
module t(input en, input a, output y);
assign y = en ? a : 1'bx;
endmodule
min_0.sv — identical but for the else-arm:
module t(input en, input a, output y);
assign y = en ? a : 1'b0;
endmodule
Compare each design against itself:
kepler-formal -sv --design1 <f> --design2 <f> \
--sv_design1_top t --sv_design2_top t -v sec --sec-engine pdr
| module |
result |
min_0.sv |
coverage: 100.00%, No binary-defined difference was found |
min_x.sv |
coverage: 0.00% |
min_z.sv (1'bz) |
coverage: 0.00% |
The failure for the x case is
- y[0]: design0 no-driver connectivity: encountered internal frontier term N
that was not collected as a primary input
Nothing 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:
assign R0_data = R0_en ? Memory[R0_addr] : 46'bx;
Swapping 46'bx for 46'b0 takes that module from 0% to 100% coverage.
Suggested
- Treat an unknown literal as unconstrained — a free variable, which is
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.
- Failing that, say what happened: name the unknown literal and its
location instead of reporting an unmapped frontier term. The current message
sends the reader looking for a connectivity problem that does not exist.
- If X handling is deliberately out of scope, rejecting the input up front
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.
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.