ASIC Point Explore

Modelling Code and Helper Assertions

Count outstanding requests in the bench, bind the counter as an assumption and as an assertion, and track one symbolic tag that stands for all of them.

Lesson
F3.6
Time
15 min
Runs on
SymbiYosys
Check
5 questions

A block allowed four outstanding requests, and its bench counted them in a helper register that someone bounded with assume(f_outstanding <= 4). The block's own counter was two bits wide and wrapped on the fourth accept, so it took a fifth request. The assumption deleted every world with five, the proof passed, and the design ran out of buffer in the lab.

Run B: the two-bit counter wraps and takes a fifth request
01234567clkfreereqackrespfreeresp_takeused012301f_outstanding012345first acceptused 0, four outstanding, ackf_outstanding 5SBY reports FAIL

Measured with smtbmc yices at depth 20. Five accepts on steps 1 to 5, no responses taken. Note resp falling at step 5: the design thinks it is empty.

Numbers the Design Keeps to Itself

Modelling Code Is Part of the CheckerThe bench computes what the properties need and the design does not export. It reads ports, and never drives anything the design reads. Arrows mean "feeds".
data: where the transaction goes
Modelling code is part of the checkerThe bench computes what the properties need and the design does not export. It reads ports, and never drives anything the design reads. Arrows mean "feeds". component Solver req, req_tag,resp_take component req4 four credits, a tagqueue component Modelling code f_outstanding, thef_tag tracker component Helper assertions claims about the DUT,proven component ack, resp,resp_tag ports component anyconst f_tag one value, fixed atstep 0 readsreads
Read the diagram as text
  • Solver: req, req_tag, resp_take
  • req4: four credits, a tag queue
  • Modelling code: f_outstanding, the f_tag tracker
  • Helper assertions: claims about the DUT, proven
  • ack, resp, resp_tag: ports
  • anyconst f_tag: one value, fixed at step 0
  • Solver → req4
  • req4 → ack, resp, resp_tag
  • ack, resp, resp_tag → Modelling code: reads
  • Solver → Modelling code: reads
  • anyconst f_tag → Modelling code
  • Modelling code → Helper assertions

No arrow runs from the modelling code back into the design. If one did, the checker would be changing what it checks.

Properties often need a number the design does not show: how many requests are outstanding, which byte was pushed fourth. Modelling code computes it in the bench, behind FORMAL: counters, trackers, shadow registers. It reads the design's ports, and for glue properties its state. It never drives anything. In a real project it lives in the bound checker module beside the properties (A7.1), so the RTL file never changes.

A Helper Is a Claim, so Assert It

Run A: the helper as a promise

assert property (@(posedge clk) disable iff (rst) ack |-> req);
assume property (@(posedge clk) disable iff (rst) f_outstanding <= 3'd4);

BMC PASS to depth 20, with the wrap bug in the RTL.

Run B: the helper as a claim

assert property (@(posedge clk) disable iff (rst) ack |-> req);
assert property (@(posedge clk) disable iff (rst) f_outstanding <= 3'd4);

FAIL at reported step 7.

f_outstanding is a claim about the design: accepts minus responses never exceed four. Written as an assumption, it constrains the design through the bench's own arithmetic, the master rule broken by a side door (F3.1). Written as an assertion, it is proven, and later it becomes an invariant for induction (F4.6).

RunMeasured resultTime
A: tracker assumed (bmc)BMC PASS to depth 20537 ms
B: tracker asserted (bmc)FAIL at reported step 7539 ms
Cover of a fifth accept, under the assumptioncover reached, reported step 6516 ms
Cover of a fifth accept, no assumptioncover reached, reported step 6519 ms
Fixed: a three-bit counter, tracker assertedBMC PASS to depth 20563 ms

req4 with the two-bit counter; depth 20, smtbmc yices, reset assumed in step 0.

The cover of a fifth accept is reached even under the assumption, at step 6. A cover trace stops at the covered sample, and an assumption binds only the samples inside it. There f_outstanding is still 4; the 5 it forbids is the next sample, after the trace ends. A cover you expected impossible came back reached: a bug report the bmc PASS was hiding.

One Symbolic Tag for All of Them

One tracked tag stands for every tag
0123clkfreereqfreereq_tag8000f_tag00f_tag_inrespfreeresp_takeresp_tag80request tagged 00 = f_tagresponse tag 80SBY reports FAIL

The tag-swap bug at depth 10. The solver chose f_tag = 00, the tag of the request it could break; any other choice is equally legal. The wrong response tag comes from a slot never written.

(* anyconst *) reg [7:0] f_tag; is a value the solver picks once, at step 0, and holds for the whole run. A tracker that follows the request carrying f_tag follows every request at once, because the solver may pick the worst one. (* anyseq *) is its partner: a fresh value every step, an input without a port.

Tag tracker runMeasured resultTime
Fixed design, depth 10BMC PASS to depth 10712 ms
Tag-swap bug, depth 10FAIL at reported step 3516 ms
Fixed design, depth 14BMC PASS to depth 1418091 ms

A tracker over data costs depth: compare the two depths on the same fixed design, measured on the authoring machine. On the shared server depth 14 exceeds the 20-second budget, so the editor keeps depth 10. F4.4 builds the formal scoreboard on this idea.

Asked in Interviews

QuestionAnswer
What is modelling code in a formal testbench?Bench logic that computes what the properties need and the design does not export. It is part of the checker.
Should a helper be an assume or an assert?An assert. It is a claim about the design, it gets proven, and it strengthens induction.
What is anyconst for?A symbolic constant: one tracked value that stands for every value.

Try It

In concurrent SVA over bench signals

assert property (@(posedge clk) disable iff (rst) f_outstanding <= 3'd4);
assert property (@(posedge clk) disable iff (rst) f_tag_in && f_ahead == 0 && resp && resp_take |-> resp_tag == f_tag);
cover property (@(posedge clk) !rst && req && ack && f_outstanding == 3'd4);

Claims about the design, read through the modelling code.

The tracker as the editor runs it

reg [2:0] f_outstanding=0;
always @(posedge clk)
  if (rst) f_outstanding <= 0;
  else f_outstanding <= f_outstanding
         + (req && ack) - (resp && resp_take);

Accepts minus responses, as the ports see them.

Depth 20 for the counter runs; the tag tracker runs use depth 10.
[options]
mode bmc
depth 20
[engines]
smtbmc yices
[script]
read_verilog -formal -sv design.sv
prep -top req4
[files]
design.sv

  1. Read the counter

    Find f_outstanding in the bench and say in one sentence what it counts.

  2. Run it as a promise

    Run as it is: BMC PASS to depth 20. Add the fifth-accept cover and run in mode cover.

  3. Change the verb

    Make the helper an assert: FAIL at reported step 7. Find the step where used reads 0 with four requests outstanding.

  4. Fix the width

    Widen used to three bits: BMC PASS to depth 20.

  5. Track one tag

    Add the f_tag tracker at depth 10, then break the response read. Which tag did the solver pick?

design.sv

props.sv

Use assert property (@(posedge clk) ...);. Leave blank for immediate assertions in the design.

Inputs are free unless constrained. Run to find a counterexample or check a proof.

Model: one positive-edge clock, binary data. Sampled history requires declaration-initialized variables; primary-input history is unsupported.

SBY summary and log

    
Check Yourself

      

        
Predict the outputreq4 with the two-bit counter, mode bmc, default depth 20, smtbmc yices, reset assumed in step 0, assume(f_outstanding <= 4) and the one assertion ack |-> req. The summary verdict is:
      
module req4(input clk, rst, req, input [7:0] req_tag, input resp_take,
  output ack, output resp, output [7:0] resp_tag);
  reg [7:0] tq [0:3];
  reg [1:0] wp=0, rp=0;
  reg [1:0] used=0;   // bug: two bits cannot hold four
  assign ack  = req && used < 3'd4;
  assign resp = used != 0;
  assign resp_tag = tq[rp];
  wire take = resp && resp_take;
  always @(posedge clk)
    if (rst) begin used <= 0; wp <= 0; rp <= 0; end
    else begin
      if (ack) begin tq[wp] <= req_tag; wp <= wp + 2'd1; end
      if (take) rp <= rp + 2'd1;
      used <= used + ack - take;
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // Modelling code: accepts minus responses, as the interface sees them.
  reg [2:0] f_outstanding=0;
  always @(posedge clk)
    if (rst) f_outstanding <= 0;
    else f_outstanding <= f_outstanding + (req && ack) - (resp && resp_take);
  always @(posedge clk) if (!rst) begin
    assert(!ack || req);   // no acknowledge without a request
    assume(f_outstanding <= 3'd4);
  end
`endif
endmodule


      

      

      


Predict the outputThe same design and assumption, mode cover, default depth 20, with cover(req && ack && f_outstanding == 4), a fifth accept. The cover result is:
      
module req4(input clk, rst, req, input [7:0] req_tag, input resp_take,
  output ack, output resp, output [7:0] resp_tag);
  reg [7:0] tq [0:3];
  reg [1:0] wp=0, rp=0;
  reg [1:0] used=0;   // bug: two bits cannot hold four
  assign ack  = req && used < 3'd4;
  assign resp = used != 0;
  assign resp_tag = tq[rp];
  wire take = resp && resp_take;
  always @(posedge clk)
    if (rst) begin used <= 0; wp <= 0; rp <= 0; end
    else begin
      if (ack) begin tq[wp] <= req_tag; wp <= wp + 2'd1; end
      if (take) rp <= rp + 2'd1;
      used <= used + ack - take;
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // Modelling code: accepts minus responses, as the interface sees them.
  reg [2:0] f_outstanding=0;
  always @(posedge clk)
    if (rst) f_outstanding <= 0;
    else f_outstanding <= f_outstanding + (req && ack) - (resp && resp_take);
  always @(posedge clk) if (!rst) begin
    assert(!ack || req);   // no acknowledge without a request
    assume(f_outstanding <= 3'd4);
    c_fifth: cover(req && ack && f_outstanding == 3'd4);
  end
`endif
endmodule


      

      

      


ConceptWhich bench line is the wrong one?


ConceptWhat is anyconst?


Read the waveformIn run B, at which step does the design's counter used read 0 while four requests are outstanding?
Run B: the two-bit counter wraps and takes a fifth request

    
  01234567clkfreereqackrespfreeresp_takeused012301f_outstanding012345first acceptused 0, four outstanding, ackf_outstanding 5SBY reports FAIL
Measured with smtbmc yices at depth 20. Five accepts on steps 1 to 5, no responses taken. Note resp falling at step 5: the design thinks it is empty.

        

        
      

    

    
Remember
  • Modelling code computes what properties need and the design does not export; it reads, it never drives.
  • A helper is a claim about the design: assert it. As an assumption it hides bugs through the bench's arithmetic.
  • A cover trace stops at the covered sample; an assumption that only the next sample would break cannot hide it. A cover you expected impossible, reached, is a bug report.
  • anyconst is a value fixed once by the solver; one tracked value stands for all values.