Three homes, three tradeoffs

Every assertion lives inline in the RTL next to the logic, in an interface beside the signals, or in a separate checker attached with bind. The choice decides ownership, visibility, reuse, and flow handling.

Placement is an architecture decision wearing a style-question costume. It also routes triage: inline failures page designers, bound-checker failures page verification first.

Each option in code

The interface and bind forms below are fragments, so they are not run in this course's checks; Verilator 5.048 compiles both inside a complete design. The testbench proves the inline form on a small FIFO.

1
2
3
4
5
6
7
8
9

// not-run: fragment: an interface with no module that instantiates it
// INTERFACE: the protocol rule rides with the bus definition;
// every instance of the interface checks itself.
interface axi_lite_if (input logic clk, rst_n);
  logic awvalid, awready; logic [31:0] awaddr;
  ap_aw_stable: assert property (@(posedge clk) disable iff (!rst_n)
    awvalid && !awready |=> awvalid && $stable(awaddr))
    else $error("AW channel unstable while stalled");
endinterface

1
2
3
4
5
6
7

// not-run: fragment: fifo_core and fifo_chk are not defined here
// BIND: zero RTL edits; a verification-owned file attaches a checker
// to every instance of a module type, seeing its internals.
bind fifo_core fifo_chk #(.DEPTH(16)) u_chk (
  .clk(clk), .rst_n(rst_n),
  .push(wr_en && !full), .pop(rd_en && !empty),
  .count(occupancy_q));            // internal signal: bind can see it

Designers own inline assertions: micro-architectural invariants only they know, written while the intent is fresh. Protocol owners own interface assertions. Verification owns bind files and checker libraries.

Bind by module type, not by instance path. Newly added instances of the type are then checked automatically, instead of silently escaping.

Surviving synthesis and tool flows

Concurrent assertions are not synthesizable. Most synthesis tools ignore them, but relying on every tool in the flow to ignore them is how builds break at night.

1
2
3
4
5

// snippet: standard guard pattern for inline assertions
`ifndef SYNTHESIS
  ap_no_ov: assert property (@(posedge clk) disable iff (!rst_n)
    !(push && full));
`endif

Bound checkers are excluded from synthesis file lists structurally. Inline and interface assertions get guarded, since a synthesized interface carries its assertions into synthesis: one macro convention per project, linted for unguarded stragglers.

The same property text serves simulation and formal tools. Bind plus checker is the most formal-friendly home: the formal tool compiles RTL plus bind files with no testbench.

Keep properties pure and side effects in action blocks only. At block boundaries, input-protocol assertions flip from assert to assume, and simulation-tuned bounds relax back to liveness behind a parameter.

Testbench

A four-deep FIFO with designer-owned inline invariants. The stimulus fills it, drops one extra push, drains in order, and pops once while empty.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45

module tiny_fifo #(
  parameter int DEPTH = 4,
  parameter int W = 8
) (
  input logic clk, rst_n,
  input logic push, pop,
  input logic [W-1:0] wdata,
  output logic [W-1:0] rdata,
  output logic full, empty
);
  localparam int AW = $clog2(DEPTH);
  logic [W-1:0] mem [DEPTH];
  logic [AW-1:0] wptr, rptr;
  logic [AW:0] count;

  assign full = (count == DEPTH);
  assign empty = (count == '0);
  assign rdata = mem[rptr];

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      wptr <= '0; rptr <= '0; count <= '0;
    end else begin
      if (push && !full) begin
        mem[wptr] <= wdata;
        wptr <= wptr + 1'b1;
      end
      if (pop && !empty) begin
        rptr <= rptr + 1'b1;
      end
      case ({push && !full, pop && !empty})
        2'b10:   count <= count + 1'b1;
        2'b01:   count <= count - 1'b1;
        default: count <= count;
      endcase
    end
  end

  `ifndef SYNTHESIS
  ap_count_bound: assert property (@(posedge clk) disable iff (!rst_n)
    count <= DEPTH);
  ap_flags_agree: assert property (@(posedge clk) disable iff (!rst_n)
    !(full && empty));
  `endif
endmodule

PASS: fifo held four words, dropped the extra push, and drained in order

Related topics

• The Assertion Review Checklist