An Assertion That Wasn’t Evaluated Did Not Pass

A green simulation log is meaningless if the property you depended on was never evaluated.

Concurrent SystemVerilog assertions contain some of the most valuable checks in a verification environment.

Consider this property:

property req_ack;
  @(posedge clk)
    req |-> ##[1:3] ack;
endproperty

assert property (req_ack);

It requires an acknowledgement to arrive one to three cycles after a request.

If a simulator cannot lower the cycle-delay range, it has three choices:

Reject the property
Warn and skip it
Silently skip it

Only the first choice is safe by default.

If the simulation continues without evaluating the assertion, a clean run may look like a pass even though the intended behaviour was never checked.

Use a planted failure as proof of evaluation

A reliable assertion test should include a negative control:

Many valid handshakes
+
One deliberate violation

The planted failure proves that the property is active.

If the simulator reports an all-pass result, the next question should be:

Did the property genuinely pass, or was it never evaluated?

A pass count without an evaluated count cannot answer that question.

Track the complete assertion lifecycle

FSimX separates assertion activity into five categories:

evaluated — lowered, armed and checked
skipped   — parsed but not evaluated
passed    — substantive successful evaluations
failed    — detected violations
vacuous   — antecedent never triggered

The verdict policy is intentionally strict:

skipped > 0 → PASS is forbidden
failed  > 0 → Run exits non-zero

A skipped assertion remains unproven. It cannot contribute to a successful verdict.

Vacuous is not the same as passed

Consider:

req |-> ##1 ack

If req never becomes true, the assertion may be vacuously satisfied. No violation occurred—but the stimulus also never exercised the behaviour.

That result can be useful diagnostically:

High vacuity
→ Antecedent rarely or never triggered
→ Stimulus may not be testing the intended scenario

Combining vacuous and substantive passes into one number would exaggerate how much behaviour was actually checked.

Make the result machine-readable

The same assertion ledger should be available to CI pipelines and reporting systems:

{
  "assertions": {
    "evaluated": 2,
    "skipped": 0,
    "passed": 815,
    "failed": 1,
    "vacuous": 0
  }
}

This allows automation to enforce the same rules as the human-readable log.

A pipeline can fail when:

assertions.skipped > 0
assertions.failed > 0

That prevents an unsupported or dropped property from disappearing inside a green build.

Compare evaluation—not parsing

Simulator capability should be measured by whether a property was executed, not merely accepted as source text.

The SVA comparison distinguishes evaluated properties from properties the tested tool versions could not compile.

Version-scoped comparison matters because assertion-language support evolves. A reproducible result should identify the exact tool release, property and workload being tested.

See the negative control and full assertion evidence

The complete WIOWIZ study includes:

• The ranged-delay SVA probe
• A deliberately planted violation
• Version-specific simulator results
• Machine-readable assertion counts
• Vacuity measurements
• Larger assertion workloads
• Strict CI verdict behaviour

👉 Read the full study: An Assertion That Wasn’t Evaluated Did Not Pass

#systemverilog #verification #testing #semiconductor