Skip to main content

Assertion-Based Checking

Concurrent Assertions named this topic directly as where scoreboard-based checking gets a complementary strategy: assertion-based verification (ABV), catching protocol and timing violations at the exact cycle they happen, at the pins, independent of whether the generator/driver/monitor/scoreboard pipeline built across this topic is even running correctly.

A protocol invariant the scoreboard can't see​

The scoreboard checks data — does the value that came out match what should have. It has no opinion on whether the FIFO's status pins ever violate their own protocol. full and empty should never both be asserted at once (a FIFO with any depth can't be simultaneously completely full and completely empty) — a genuine invariant, checkable every single cycle with no dependency on any transaction ever completing:

module fifo_protocol_checker (
input bit clk,
input bit rst_n,
input logic full,
input logic empty
);
property full_empty_mutex;
@(posedge clk) disable iff (!rst_n) !(full && empty);
endproperty

assert property (full_empty_mutex)
else $error("Protocol violation: full and empty asserted simultaneously");
endmodule

A second invariant, in an extended checker: no write while full, no read while empty​

full_empty_mutex isn't the only protocol rule this FIFO's pins carry — a well-behaved driver should never assert wr_en while full is already high, or rd_en while empty is already high. Checking that needs two more input ports (wr_en, rd_en) beyond what fifo_protocol_checker above declares, so it's shown here as its own separate, extended checker module rather than a change to the one above:

module fifo_protocol_checker_ext (
input bit clk,
input bit rst_n,
input logic wr_en,
input logic full,
input logic rd_en,
input logic empty
);
property no_write_when_full;
@(posedge clk) disable iff (!rst_n) !(wr_en && full);
endproperty

property no_read_when_empty;
@(posedge clk) disable iff (!rst_n) !(rd_en && empty);
endproperty

assert property (no_write_when_full)
else $error("Protocol violation: wr_en asserted while full");

assert property (no_read_when_empty)
else $error("Protocol violation: rd_en asserted while empty");
endmodule

These catch a different bug class than full_empty_mutex: not an impossible state the FIFO itself entered, but an illegal action the driver attempted against a state the FIFO correctly reported. If the driver has a bug that ignores full/empty entirely — say, a missing guard before asserting wr_en — the scoreboard might still never notice, since it only compares data that actually made it through a completed write/read; fifo_protocol_checker_ext's two properties catch the illegal attempt itself, at the exact cycle it happens, regardless of what (if anything) the FIFO does in response. Both checkers can be bound to sync_fifo at once — nothing about bind limits a target module to a single bound checker.

Attaching it without touching the DUT​

bind sync_fifo fifo_protocol_checker checker_inst (
.clk(clk), .rst_n(rst_n), .full(full), .empty(empty)
);

bind is new here, and worth explaining directly: it attaches a module — fifo_protocol_checker, here — to every instance of a target module (sync_fifo) without editing that target's source at all. The DUT has no idea the checker exists; it's purely observational, wired to the exact same ports an ordinary instantiation would use. This is the standard way to attach non-intrusive protocol checking to a DUT whose source you don't want to (or can't) modify directly.

Why this doesn't replace the scoreboard, and vice versa​

Exactly the framing Concurrent Assertions closed with, now made concrete with a real component built on both sides:

  • The assertion catches protocol/timing violations at their exact source cycle — full/empty both asserted, the moment it happens, with the exact signal values already in the error message. It has no idea whether the data flowing through the FIFO is correct — it never looks at wr_data/rd_data at all.
  • The scoreboard catches whether the FIFO's actual data behavior was correct — but only once a full write-then-read round trip completes, and only for data content, never for protocol-level pin behavior.

A real verification environment runs both, always, not one instead of the other — each one is blind to exactly the class of bug the other one exists to catch.

What's next​

Every checking mechanism this topic needs now exists — a reference model, a scoreboard, and a protocol-level assertion, independent of each other. Section E composes everything built so far — generator, driver, monitor, reference model, scoreboard — into one environment, launched concurrently, plus the top-level test that drives it.