Assertions inside RTL and the synthesis guards

Write the checks you rely on as assertions inside the design, guard them so the synthesizer never reads them, and decide which checks belong in a bound module instead.

Lesson: R7.2
Time: 25 min
Runs on: Verilator
Check: 5 questions

A FIFO designer wrote a property inside the RTL: a write offered while the FIFO is full is never taken. Synthesize refused the file with encountered unsupported SVA feature. The next designer deleted the property to get a netlist, and a later edit that let writes through when full went unseen.

The property, unguarded

a_no_write_when_full: assert property (
  @(posedge clk) disable iff (!rst_n)
  write_en && full |-> !take_w)
  else $error("write taken while full: used=%0d", used);

Yosys 0.70 stops at the line with the implication: ERROR: encountered unsupported SVA feature. No netlist, no counts.

The same property, guarded

`ifndef SYNTHESIS
a_no_write_when_full: assert property (
  @(posedge clk) disable iff (!rst_n)
  write_en && full |-> !take_w)
  else $error("write taken while full: used=%0d", used);
`endif

The synthesizer skips the lines and builds 116 cells, the count of the FIFO with no checks at all. Verilator still runs the property in every simulation.

Checks the designer knows

You know facts about your design that no bench writer sees. A count never passes DEPTH; a pointer never overtakes another; a write is never taken when full. An assertion states such a fact so the simulator checks it at every step. Two kinds sit well inside RTL.

Kind	Where it goes	When it is checked	In the lab
immediate `assert (expr) else $error(...)`	a statement inside procedural code	each time the code reaches it, with the values of that moment	the count bound, in the `else` branch of the register block
concurrent `assert property (@(posedge clk) ...)`	module level, beside the logic	at each clock edge, on values sampled just before it; it can span edges	`a_no_write_when_full`
deferred `assert final (expr)`	procedural code or module level	on the final values of the time step, so a passing glitch is not reported	not used

An immediate assertion inside the reset branch's else runs only out of reset. A concurrent one needs disable iff (!rst_n) for the same effect.

Give every check a message with the values that failed. A message that says used=5 points at the bug; a bare assertion failed sends you to the waveform.

What each tool does with an assertion

Assertion	Icarus 12	Verilator 5.052	Yosys 0.70 on this flow
immediate `assert (used <= 4)`	runs it; a label before it is a `syntax error`	runs it	one `$check` cell, plus gates for the condition
deferred `assert final (...)`	`sorry: Deferred assertions are not supported.`	runs it	one `$check` cell
concurrent, one edge: `$onehot0(d)`	`sorry: concurrent_assertion_item not supported.`	runs it	one `$check` cell
concurrent with `\|->`, `\|=>`, `##2` or `##[1:3]`	rejected at compile	runs it	refuses: `encountered unsupported SVA feature`

One small design per row. A $check cell has four inputs and no output, like the $print cell of R1.1, so nothing on the chip reads it.

So "the synthesizer rejects assertions" is only half true on this flow. Properties with an implication or a delay are refused. Single-edge checks are kept as cells that do nothing, and they still change the netlist around them. Unguarded, the lab's immediate assertion alone gives 113 cells and 11 levels of logic. With the guard it is 116 cells and 10 levels, the same as no assertion.

The guard, and who defines SYNTHESIS

The guard is conditional compilation. Code between ` ifndef SYNTHESIS ` and endif ` is compiled only when no macro named SYNTHESIS exists. The slang front end of Yosys 0.70 defines it by itself; its help lists --no-synthesis-define` to turn that off. Icarus 12 and Verilator 5.052 define nothing, so both compile the checks.

Older flows use comments instead: // synthesis translate_off before the checks and // synthesis translate_on after. The slang front end honours them by default, and the lab still builds 116 cells. Simulators read them as comments. This track uses the macro: it is part of the language, while each tool lists its own comment forms.

Three pieces, two readersArrows show which tool reads which code. The checks inside the design travel with it; the bound rules live in a bench file.

Synthesize
SYNTHESIS is defined, so the synthesizer reads the logic and skips the guarded checks. The bound rules are in another file and never reach it.
Run
The simulator defines nothing. It compiles the logic, the checks inside it and any bound rules, and runs them all.

Read the diagram as text

Synthesizer: defines SYNTHESIS
FIFO logic: main.sv
Checks inside: `ifndef SYNTHESIS
Simulator: Verilator, --assert
Bound rules: bind sync_fifo ...

FIFO logic → Synthesizer: reads
FIFO logic → Simulator: reads
Checks inside → Simulator: reads
Bound rules → Simulator: reads

A check inside the design goes wherever the design goes. A bound rule goes only where a bench attaches it.

Inside the design or bound to it

Put a fact your design relies on inside it, guarded: the count bound, a one-hot state, a pointer order. It documents the design and fires in every bench that uses it, even one written years later. Put a protocol rule that a bench may want to switch off in its own module. Attach it with bind, as R6.6 did: bind sync_fifo fifo_rules rules (.*); needs no edit and no guard.

Lint reads the guarded checks too, since it does not define SYNTHESIS. On the lab it gives one warning: SYNCASYNCNET on rst_n, because disable iff reads it while the flops use it as an asynchronous reset. The warning is about the check, not the gates.

The lab: the FIFO with its own checks

Design brief

Port	Direction	Width	Meaning
clk	input	1	clock
rst_n	input	1	reset, asynchronous, active-low
write_en	input	1	a write when `write_en` and not `full`
write_data	input	[WIDTH-1:0]	the word to write
read_en	input	1	a read when `read_en` and not `empty`
read_data	output	[WIDTH-1:0]	the word read
read_valid	output	1	read_data holds a word
full	output	1	4 words held
empty	output	1	no word held

Clock: rising edge
Reset: rst_n asynchronous, active-low
Parameters: Depth: 4 words; pointers 3 bits, with the wrap bit of R5.2
Corner cases: writes offered while full; reads offered while empty. Checks: the count never above 4 (immediate); no write taken while full (concurrent); both guarded

Run and Synthesize as shipped
Edges 6 and 7 offer writes to a full FIFO; both are refused and the checks stay quiet. Synthesize reports 116 cells, 47 flops, 10 levels.
Break the design
Change the write accept to assign take_w = write_en; and Run. The run stops at edge 6 with %Error: main.sv:51: Assertion failed in tb.dut.a_no_write_when_full: write taken while full: used=4.
Remove the guards
Put the accept back, delete the four guard lines and Synthesize. Yosys 0.70 reports main.sv:47: ERROR: encountered unsupported SVA feature.

Asked in interviews

Where do you put assertions, design or testbench?
Both. The designer asserts the micro-architecture facts the logic relies on, inside the RTL. The verifier writes interface and end-to-end rules, usually in a separate module attached with bind.
How do you keep assertions out of synthesis?
Wrap them in ` ifndef SYNTHESIS ``, a macro most synthesizers define, or in translate_off and translate_on comments. Check what your flow defines: here the slang front end defines SYNTHESIS itself.
What is bind?
A statement that instantiates a module inside every instance of a target module, or one instance, without editing its source. Rules attached that way need no guard, because the synthesizer never reads the bench file.

Try it

Four writes fill the FIFO by edge 5. The writes offered at edges 6 and 7 meet full and are refused, so both checks stay quiet. The reads return 10, 20, 30, 40 and then find the FIFO empty.

Synthesize sees the design with SYNTHESIS defined: 116 cells, 47 flops (32 of them the memory), 0 latches, 10 levels of logic. Delete both checks and the guards, and the counts do not move.

RTLVerilator · simulator service · Lint: Verilator service · Synthesize: Yosys service

Edit the design, then Run, Lint or Synthesize

Expected: e0 we=0 re=0 full=0 empty=1 valid=0 data=00 e1 we=0 re=0 full=0 empty=1 valid=0 data=00 e2 we=1 re=0 full=0 empty=0 valid=0 data=00 e3 we=1 re=0 full=0 empty=0 valid=0 data=00 e4 we=1 re=0 full=0 empty=0 valid=0 data=00 e5 we=1 re=0 full=1 empty=0 valid=0 data=00 e6 we=1 re=0 full=1 empty=0 valid=0 data=00 e7 we=1 re=0 full=1 empty=0 valid=0 data=00 e8 we=0 re=1 full=0 empty=0 valid=1 data=10 e9 we=0 re=1 full=0 empty=0 valid=1 data=20 e10 we=0 re=1 full=0 empty=0 valid=1 data=30 e11 we=0 re=1 full=0 empty=1 valid=1 data=40 e12 we=0 re=1 full=0 empty=1 valid=0 data=40 e13 we=0 re=0 full=0 empty=1 valid=0 data=40

Original design · 116 cells · 47 flip-flops · 0 latches · 10 logic levels. Synthesis uses Yosys; counts depend on the toolchain.

Original example source

// sync_fifo: the FIFO of R5.2 (pointers with the extra wrap bit), four words deep, with the
// designer's own checks inside. The guard keeps the checks away from the synthesizer.
module sync_fifo #(parameter int DEPTH = 4, parameter int WIDTH = 8) (
  input  logic             clk,
  input  logic             rst_n,         // asynchronous, active-low
  input  logic             write_en,
  input  logic [WIDTH-1:0] write_data,
  input  logic             read_en,
  output logic [WIDTH-1:0] read_data,
  output logic             read_valid,
  output logic             full,
  output logic             empty
);
  localparam int AW = $clog2(DEPTH);      // address bits: 2 for 4 words

  logic [WIDTH-1:0] mem [DEPTH];
  logic [AW:0]      wptr_q, rptr_q;       // the extra bit counts the wraps
  logic [AW:0]      used;                 // words held
  logic             take_w, take_r;       // a write, a read accepted at this edge

  assign used   = wptr_q - rptr_q;
  assign empty  = (used == 0);
  assign full   = (used == (AW+1)'(DEPTH));
  assign take_w = write_en && !full;
  assign take_r = read_en && !empty;

  always_ff @(posedge clk)
    if (take_w) mem[wptr_q[AW-1:0]] <= write_data;

  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) begin
      wptr_q <= '0; rptr_q <= '0; read_valid <= 1'b0; read_data <= '0;
    end else begin
      if (take_w) wptr_q <= wptr_q + 1'b1;
      if (take_r) begin
        rptr_q    <= rptr_q + 1'b1;
        read_data <= mem[rptr_q[AW-1:0]];
      end
      read_valid <= take_r;
`ifndef SYNTHESIS
      // Immediate assertion: at every rising edge out of reset, the count is in range.
      assert (used <= (AW+1)'(DEPTH))
        else $error("used=%0d is above DEPTH=%0d", used, DEPTH);
`endif
    end

`ifndef SYNTHESIS
  // Concurrent assertion: a write offered while full is never taken.
  a_no_write_when_full: assert property (@(posedge clk) disable iff (!rst_n)
    write_en && full |-> !take_w)
    else $error("write taken while full: used=%0d", used);
`endif
endmodule

Read included file: tb.sv

`timescale 1ns/1ps
module tb;
  logic clk = 0;
  always #5 clk = ~clk;                   // rising edges at 5, 15, 25, ...
  logic rst_n = 1;                        // falls at 1 ns: a real edge, so an asynchronous reset acts before any clock
  int edge_n = -1;
  always @(posedge clk) edge_n = edge_n + 1;
  logic       write_en = 0, read_en = 0;
  logic [7:0] write_data = 0;
  logic [7:0] read_data;
  logic       read_valid, full, empty;
  sync_fifo dut (.*);
  // Advance to the next rising edge, wait for the design to settle, then print one line.
  task automatic tick();
    @(posedge clk); #1;
    $display("e%0d we=%b re=%b full=%b empty=%b valid=%b data=%h", edge_n, write_en, read_en, full, empty, read_valid, read_data);
  endtask
  initial begin
    #1 rst_n = 0; tick(); tick(); rst_n = 1;   // asserted at 1 ns, edges 0 and 1 in reset, released 1 ns after edge 1
    // Six writes in a row into a FIFO of four: the last two meet a full FIFO.
    for (int i = 1; i <= 6; i++) begin write_en = 1; write_data = 8'(16 * i); tick(); end
    write_en = 0;
    // Five reads in a row: four words come back, then the FIFO is empty.
    repeat (5) begin read_en = 1; tick(); end
    read_en = 0; tick();
    $finish(0);                             // quiet: no "$finish called" line
  end
endmodule

Check yourself

Predict the outputA FIFO count ignores full. The concurrent check counts its failures in fails, the immediate count bound in over. Six writes arrive at six edges in a row, then two idle edges pass. What does the program print?

module tb;
  logic clk = 0, rst_n = 0, write_en = 0;
  always #5 clk = ~clk;
  logic [2:0] used = 0;                       // words held, in a FIFO of four
  logic full;
  assign full = (used == 3'd4);
  logic take_w;
  assign take_w = write_en;                   // the bug: full is ignored
  always_ff @(posedge clk) if (take_w) used <= used + 1'b1;

  int fails = 0, over = 0;
  a_full: assert property (@(posedge clk) disable iff (!rst_n) write_en && full |-> !take_w)
    else fails++;
  always_ff @(posedge clk) if (rst_n) assert (used <= 3'd4) else over++;

  initial begin
    #2 rst_n = 1; write_en = 1;               // a write at each of the next six edges
    repeat (6) @(posedge clk);
    #1 write_en = 0;
    repeat (2) @(posedge clk);
    #1 $display("fails=%0d over=%0d", fails, over);
    $finish(0);
  end
endmodule

Spot the bugEach option is the end of a FIFO: its accept logic and one check. The bench defines SYNTHESIS, as the synthesizer's front end does, then writes six words and reads four back. Which option fails?

assign take_w = write_en && !full;
  assign take_r = read_en && !empty;
`ifndef SYNTHESIS
  a_full: assert property (@(posedge clk) disable iff (!rst_n)
    write_en && full |-> !take_w);
`endif

assign take_r = read_en && !empty;
`ifndef SYNTHESIS
  assign take_w = write_en && !full;
  a_full: assert property (@(posedge clk) disable iff (!rst_n)
    write_en && full |-> !take_w);
`endif

`ifndef SYNTHESIS
  a_full: assert property (@(posedge clk) disable iff (!rst_n)
    write_en && full |-> !take_w);
`endif
  assign take_w = write_en && !full;
  assign take_r = read_en && !empty;

assign take_w = write_en && !full;
  assign take_r = read_en && !empty;
  // synthesis translate_off
  a_full: assert property (@(posedge clk) disable iff (!rst_n)
    write_en && full |-> !take_w);
  // synthesis translate_on

ConceptOn this flow, why does the lab's concurrent assertion need a guard?

Verilator compiles the design twice and reports the property twiceWithout the guard the property would also check the synthesized netlistThe slang front end refuses any property with an implication or a delayYosys 0.70 keeps it as extra gates that would make the FIFO slower

ConceptA verification engineer has a set of APB protocol rules and wants to switch them on for some benches and off for others. Where should they live?

In the bench's stimulus, as if statements that print errorsInside each completer, guarded with translate_off commentsInside each completer, inside an ifndef SYNTHESIS guardIn their own module, attached with bind where a bench wants them

ConceptYou leave the lab's immediate assertion unguarded and delete the concurrent one. What does Synthesize report?

A netlist with one $check cell, and a cell count that moved from 116 to 113An error at the assertion, the same as for the concurrent propertyA netlist with a new output port that goes high when the count passes 4The same 116 cells, because an immediate assertion is ignored by every synthesizer

Remember

Write the facts your design relies on as assertions inside it, each with a message that prints the values.
On this flow a property with an implication or a delay stops synthesis; a single-edge check becomes a $check cell that moves the counts. Guard them all.
` ifndef SYNTHESIS ` works because the slang front end defines SYNTHESIS` and the simulators do not; check what your own flow defines.
Rules a bench may switch off belong in their own module, attached with bind.