Registers (CSRs)

Generate a fixed set of checks per access type from a register map, run them on an APB completer with the bus rules as assumptions, and catch a W1C field built as plain read-write.

Lesson: F5.4
Time: 18 min
Runs on: SymbiYosys
Check: 4 questions

An interrupt-status register was specified write-one-to-clear and built as plain read-write. Every test passed for months, because the tests cleared it by writing zero, which works on both. In the field an interrupt that arrived during the handler was written over and lost.

A write of 0 clears a W1C bit

Measured with smtbmc yices at depth 20, the write-0 row only. The write completes at step 2 with the set bit's data bit at 0; at step 3 irq_stat is 0. Reported at 4.

A Row in the Map, a Few Fixed Checks

CSV row	Generated property (SVA)
`0x108 IRQ_STAT W1C`, write 0	`wr(108) \|=> bits written 0 and not set by hardware keep their value`
`0x108 IRQ_STAT W1C`, write 1	`wr(108) \|=> bits written 1 and not set by hardware are 0`
`0x108 IRQ_STAT`, hardware set	`irq_in != 0 \|=> every bit set last cycle is 1`
`0x10C IRQ_EN RW1S`	`wr(10C) \|=> irq_en == $past(irq_en) \| data`
`0x100 CTRL RW`, byte strobes	`wr(100) \|=> each strobed byte is the data, the others unchanged`
every field: reset value	`!presetn \|=> ctrl == 0 && irq_en == 0`

wr(R) is psel && penable && pwrite && paddr == R: the completion cycle (pready is tied high here). Each check reads the register one cycle later, so every property stays one row long.

A register map is a table: offset, field, bits, access type, reset value. Each access type implies the same small set of checks wherever it appears. RW: a write lands. RO: a write changes nothing and a read returns the source. W1C: a 1 clears, a 0 leaves, hardware wins. RW1S: a 1 sets.

The generator reads the map, not the RTL. A property derived from the RTL would check the RTL against itself; the map is the spec.

Why W1C Needs Three Rows

One W1C Bit Is a Two-State MachineEach bit of IRQ_STAT moves only on these arcs. A plain read-write register adds the forbidden arc: a write of 0 clears. Arrows mean "next cycle".

call: who calls whom

Read the diagram as text

bit = 0: nothing pending
bit = 1: an interrupt pending
irq_in[i] = 1: hardware sets, and wins over a clearing write
write with data[i] = 1: firmware clears what it handled
write with data[i] = 0: must leave the bit alone
plain RW: data[i] = 0 clears: the forbidden arc the story hit

bit = 0 → irq_in[i] = 1
irq_in[i] = 1 → bit = 1
bit = 1 → write with data[i] = 1
write with data[i] = 1 → bit = 0
bit = 1 → write with data[i] = 0
write with data[i] = 0 → plain RW: data[i] = 0 clears: RW only

Two arcs leave "bit = 1": a clearing write of 1, or nothing. The write-0 property catches the third arc that a plain register adds.

The plain read-write block breaks two of the three W1C rows: a 0 clears and a 1 sets. With every row present the solver reported the first it met, the write of 1. Run the write-0 row alone and it reports the story's bug: FAIL at reported step 4.

Tests that write only zeros cannot tell the two blocks apart, and the property that catches the field bug never mentions the test's data at all.

The Bus Rules Are Assumptions

Requester rules, assumed (IHI 0024E)

if (penable) assume(psel && setup_q);
if (setup_q) assume(psel && penable &&
  paddr == paddr_q && pwrite == pwrite_q &&
  pwdata == pwdata_q);

ACCESS follows SETUP with the same address, direction and data.

What the completer claims

wr && paddr == 12'h108 |=> ((irq_stat ^ $past(irq_stat)) & ~wdata4_q & ~irq_in_q) == 0

One W1C row, checked on every completed write.

The bus side is the neighbour's promise, so it is assumed (F3.1); the register behaviour is the block's claim, so it is asserted. The covers show the assumptions left every write kind possible: a write to IRQ_STAT, one racing a hardware set, a single-lane CTRL write, all reached by step 3.

Run	Measured result	Time
Correct block, clocked immediate	BMC PASS to depth 20	686 ms
Correct block, concurrent props.sv	BMC PASS to depth 20	1009 ms
W1C as RW, write-0 row only	FAIL at reported step 4	1163 ms
W1C as RW, every row	FAIL at reported step 4	995 ms
CTRL resets to 1	FAIL at reported step 2	748 ms
CTRL ignores pstrb (immediate)	FAIL at reported step 4	536 ms
Correct block, prove k = 4 (immediate)	Prove PASS (k = 4)	533 ms
Correct block, abc pdr (concurrent)	Prove PASS (abc pdr)	791 ms

Mode bmc, depth 20, smtbmc yices unless named; presetn assumed low in step 0. The engine refuses $past(pwdata) on an input, so props.sv reads registered copies.

The checks are the easy part; the exceptions column is the work. A read that clears, a write that starts a transfer, two offsets for one register, privilege from pprot, a status field the hardware writes on its own path. Each needs a row of its own or an assumption that switches the path off, and a review of that assumption.

Asked in Interviews

Question	Answer
How are registers verified formally?	From the register map: a fixed check set per access type, generated per field, with the bus protocol as assumptions and covers on each write kind.
What is hard about it?	Side effects, aliasing, privilege, byte strobes and hardware write paths: the exceptions column of the map.
Why not simulation?	Simulation checks the writes the tests make. The W1C bug passed every test that wrote zero.

Try It

The register map. The notes column holds what no fixed check covers.

offset,field,bits,access,reset,notes
0x100,CTRL,31:0,RW,0x00000000,byte strobes
0x104,STATUS,3:0,RO,-,reads fcount
0x108,IRQ_STAT,3:0,W1C,0x0,set by irq_in; a hardware set wins
0x10C,IRQ_EN,3:0,RW1S,0x0,
0x110,ID,31:0,RO,0x43505231,constant

props.sv: the concurrent rows

assert property (@(posedge clk) disable iff (!presetn) wr && paddr == 12'h108 |=> ((irq_stat ^ $past(irq_stat)) & ~wdata4_q & ~irq_in_q) == 0);
assert property (@(posedge clk) disable iff (!presetn) wr && paddr == 12'h108 |=> (irq_stat & wdata4_q & ~irq_in_q) == 0);
assert property (@(posedge clk) disable iff (!presetn) irq_in != 0 |=> (irq_stat & irq_in_q) == irq_in_q);
assert property (@(posedge clk) disable iff (!presetn) wr && paddr == 12'h10C |=> irq_en == ($past(irq_en) | wdata4_q));
assert property (@(posedge clk) disable iff (!presetn) wr && paddr == 12'h100 |=> ctrl == (($past(ctrl) & ~lanes_q) | (pwdata_q & lanes_q)));
assert property (@(posedge clk) !presetn |=> ctrl == 0 && irq_en == 0);

History on registers uses $past; history on inputs reads the copies in the bench.

The clocked immediate fallback

    wr_en_q   <= presetn && wr && paddr == 12'h10C;
    live_q    <= presetn;
  end
  always @(posedge clk) if (presetn) begin
    if (wr_irq_q) assert(((irq_stat ^ irq_stat_q) & ~pwdata_q[3:0] & ~irq_in_q) == 0);   // W1C: a 0 leaves the bit
    if (wr_irq_q) assert((irq_stat & pwdata_q[3:0] & ~irq_in_q) == 0);                  // W1C: a 1 clears it
    if (live_q)   assert((irq_stat & irq_in_q) == irq_in_q);                            // a hardware set wins
    if (wr_en_q)  assert(irq_en == (irq_en_q | pwdata_q[3:0]));                         // RW1S
    if (wr_ctrl_q) assert(ctrl == ((ctrl_q & ~lanes_q) | (pwdata_q & lanes_q)));        // RW, byte strobes
    if (psel && penable && !pwrite && paddr == 12'h104) assert(prdata == {28'd0, fcount});   // RO
  end
  always @(posedge clk) if (!live_q && presetn) assert(ctrl == 0 && irq_en == 0);       // reset values

Each |=> becomes a flop that remembers the write.

The whole task. The prove runs change the mode and the engine.

[options]
mode bmc
depth 20
[engines]
smtbmc yices
[script]
read_verilog -formal -sv design.sv props.sv
prep -top csr_apb
[files]
design.sv
props.sv

Run the write-0 row
Run as it is: FAIL at reported step 4. In the trace find the hardware set, the write and the lost bit.
Run every row
Paste the full props.sv: FAIL at reported step 4. Which W1C row failed this time?
Fix the field
Make the IRQ_STAT write clear the bits written 1: BMC PASS to depth 20.
Add the missing row
The ID register is RO with the constant 32'h4350_5231. Write its check and run the immediate form: BMC PASS to depth 20.
Prove it
Switch to mode prove with abc pdr: Prove PASS (abc pdr).

Top moduleModeDepthEngine

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

Enable JavaScript to edit and run. The original design and properties follow.

module csr_apb(input clk, presetn, psel, penable, pwrite, input [11:0] paddr,
  input [31:0] pwdata, input [3:0] pstrb, input [2:0] pprot, input [3:0] fcount, input [3:0] irq_in,
  output reg [31:0] prdata, output pready, output pslverr);
  reg [31:0] ctrl=0;
  reg [3:0] irq_stat=0, irq_en=0;
  assign pready = 1'b1;
  assign pslverr = 1'b0;
  wire wr = psel && penable && pwrite;   // the completion cycle of a write
  wire [31:0] lanes = {{8{pstrb[3]}}, {8{pstrb[2]}}, {8{pstrb[1]}}, {8{pstrb[0]}}};
  always @(posedge clk)
    if (!presetn) begin ctrl <= 32'h0; irq_stat <= 0; irq_en <= 0; end
    else begin
      if (wr && paddr == 12'h100) ctrl <= (ctrl & ~lanes) | (pwdata & lanes);
      if (wr && paddr == 12'h108) irq_stat <= pwdata[3:0] | irq_in;   // bug: plain read-write
      else irq_stat <= irq_stat | irq_in;
      if (wr && paddr == 12'h10C) irq_en <= irq_en | pwdata[3:0];   // RW1S
    end
  always @(*)
    case (paddr)
      12'h100: prdata = ctrl;
      12'h104: prdata = {28'd0, fcount};
      12'h108: prdata = {28'd0, irq_stat};
      12'h10C: prdata = {28'd0, irq_en};
      12'h110: prdata = 32'h4350_5231;
      default: prdata = 32'd0;
    endcase
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(!presetn); end else begin assume(presetn); end
  end
  // last cycle's inputs and state: the registered form of $past
  reg [31:0] pwdata_q=0, lanes_q=0, ctrl_q=0;
  reg [3:0] irq_in_q=0, irq_stat_q=0, irq_en_q=0;
  reg [11:0] paddr_q=0;
  reg pwrite_q=0, setup_q=0;
  wire [3:0] wdata4_q = pwdata_q[3:0];   // the low nibble written last cycle
  always @(posedge clk) begin
    pwdata_q <= pwdata; lanes_q <= lanes; irq_in_q <= irq_in; paddr_q <= paddr; pwrite_q <= pwrite;
    ctrl_q <= ctrl; irq_stat_q <= irq_stat; irq_en_q <= irq_en;
    setup_q <= presetn && psel && !penable;
  end
  // the APB requester's rules (IHI 0024E): SETUP is followed by ACCESS with the same address, direction, data
  always @(posedge clk) if (presetn) begin
    if (penable) assume(psel && setup_q);
    if (setup_q) assume(psel && penable && paddr == paddr_q && pwrite == pwrite_q && pwdata == pwdata_q);
  end
`endif
endmodule

assert property (@(posedge clk) disable iff (!presetn) wr && paddr == 12'h108 |=> ((irq_stat ^ $past(irq_stat)) & ~wdata4_q & ~irq_in_q) == 0);

Check Yourself

Predict the outputcsr_apb with CTRL resetting to 1, mode bmc, default depth 20, smtbmc yices, presetn assumed low in step 0 and high after, the six rows of props.sv including !presetn |=> ctrl == 0 && irq_en == 0. At which reported step does it fail?

module csr_apb(input clk, presetn, psel, penable, pwrite, input [11:0] paddr,
  input [31:0] pwdata, input [3:0] pstrb, input [2:0] pprot, input [3:0] fcount, input [3:0] irq_in,
  output reg [31:0] prdata, output pready, output pslverr);
  reg [31:0] ctrl=0;
  reg [3:0] irq_stat=0, irq_en=0;
  assign pready = 1'b1;
  assign pslverr = 1'b0;
  wire wr = psel && penable && pwrite;   // the completion cycle of a write
  wire [31:0] lanes = {{8{pstrb[3]}}, {8{pstrb[2]}}, {8{pstrb[1]}}, {8{pstrb[0]}}};
  always @(posedge clk)
    if (!presetn) begin ctrl <= 32'h1; irq_stat <= 0; irq_en <= 0; end   // bug: CTRL resets to 1
    else begin
      if (wr && paddr == 12'h100) ctrl <= (ctrl & ~lanes) | (pwdata & lanes);
      if (wr && paddr == 12'h108) irq_stat <= (irq_stat & ~pwdata[3:0]) | irq_in;   // W1C, a hardware set wins
      else irq_stat <= irq_stat | irq_in;
      if (wr && paddr == 12'h10C) irq_en <= irq_en | pwdata[3:0];   // RW1S
    end
  always @(*)
    case (paddr)
      12'h100: prdata = ctrl;
      12'h104: prdata = {28'd0, fcount};
      12'h108: prdata = {28'd0, irq_stat};
      12'h10C: prdata = {28'd0, irq_en};
      12'h110: prdata = 32'h4350_5231;
      default: prdata = 32'd0;
    endcase
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(!presetn); end else begin assume(presetn); end
  end
  // last cycle's inputs and state: the registered form of $past
  reg [31:0] pwdata_q=0, lanes_q=0, ctrl_q=0;
  reg [3:0] irq_in_q=0, irq_stat_q=0, irq_en_q=0;
  reg [11:0] paddr_q=0;
  reg pwrite_q=0, setup_q=0;
  wire [3:0] wdata4_q = pwdata_q[3:0];   // the low nibble written last cycle
  always @(posedge clk) begin
    pwdata_q <= pwdata; lanes_q <= lanes; irq_in_q <= irq_in; paddr_q <= paddr; pwrite_q <= pwrite;
    ctrl_q <= ctrl; irq_stat_q <= irq_stat; irq_en_q <= irq_en;
    setup_q <= presetn && psel && !penable;
  end
  // the APB requester's rules (IHI 0024E): SETUP is followed by ACCESS with the same address, direction, data
  always @(posedge clk) if (presetn) begin
    if (penable) assume(psel && setup_q);
    if (setup_q) assume(psel && penable && paddr == paddr_q && pwrite == pwrite_q && pwdata == pwdata_q);
  end
`endif
endmodule

Read included file: props.sv

assert property (@(posedge clk) disable iff (!presetn) wr && paddr == 12'h108 |=> ((irq_stat ^ $past(irq_stat)) & ~wdata4_q & ~irq_in_q) == 0);
assert property (@(posedge clk) disable iff (!presetn) wr && paddr == 12'h108 |=> (irq_stat & wdata4_q & ~irq_in_q) == 0);
assert property (@(posedge clk) disable iff (!presetn) irq_in != 0 |=> (irq_stat & irq_in_q) == irq_in_q);
assert property (@(posedge clk) disable iff (!presetn) wr && paddr == 12'h10C |=> irq_en == ($past(irq_en) | wdata4_q));
assert property (@(posedge clk) disable iff (!presetn) wr && paddr == 12'h100 |=> ctrl == (($past(ctrl) & ~lanes_q) | (pwdata_q & lanes_q)));
assert property (@(posedge clk) !presetn |=> ctrl == 0 && irq_en == 0);

ConceptWhich line is the RW check, wrongly offered as a W1C check for IRQ_STAT?

wr(108) |=> irq_stat == $past(pwdata)wr(108) |=> bits written 1 and not set by hardware are 0wr(108) |=> bits written 0 keep their valueirq_in != 0 |=> every bit set last cycle is 1

ConceptWhy does the register checker generate its properties from the map and not from the RTL?

Parsing a CSV is faster than elaborating RTL.The map is the spec; checks from the RTL check it against itself.The RTL is too large for the solver to read directly.The RTL has no reset values for the solver to read.

Read the waveformIn the W1C trace, at which step does the write complete, and what does irq_stat hold one step later?

A write of 0 clears a W1C bit

Measured with smtbmc yices at depth 20, the write-0 row only. The write completes at step 2 with the set bit's data bit at 0; at step 3 irq_stat is 0. Reported at 4.

Step 3; the value before the writeStep 1, the SETUP step; 0Step 2; 0, the bit was clearedStep 1, when irq_in rises; 1000

Remember

A register map is a table, and each access type implies a fixed check set: RW lands, RO ignores writes, W1C clears on 1 and keeps on 0 with hardware winning, RW1S sets.
Generate the checks from the map, never from the RTL.
The bus protocol is assumed and covered; the register behaviour is asserted one cycle after the completing write.
The hard part is the exceptions: side effects, aliasing, privilege, strobes and hardware write paths.

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.