Capstone: an assertion suite

What the Verify problems ask

The problems that follow this lesson give you a design, a stimulus that you do not control, and a bank of variants: one correct design and several faulty ones. You write the assertions.

Your suite is scored on two counts. It must report at least one failure on every faulty variant, and it must report none on the correct design. A suite that fails the correct design is wrong, however many faults it catches.

The FIFO under test

The design is hardware_fifo, the problem bank's FIFO, which Module 7 built and checked with a scoreboard. It has DEPTH entries of WIDTH bits. The data pins are 32 bits wide, and only the low WIDTH bits are stored.

At each rising edge, both requests are decided from the number of items held before the edge. A write is accepted when the FIFO is not full, and a read when it is not empty. An accepted read is answered after that edge: read_valid is 1 for one cycle, and read_data holds the oldest item.

reset is synchronous and active high. At a reset edge the FIFO empties, clears read_valid and accepts nothing. The problem bank's fixture also pulses an initialize pin once at the start, which clears everything as a reset does.

From spec to rule list

Start from the specification, one sentence at a time, exactly as lesson A1.1 did. Each sentence becomes one labelled assertion, and each assertion uses the smallest set of operators that states it.

Every rule except the last carries disable iff (initialize || reset), because a reset edge legally breaks it. The reset rule checks reset itself, so only initialize disables it, as lesson A3.5 recommended.

Two rules look one edge ahead with |=>, because the FIFO registers its answer. A rule written with |-> would compare the answer at the same edge as the read, and fail on the correct design.

What a fault bank contains

Each faulty variant breaks one sentence of the specification, in the way real designs break. Knowing the usual faults helps you check that your rule list covers them.

A fault can only be caught where the stimulus exposes it. A pointer that wraps in the wrong place does no harm until the FIFO has taken more writes than it has slots.

A model for the data rules

The rules need to know how many items the FIFO should hold and which item a read should return. A few lines of auxiliary code keep that: a count n, a queue of the values written, and exp_data, the item the last accepted read removed.

The model decides acceptance from its own count, take_r = read_en && n > 0, exactly as the specification does. It never reads the FIFO's internal used or its pointers, even though a bound module could. A model that copies the design's state copies its bugs too.

Update the model with nonblocking assignments at the clock, as lesson A2.2 advised. At the edge after a read, the sampled exp_data then holds the item that read removed, ready to compare with read_data.

Checking the suite itself

Every assertion should be shown to fail at least once, on purpose. Bind the suite to a faulty variant, or force a violation in a small test, and check that the right rule fires at the right edge.

Check that every antecedent matches during the tests, as lesson A1.3 showed. A rule that never triggers scores nothing, because it cannot catch a fault.

// no reset guard, antecedent too wide
assert property (@(posedge clk)
  read_en |=> read_valid);

assert property (@(posedge clk)
  disable iff (initialize || reset)
  take_r |=> read_valid);

Working inside the simulator's limits

The problems run on the same simulator as this track, so the same runnable subset applies. Put any waiting at the end of the consequent with ##[m:n], until_with or s_eventually, and keep antecedents of fixed length. Write one implication per rule, and count events with auxiliary counters rather than gotos. A submission outside that subset is refused before it runs.

Report each failure through the fail action, as the examples do. The problems count failures per variant, so each assertion only needs to fail; it does not need to print anything in particular.

An order of work

1. List the rules

   Write one line per spec sentence, in plain words, before writing any SystemVerilog.

2. Write and label the assertions

   Use the smallest operator set for each rule, with a reset guard only where reset can break it.

3. Run on the correct design

   The suite must be silent. Any failure here is a rule that disagrees with the spec, so fix the rule first.

4. Run on known faults

   Break the design on purpose, one sentence at a time, and check that the matching rule fires at the right edge.

5. Count the triggers

   Check that every antecedent matched at least once, so that no rule passed only vacuously.

Reading a variant's result

When a variant is caught, look at which rule fired first and at what edge. The first failure usually names the fault, while later failures are its consequences, such as the wrong data that follows a pointer wrapping in the wrong place.

When a variant is missed, ask which spec sentence it breaks and whether your suite states that sentence at all. Missing rules are far more common than wrongly written ones.

Try it

The same suite, bound to all four FIFOs, stayed silent on the correct one. Fault 2 left read_valid high after the last read, so no_extra failed at the two edges before the reset cleared it. Fault 4 answered late: answered failed for the two reads that did not follow another read, and in_order for all five.

Fault 6 sent the fourth write to a spare slot, so the read of 0x15 returned the stale 0x10 and only in_order saw it. Delete the op(1, 1, 'h15) line and predict the fault 6 line.

Check yourself

module tb;
  bit clk = 0;
  always #5 clk = ~clk;                  // rising edges at 5, 15, 25, ...
  bit take_r = 0, read_valid = 0;        // stimulus changes at falling edges
  int f_answer, f_extra;
  answered: assert property (@(posedge clk) take_r |=> read_valid) else f_answer++;
  no_extra: assert property (@(posedge clk) !take_r |=> !read_valid) else f_extra++;
  initial begin
    @(negedge clk); take_r = 1;          // a read is accepted at 15
    @(negedge clk); take_r = 0;
    @(negedge clk); read_valid = 1;      // its answer is seen at 35
    @(negedge clk); read_valid = 0;
    #2 $display("answered=%0d no_extra=%0d", f_answer, f_extra);
    $finish;
  end
endmodule

!(full && empty)

take_r |=> read_valid && read_data == exp_data

!take_r |=> !read_valid

take_r |=> read_valid

Practice

• A read-channel assertion suite Verify · Hard