Packaging and binding

Named sequences and properties

A sequence declaration names a sequence, and a property declaration names a property. sequence beat_then_last; (rvalid && rready) ##1 rlast; endsequence lets every rule say beat_then_last instead of repeating the timing.

Both can take arguments, like functions. property needs_valid(logic sig); sig |-> rvalid; endproperty serves rlast, ruser and any other signal that is only meaningful with rvalid.

A named sequence can be used inside other sequences, so small pieces build up into larger rules. Give each one a name that reads well inside a property, such as burst_done.

Range bounds such as ##[0:MAX_STALL] must be constants known when the design is elaborated, so they come from parameters rather than from property arguments.

Naming an expression with let

Many rules share a plain condition with no timing in it, such as "the beat is stalled". let stalled = rvalid && !rready; names that expression once. Every assertion that writes stalled gets the same definition, and a fix reaches all of them.

let can take arguments, let in_window(x, lo, hi) = x >= lo && x <= hi;, and it works anywhere an expression does: in concurrent assertions, in immediate assertions and in ordinary procedural code. The example uses one let in two rules.

`define STALLED rvalid && !rready
assert property (!`STALLED |-> ...);
// expands to !rvalid && !rready

let stalled = rvalid && !rready;
assert property (!stalled |-> ...);
// means !(rvalid && !rready)

Use let for conditions, a sequence for anything that spans clock edges, and a property for a complete rule with an implication.

A module of rules

Collect the rules for one interface in a checker module: a module whose ports are inputs only and whose body is assertions, plus any auxiliary code they need. default clocking and default disable iff at the top keep every assertion short.

Parameters adapt the rules to each use, such as the longest legal stall. Because the module only reads its inputs, it never changes the behaviour of the design it watches.

Binding into a DUT you cannot edit

bind rd_port rd_rules #(.MAX_STALL(2)) rules (.*); instantiates rd_rules inside every instance of rd_port, without touching the rd_port source. The .* connects each checker port to the signal of the same name in the target.

The bound instance can see the target's internal signals, not only its ports, so assertions can watch state that never reaches an output. A bind can also name one instance instead of every instance of a module.

// tb_port0.sv
assert property (... hold rule ...);
// tb_port1.sv
assert property (... old hold rule ...);

module rd_rules ...;
  hold: assert property (holds_offer);
endmodule
bind rd_port rd_rules rules (.*);

Use %m in fail messages to print the full path of the failing assertion. With rules bound into many ports, tb.port1.rules.stall says at once which port broke which rule.

Binding one instance

Sometimes only one instance needs a rule set, or needs different parameters. The bind statement can name a single instance instead of a module, so one port can have a tighter stall bound than the others.

Binding by module is the safer default. Every new instance of the module then gets the rules automatically, while an instance-specific bind has to be remembered each time the design grows.

Assertions in the interface

Rules can also sit inside the interface that bundles the signals, as Module 6 suggested. Every instance of the interface then checks itself, with no bind statement at all.

The cost is that the rules travel with the interface into every testbench, whether or not they apply there. A separate checker module bound where needed keeps that choice explicit and easy to change.

Organising a rule library

Group the named sequences and properties for one protocol in one place, and give each assertion a label that says its rule, such as hold or last_needs_valid. Labels end up in reports, waivers and coverage databases, so they should not change casually.

Document each rule with the spec sentence it implements, as a comment above it. When a rule fires, that comment is the first thing an engineer needs.

A checker instead of a module

The checker construct is a container made for assertions and the modelling code they need. It is declared with checker ... endchecker, instantiated like a module, and bound like a module. Inside it, %m names the checker instance, such as tb.p1.bound.hold, so reports stay as precise as with a module of rules.

The standard gives checkers more than modules: they can be instantiated inside procedural code, their arguments can be sequences and properties, and synthesis tools normally ignore them. A module is the general container, with no limits on its modelling code.

In this track both work. Use a module when the rules need a real model, such as the queues of lesson A8.1. Use a checker for a self-contained rule set that you want to reuse as a library unit.

Try it

One checker module, bound into both ports, reported three different rules: port 0 changed data while stalled, port 1 stalled longer than its bound, and port 1 raised rlast without rvalid. Each line carries the full path, so the port and the rule are obvious.

Change the bind to #(.MAX_STALL(3)) and predict which line disappears.

Check yourself

module port #(parameter string NAME = "") (input logic clk, v, l);
endmodule

module rules #(parameter string PORT = "?") (input logic clk, v, l);
  last_needs_valid: assert property (@(posedge clk) l |-> v)
    else $display("%s failed at %0t", PORT, $time);
endmodule

module tb;
  logic clk = 0;
  always #5 clk = ~clk;
  logic v0 = 0, l0 = 0, v1 = 0, l1 = 0;
  port #("p0") p0 (.clk, .v(v0), .l(l0));
  port #("p1") p1 (.clk, .v(v1), .l(l1));
  initial begin
    @(negedge clk); v0 = 1; l0 = 1;           // legal on p0 at 15
    @(negedge clk); v0 = 0; l0 = 0; l1 = 1;   // rlast without valid on p1 at 25
    @(negedge clk); l1 = 0;
    #20 $finish;
  end
endmodule

bind port rules #(.PORT(NAME)) chk (.*);

checker hold_chk (logic clk, logic v, logic r, logic [7:0] d);
  let stalled = v && !r;
  hold: assert property (@(posedge clk) stalled |=> $stable(d))
    else $display("t=%0t %m failed", $time);
endchecker

module rd_port (input logic clk, rvalid, rready, input logic [7:0] rdata);
endmodule

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                  // rising edges at 5, 15, 25, ...
  logic       v0 = 0, r0 = 0, v1 = 0, r1 = 0;
  logic [7:0] d0 = 0, d1 = 0;
  hold_chk direct (clk, v0, r0, d0);     // instantiated like a module
  rd_port p1 (.clk, .rvalid(v1), .rready(r1), .rdata(d1));
  initial begin
    @(negedge clk); v0 = 1; d0 = 8'h01;  // direct: stalled at 15, data held
    @(negedge clk); r0 = 1;              // taken at 25
    @(negedge clk); v0 = 0; r0 = 0; v1 = 1; d1 = 8'h05;   // p1: stalled at 35
    @(negedge clk); d1 = 8'h06;          // data changes while still stalled
    @(negedge clk); r1 = 1;
    @(negedge clk); v1 = 0; r1 = 0;
    #20 $finish;
  end
endmodule

bind rd_port hold_chk bound (clk, rvalid, rready, rdata);

`define STALLED rvalid && !rready
module tb;
  logic rvalid = 0, rready = 1;          // no beat is stalled
  let stalled = rvalid && !rready;
  initial #1 $display("macro=%0d let=%0d", !`STALLED, !stalled);
endmodule

bind rd_port rd_rules rules (.clk(clk), .rvalid(rvalid), .rready(rready), .rlast(rlast));

bind rd_port rd_rules rules (clk, rvalid, rready, rlast);

bind rd_port rd_rules rules (.clk(clk), .rvalid(rready), .rready(rvalid), .rlast(rlast));

bind rd_port rd_rules rules (.*);