Why an assertion passes without testing its intended behavior

How-to Last tested 24 October 2026

A passing implication is useful only if its trigger occurred while the assertion was enabled. Record trigger coverage alongside failures, and distinguish a response that met its obligation from a run that created no obligation at all. Reset disabling and sampled values add two more questions: whether an attempt was cancelled, and which clock edge supplied the value being compared.

Give the assertion an observable obligation

Start with a requirement that can be stated without language syntax: when a request is sampled outside reset, an acknowledgement must be sampled on the following rising edge. The printed example expresses that one-cycle obligation with non-overlapped implication. It also counts requests independently and places a cover property on the antecedent. The three observations answer different questions: was the initiating condition seen, did the response satisfy the requirement, and did an independent counter agree with the cover result?

A zero failure count by itself cannot answer the first question. In mode 2, every active edge has request low. The property produces no failure, but its trigger cover and request counter both remain zero. Calling that a verified request-response path would turn absence of stimulus into evidence of correct response. Here, “vacuous pass” describes the logical implication when its antecedent is false; the recorded simulator output contains counters, not a dedicated vacuity report.

The same distinction matters when copying an assertion from a block into a larger integration. An address decoder, a disabled feature or an over-restrictive stimulus constraint can prevent the trigger from reaching the property. A successful regression can then repeat the same empty obligation many times. Inspect trigger reachability at the integration boundary before interpreting the assertion as evidence about the responder. The block-to-SoC guide adds software-visible scenarios to that boundary check.

Run one source in five modes

Save the complete source below as example.sv, or download the exact source. The commands and expected interpretations select each mode from the same compiled model. The source drives inputs on falling edges so the next rising-edge sample is deliberate; it does not rely on a testbench assignment racing an assertion at the sampling edge.

// SPDX-License-Identifier: MIT
`timescale 1ns/1ps
module tb;
  bit clk = 0;
  bit reset = 1;
  bit request = 0;
  bit acknowledge = 0;
  bit [7:0] data = 0;
  int mode = 0;
  int active_samples = 0;
  int trigger_count = 0;
  int implication_failures = 0;
  int sampled_failures = 0;
  always #5 clk = ~clk;

  Reply: assert property (@(posedge clk) disable iff (reset)
    request |=> acknowledge)
    else begin
      implication_failures++;
      $display("REPLY_FAIL t=%0t", $time);
    end
  Trigger: cover property (@(posedge clk) !reset && request);
  PreviousData: assert property (@(posedge clk) disable iff (reset)
    acknowledge |-> data == $past(data) + 8'd1)
    else begin
      sampled_failures++;
      $display("SAMPLED_FAIL t=%0t", $time);
    end

  always @(posedge clk) begin
    if (!reset) begin
      active_samples++;
      if (request) trigger_count++;
    end
  end
  task automatic drive(input bit r, input bit a, input bit rst,
                       input bit [7:0] value);
    @(negedge clk);
    request = r;
    acknowledge = a;
    reset = rst;
    data = value;
  endtask
  initial begin
    if (!$value$plusargs("MODE=%d", mode)) mode = 0;
    drive(0, 0, 0, 8'd10);
    if (mode == 2) begin
      drive(0, 0, 0, 8'd11);
      drive(0, 0, 0, 8'd12);
    end else begin
      drive(1, 0, 0, 8'd20);
      if (mode == 3) drive(0, 0, 1, 8'd21);
      else if (mode == 1) drive(0, 0, 0, 8'd21);
      else if (mode == 4) drive(0, 1, 0, 8'd25);
      else drive(0, 1, 0, 8'd21);
    end
    drive(0, 0, 0, 8'd30);
    drive(0, 0, 0, 8'd31);
    @(negedge clk);
    $display("RESULT mode=%0d active=%0d triggers=%0d reply_fail=%0d sampled_fail=%0d",
      mode, active_samples, trigger_count,
      implication_failures, sampled_failures);
    if (mode == 1 && implication_failures != 1) $fatal(1, "Expected reply failure");
    if (mode != 1 && implication_failures != 0) $fatal(1, "Unexpected reply failure");
    if (mode == 4 && sampled_failures != 1) $fatal(1, "Expected sampled failure");
    if (mode != 4 && sampled_failures != 0) $fatal(1, "Unexpected sampled failure");
    if (mode == 2 && trigger_count != 0) $fatal(1, "Expected no trigger");
    if (mode != 2 && trigger_count != 1) $fatal(1, "Expected one trigger");
    $finish;
  end
endmodule

Mode 0 sends one request and acknowledges it on the next rising edge. Mode 1 sends the same request but omits the acknowledgement. Mode 2 never sends a request. Mode 3 raises reset before the response sample, cancelling that pending assertion attempt. Mode 4 acknowledges on time but changes data by five rather than the required one. No mode requires changing the source or removing a failing property.

The failure actions count and print the expected failures instead of stopping at the first assertion. The final checks then verify that the chosen mode produced the intended pattern. Consequently, a zero process exit code for mode 1 means the demonstration successfully detected its deliberate failure. It does not mean the request-response property passed. Keep that distinction when importing these outputs into an automated report.

Read trigger and failure counts together

The following values came from the same Verilator 5.052 executable with assertions and user coverage enabled. “Cover” is the Trigger cover-property count written by Verilator; “requests” is the independent testbench count. Neither column is line, toggle or branch coverage.

A useful report retains the mode, source hash, assertion options and these separate counts. A dashboard that collapses all five rows into “exit code zero” would erase the reason for running them. Conversely, marking every printed failure as an unexpected test failure would misclassify the two deliberate negative cases. The expected outcome belongs to the test definition, while the literal assertion result belongs to the evidence.

Treat reset as part of the requirement

disable iff (reset) does more than add a convenient guard to a failure message. In the reset mode, a request is observed before reset, yet no later reply failure is counted because that attempt is disabled. A nonzero antecedent count therefore still does not establish a completed obligation. The useful combination is trigger evidence, a known reset history and a check that the required response window was actually reached.

Do not silently choose reset behavior for a real interface. Some requirements permit abandoning in-flight work on reset; others require recovery, error reporting or replay. An assertion that disables every difficult transition may accurately implement its syntax while omitting the requirement you intended to test. Write down which events reset cancels, what becomes invalid, and when checking restarts. The power-boundary example makes reset and restoration ordering explicit in a different context.

This example changes reset away from the rising sample edge. It does not exercise all event-region corner cases, asynchronous reset glitches or release ordering. Its observed cancellation is sufficient to demonstrate why a trigger count cannot stand in for a completed check. It is not evidence that every reset interaction in another design has been covered.

Make the sampled value visible

The second assertion compares acknowledged data with the previous sampled data plus one. The passing case moves from 20 to 21; the deliberate mismatch moves from 20 to 25. The resulting SAMPLED_FAIL message identifies a data-relation failure while the reply-timing counter remains zero. That separation keeps a timely but wrong response from being reported as a transport timeout.

For a larger checker, document whether a value belongs to the request edge, response edge or an intervening pipeline stage. Guard any use of history until the relevant earlier sample exists, and decide how reset clears that history. A current procedural value printed after an edge need not be the same value used by a sampled assertion. The source avoids that ambiguity by fixing stimulus between sample edges and using a one-step relationship that can be checked by inspection.

Keep unsupported results in the record

The identical source was offered to Icarus 13.0 with SystemVerilog assertions enabled. It did not compile. Among its literal diagnostics was sorry: concurrent_assertion_item not supported. Its syntax errors around the implication and sampled-value property are preserved in the run record. No Icarus pass, vacuity count or runtime behavior is inferred from that failed compilation.

Icarus documents separate assertion-generation switches, including an option that enables only supported assertions¹. Turning assertions off to obtain a successful executable would not validate this page’s checks. Verilator likewise documents partial assertion support, so the five observed cases establish support for these specific constructs and options rather than for every assertion in the language². The language reference is IEEE 1800-2023; this Verilator run selected --language 1800-2012. Implementation support, the selected language mode and the reference standard are different things³.

Use the simulator observation reference for other bounded comparisons. When moving this example into another simulator, retain the deliberate failing and never-triggered modes. They are practical checks that the properties were enabled and that the report still distinguishes a missing trigger from a satisfied response.

Not covered on this page

• Exhaustive or formal proof of request-response behavior.
• All SystemVerilog sequence, vacuity or event-region features.
• Analog reset integrity or metastability behavior.
• UVM execution or commercial-simulator comparisons.