Lesson 7.3 · Formal Apps for Everyday Problems

Control and status registers

Register blocks are large, regular and full of subtle access rules — perfect for formal. A register app reads the register description and generates one small property per field behaviour. Here is a hand-written version for a tiny block.

Addr	Register	Access	Behaviour
0	CTRL[7:0]	RW	Software writes; reads back the written value; reset 0
1	STATUS[0]	W1C	Set by hardware event; cleared by writing 1; hardware set wins over a simultaneous clear
2	ID[7:0]	RO	Constant 0xA5; writes ignored
3	—	reserved	Reads 0; writes ignored

csr_block.sv

// csr_block.sv — tiny register block with RW, W1C, RO and reserved addresses
module csr_block (
  input  logic       clk,
  input  logic       rst,
  input  logic       wr_en,
  input  logic [1:0] addr,
  input  logic [7:0] wdata,
  output logic [7:0] rdata,      // combinational read of 'addr'
  input  logic       hw_event,   // sets STATUS[0]
  output logic [7:0] ctrl,
  output logic       irq         // = STATUS[0]
);
  always_ff @(posedge clk) begin
    if (rst) begin
      ctrl <= 8'h00;
      irq  <= 1'b0;
    end else begin
      if (wr_en && addr == 2'd0)                  ctrl <= wdata;
      if (hw_event)                               irq  <= 1'b1;   // hardware set wins
      else if (wr_en && addr == 2'd1 && wdata[0]) irq  <= 1'b0;   // write-1-to-clear
    end
  end

  always_comb begin
    case (addr)
      2'd0:    rdata = ctrl;
      2'd1:    rdata = {7'b0, irq};
      2'd2:    rdata = 8'hA5;
      default: rdata = 8'h00;
    endcase
  end
endmodule

csr_block_fv.sv

// csr_block_fv.sv — register properties (what a CSR app would generate)
module csr_block_fv (
  input logic       clk, rst, wr_en, hw_event,
  input logic [1:0] addr,
  input logic [7:0] wdata
);
  logic [7:0] rdata, ctrl;
  logic       irq;
  csr_block dut (.*);

  initial assume (rst);
  default clocking cb @(posedge clk); endclocking
  default disable iff (rst);

  wire wr_ctrl   = wr_en && addr == 2'd0;
  wire wr_status = wr_en && addr == 2'd1;

  // CTRL: RW
  a_ctrl_write: assert property (wr_ctrl |=> ctrl == $past(wdata));
  a_ctrl_hold:  assert property (!wr_ctrl |=> $stable(ctrl));
  a_ctrl_read:  assert property (addr == 2'd0 |-> rdata == ctrl);

  // STATUS[0]: W1C with hardware priority
  a_evt_set:    assert property (hw_event |=> irq);
  a_evt_clear:  assert property (wr_status && wdata[0] && !hw_event |=> !irq);
  a_evt_sticky: assert property (!hw_event && !(wr_status && wdata[0]) |=> irq == $past(irq));
  a_evt_read:   assert property (addr == 2'd1 |-> rdata == {7'b0, irq});

  // ID: RO constant;  addr 3: reserved
  a_id_read:    assert property (addr == 2'd2 |-> rdata == 8'hA5);
  a_rsvd_read:  assert property (addr == 2'd3 |-> rdata == 8'h00);

  // reset values (checked in the first cycle after reset)
  a_reset_vals: assert property (@(posedge clk) $fell(rst) |-> ctrl == 8'h00 && !irq);

  // covers
  c_set_and_clear_same_cycle: cover property (hw_event && wr_status && wdata[0]);
  c_ctrl_written:             cover property (wr_ctrl ##1 ctrl == 8'hFF);
endmodule

Where register bugs hide

Address decoding — aliasing, where a write to one address also changes another register (caught by the "hold" properties).
Side effects — clear-on-read, write-1-to-clear, hardware vs software priority.
Reset values that disagree with the documentation.
Byte enables and partial writes in wider registers.