The directive is the top layer: it takes a property and tells the tool what to do with it. The same text can be checked, used as a constraint, counted as a scenario, or used to prune the formal state space.
The four verbs mean different things to a simulator and a formal tool. Knowing both columns is what the interview question asks for.
Directive | Simulation | Formal |
|---|---|---|
| Checks, reports violations | Proves the property for all legal traces |
| Checked exactly like assert | Constrains inputs to legal traces |
| Counts matches, never reports | Searches for a witness trace |
| Ignored entirely, no cost | Constrains like assume |
The listing below runs. Two changes from the textbook form: the cover writes full ##1 ~full, because Verilator 5.048 rejects ! after ##1, and every directive counts in its action block so a bench can plant bugs and keep going.
module fifo_verbs (
input logic clk,
input logic rst_n,
input logic push, full, pop, empty,
input logic [1:0] mode,
output int overflows, bad_pops, full_drains
);
// 1. assert: the DUT obligation
ap_no_overflow: assert property (@(posedge clk) disable iff (!rst_n)
!(push && full)) else overflows++;
// 2. assume: an environment contract; simulation checks it like an assert
am_pop_legal: assume property (@(posedge clk) disable iff (!rst_n)
!(pop && empty)) else bad_pops++;
// 3. cover: the interesting scenario happened ("~full": Verilator rejects "!" after ##1)
cp_full_drain: cover property (@(posedge clk) disable iff (!rst_n)
full ##1 ~full) full_drains++;
// 4. restrict: formal case split; simulation ignores it
rs_mode: restrict property (@(posedge clk) mode == 2'b01);
initial begin overflows = 0; bad_pops = 0; full_drains = 0; end
endmodule
module tb_verbs;
logic clk = 0;
always #5 clk = ~clk;
logic rst_n = 0, push = 0, full = 0, pop = 0, empty = 1;
logic [1:0] mode = 2'b11; // breaks the restrict on purpose
int overflows, bad_pops, full_drains;
fifo_verbs chk (.*);
initial begin
repeat (2) @(negedge clk);
rst_n = 1;
@(negedge clk); empty = 0; full = 1; // full, nothing pushed
@(negedge clk); push = 1; // planted: push while full
@(negedge clk); push = 0; full = 0; // full drains
@(negedge clk); empty = 1; pop = 1; // planted: pop while empty
@(negedge clk); pop = 0;
repeat (2) @(negedge clk);
$display("assert: %0d overflow; assume: %0d illegal pop; cover: %0d full-then-drain; restrict: ignored (mode 3 all along)",
overflows, bad_pops, full_drains);
if (overflows != 1 || bad_pops != 1 || full_drains != 1) $fatal(1, "FAIL: directive counts");
$display("PASS: assert and assume each caught their planted bug, the cover counted once, and restrict stayed silent");
$finish;
end
endmoduleassert: 1 overflow; assume: 1 illegal pop; cover: 1 full-then-drain; restrict: ignored (mode 3 all along)
PASS: assert and assume each caught their planted bug, the cover counted once, and restrict stayed silentAssume versus restrict in one line: both constrain formal, while simulation checks assume and ignores restrict. Use restrict for case splits that simulation should not be forced to obey.
An assert or assume takes an optional action block: a pass statement, an else fail statement, or both. Action blocks are procedural code in the Reactive region, so they can call tasks, count, or dump state.
Actions run with current values, while the attempt was decided on sampled values. Signals may have moved on, so print sampled values with $sampled when exactness matters. Fail actions of windowed properties run at the window end, so include the attempt start time in the message.
// snippet
// fail actions carry the triage payload: count, timestamp, and cause
// ap_req_ack: assert property (@(posedge clk) disable iff (!rst_n)
// req |-> ##[1:3] ack)
// else begin
// err_count++;
// $error("req with no ack in 3 cycles (count %0d)", err_count);
// endThe bench above already uses counting actions. Restrict needs no planted bug: mode sits at 3 for the whole run, and simulation never looks at it.
Severity answers what a nightly regression should do. Error is the default severity of a failing assertion with no action block, and fatal stops a simulation whose later output would be noise.
Task | Simulation | Regression meaning |
|---|---|---|
| Continues | Never fails a test |
| Continues | Counted, usually non-fatal |
| Continues on most simulators; Verilator 5.048 stops at the first one unless run with | Fails the test |
| Stops immediately | Aborts a meaningless run; the first argument is the |
The identifier before the colon is the label. It appears in failure messages, coverage reports, and tool on-off controls, so treat labels as interface: stable, greppable, and prefixed by directive type.
// snippet
// prefix encodes the directive: ap_ assert, am_ assume, cp_ cover, rs_ restrict
// ap_fifo_no_overflow: assert property (p_no_overflow);
// cp_fifo_wrap: cover property (p_wrap_around);
// labels enable surgical simulation control around error injection
// initial begin
// $assertoff(0, top.dut_wrap.ap_fifo_no_overflow);
// // ... injection scenario ...
// $asserton(0, top.dut_wrap.ap_fifo_no_overflow);
// endExactly what assert does: it checks that the stimulus honors the environment contract. Only in formal does it switch roles to a constraint on the explored traces.
Over-constraining. An assume or restrict excluded the trace simulation generated, so the proof holds for a smaller input space than the testbench uses.
Run with Verilator 5.048 (--binary --timing --assert, plus --coverage when a listing has a cover property) on 2026-10-18; every bench printed the PASS line shown. Verilator stops at the first $error or failing assertion without an action block, so the benches count failures in the action block. Icarus 13 has no concurrent assertions.
Verilator 5.048 rejected full ##1 !full; the bench writes full ##1 ~full.