A concurrent assertion parsed and then dropped is an unproven property, not a passing check.
It is an unchecked property wearing a green light.
FSimX evaluates them, counts them, and refuses to print PASS if any were skipped.
Concurrent SystemVerilog assertions are where a lot of verification value lives and where a lot of it silently leaks away. A property like req |-> ##[1:3] ack looks small, but a simulator that cannot lower the cycle-delay range has three options: refuse to compile, warn and drop it, or drop it quietly. Only the first is safe. The other two produce a run that looks clean while the property that mattered was never checked. This article is about evaluating assertions rather than skipping them, and about making the count impossible to hide.
The probe: 200 passes and one planted failure
The test is a WIOWIZ-original SVA probe. It drives 200 satisfying handshakes and exactly one engineered violation, a negative control whose job is to prove the assertion is being evaluated rather than passing vacuously. If a tool reports all-pass on this probe, it either caught the planted failure or it never evaluated the property at all, and the count tells you which.
FSimX lowers the property and evaluates it every clock edge. It catches the planted violation at 6065 ns and exits nonzero because an assertion failed:
$ fsxrun -sv sva_probe.sv -top tb # property: req |-> ##[1:3] ack FSX-S1006: 2 concurrent SVA assertion(s) lowered and EVALUATED Assertions: 815 passed, 1 failed -> violation caught at 6065 ns (the engineered negative control) run verdict FAIL (exit 2) strict: an assertion failed
On the versions tested, neither of the two open-source reference simulators reaches evaluation on the full property. Verilator refuses the cycle-delay range at compile time (Unsupported: ## range cycle delay range expression); Icarus Verilog cannot parse the property block at all (Invalid module item). Reduce the property to the simpler req |=> ack and Verilator does evaluate it, and then it agrees with FSimX to the nanosecond, catching the same violation at the same 6065 ns. That agreement is the point of a reference: where Verilator evaluates, FSimX matches it exactly, which is how the engine confirms it is right. Where FSimX evaluates the fuller property and the reference does not, the gap is language coverage, not engine correctness.
The count that cannot be hidden
Evaluating assertions is only half the discipline. The other half is making the evaluated-versus-skipped split a first-class output, so a dropped property cannot masquerade as a passing one. FSimX prints this in the human verdict block and, as of the current release, emits it as machine-readable JSON next to the verdict so downstream tools read the same truth the log shows.
Each field maps to a source the log already reports. evaluated is the count of concurrent assertions lowered and armed. skipped is the count parsed and then dropped, each one an unproven property. passed and failed are the pass and fail tallies. vacuous counts the assertions whose antecedent never matched, kept deliberately separate from passed so a property that never triggered cannot pad the pass rate. Downstream consumers read skipped > 0 as an unproven verdict, the same policy the verdict banner enforces.
"assertions": { "evaluated": 2, "skipped": 0, "passed": 815, "failed": 1, "vacuous": 0 }
Vacuity is not a pass
The vacuous count is where most quiet false passes hide, so it earns its own field. On the DeepFuse sensor-fusion testbench, FSimX lowers 15 concurrent assertions and reports them like this over a bounded window:
DeepFuse: 15 concurrent SVA lowered + evaluated 39 passed, 0 failed, 1980 vacuous
Nineteen hundred and eighty of those evaluations were vacuous - the antecedent never fired in the window, so the property was never actually tested by this stimulus. Vacuity is not automatically useless: some properties are legitimately vacuous over a given run, and the count itself is diagnostic ("your stimulus never provoked this property"). What matters is that a reviewer sees 39 substantive evaluations and 1,980 vacuous ones as separate numbers, not one wall of 2,019 that would over-state what was actually checked.
Where it holds at scale
The same ledger applies at scale. On the chiplet S3 (L2) adapter (WIOWIZ-original TileLink-to-UCIe), FSimX evaluates the checker to checks_pass=766 checks_fail=0, matching Icarus Verilog check for check. FSimX also evaluates the shared assertion library from a widely used open-source silicon-verification suite, including variable-length in-band-initialisation sequences of the form A ##1 B[*1:$] ##1 C[*3] |=> D, lowered as an exact subset-construction automaton. On a representative test from that suite, roughly 450 concurrent assertions are lowered and evaluated on every clock edge, and every one of them appears in the ledger.
The strict exit is the other half of the contract. When an assertion fails, the run exits nonzero by policy, so a failed property cannot be lost in a green build log. The rule the ledger enforces: evaluate the property, count what was evaluated and what was skipped, keep vacuous separate from passed, and forbid a PASS when anything was skipped.
The ledger separates evaluated from skipped, and vacuous from passed, so the number a reviewer reads is the number that was actually checked.
Backing numbers
- SVA probe (req |-> ##[1:3] ack): 815 passed, 1 failed, violation at 6065 ns; open-source references do not compile the range on tested versions
- Reduced probe (req |=> ack): Verilator agrees to the nanosecond, same 6065 ns
- Ledger fields: evaluated, skipped, passed, failed, vacuous; skipped > 0 forbids PASS
- DeepFuse: 15 SVA lowered, 39 passed, 0 failed, 1980 vacuous kept separate
- chiplet S3 (L2): 766/766 checks, matches iverilog; ~450 assertions/edge on a full DV test
Run it yourself - FSiMX Studio
The native FSiMX engine described in this article ships in FSiMX Studio, a Docker bundle from the WIOWIZ website. Download it, build the image, and run the same elaboration, four-state and assertion behaviour you saw here, with vWIZ-Wave and vWIZ-Coverage in the same window.
Download FSiMX Studio on wiowiz.ai →
Our Approach
We're building systems that think about specifications the way engineers do.
We build our own in-house EDA with an intelligence layer across it. Our stack covers the full flow,
from spec to comprehensive sign-off, on tools we build and control.
Walk-in ones, walk-in zeros