Capstone: Formal Sign-Off of the AXI4-Lite Register Block

module axil_regs(input clk, aresetn,
  input awvalid, input [4:0] awaddr, input [1:0] awid, output awready,
  input wvalid, input [31:0] wdata, input [3:0] wstrb, output wready,
  output reg bvalid = 0, output reg [1:0] bresp = 0, output reg [1:0] bid = 0, input bready,
  input arvalid, input [4:0] araddr, input [1:0] arid, output arready,
  output reg rvalid = 0, output reg [1:0] rresp = 0, output reg [1:0] rid = 0, output reg [31:0] rdata = 0, input rready);
  reg [31:0] ctrl = 0, data = 0, status = 32'h1, id = 32'h4c495445;
  reg aw_v = 0, w_v = 0;                 // an address or a data beat held, waiting for its partner
  reg [4:0] aw_a = 0, rd_a = 0;
  reg [1:0] aw_i = 0;
  reg [31:0] w_d = 0;
  reg [3:0] w_s = 0;
  assign awready = !aw_v;
  assign wready = !w_v;
  assign arready = !rvalid || rready;
  wire commit = aw_v && w_v && (!bvalid || bready);   // both halves held, B channel free
  wire [3:0] ln = 4'hF;   // fault F_STRB_ALL
  wire [31:0] m = {{8{ln[3]}}, {8{ln[2]}}, {8{ln[1]}}, {8{ln[0]}}};   // lanes the write may change
  function [31:0] word(input [1:0] a);
    word = a == 2'd0 ? ctrl : a == 2'd1 ? data : a == 2'd2 ? status : id;
  endfunction
  always @(posedge clk)
    if (!aresetn) begin
      aw_v <= 0; w_v <= 0; bvalid <= 0; rvalid <= 0;
      ctrl <= 0; data <= 0; status <= 32'h1; id <= 32'h4c495445;
    end else begin
      if (awvalid && awready) begin aw_v <= 1; aw_a <= awaddr; aw_i <= awid; end
      if (wvalid && wready) begin w_v <= 1; w_d <= wdata; w_s <= wstrb; end
      if (bvalid && bready) bvalid <= 0;
      if (commit) begin
        aw_v <= 0; w_v <= 0; bvalid <= 1;
        bid <= aw_i;
        bresp <= aw_a[4] ? 2'd3 : aw_a[3] ? 2'd2 : 2'd0;   // DECERR, SLVERR, OKAY
        if (!aw_a[4]) case (aw_a[3:2])
          2'd0: ctrl <= (ctrl & ~m) | (w_d & m);
          2'd1: data <= (data & ~m) | (w_d & m);
          default: ;
        endcase
      end
      if (rvalid && rready) rvalid <= 0;
      if (arvalid && arready) begin
        rvalid <= 1; rid <= arid; rd_a <= araddr;
        rresp <= araddr[4] ? 2'd3 : 2'd0;
        rdata <= araddr[4] ? 32'd0 : word(araddr[3:2]);
      end
    end
endmodule
module axil_bench(input clk, aresetn,
  input awvalid, input [4:0] awaddr, input [1:0] awid,
  input wvalid, input [31:0] wdata, input [3:0] wstrb, input bready,
  input arvalid, input [4:0] araddr, input [1:0] arid, input rready);
  wire awready, wready, bvalid, arready, rvalid;
  wire [1:0] bresp, bid, rresp, rid;
  wire [31:0] rdata;
  axil_regs dut(.clk(clk), .aresetn(aresetn), .awvalid(awvalid), .awaddr(awaddr), .awid(awid), .awready(awready),
    .wvalid(wvalid), .wdata(wdata), .wstrb(wstrb), .wready(wready), .bvalid(bvalid), .bresp(bresp), .bid(bid), .bready(bready),
    .arvalid(arvalid), .araddr(araddr), .arid(arid), .arready(arready), .rvalid(rvalid), .rresp(rresp), .rid(rid), .rdata(rdata), .rready(rready));
  always @(posedge clk) begin
    if ($initstate) begin assume(!aresetn); end else begin assume(aresetn); end
  end
  wire aw_hs = awvalid && awready, w_hs = wvalid && wready, b_hs = bvalid && bready;
  wire ar_hs = arvalid && arready, r_hs = rvalid && rready;
  // registered copies: last cycle's inputs and outputs (the engine refuses $past on an input)
  reg aw_wait = 0, w_wait = 0, ar_wait = 0, b_wait = 0, r_wait = 0, live = 0;
  reg [4:0] awaddr_q = 0, araddr_q = 0;
  reg [1:0] awid_q = 0, arid_q = 0, bresp_q = 0, bid_q = 0, rresp_q = 0, rid_q = 0;
  reg [31:0] wdata_q = 0, rdata_q = 0;
  reg [3:0] wstrb_q = 0;
  always @(posedge clk) begin
    aw_wait <= aresetn && awvalid && !awready; w_wait <= aresetn && wvalid && !wready; ar_wait <= aresetn && arvalid && !arready;
    b_wait <= aresetn && bvalid && !bready; r_wait <= aresetn && rvalid && !rready; live <= aresetn;
    awaddr_q <= awaddr; awid_q <= awid; wdata_q <= wdata; wstrb_q <= wstrb; araddr_q <= araddr; arid_q <= arid;
    bresp_q <= bresp; bid_q <= bid; rresp_q <= rresp; rid_q <= rid; rdata_q <= rdata;
  end
  // the manager's promises (IHI 0022L A2.3): VALID holds, and its payload is stable, until the handshake
  always @(posedge clk) if (aresetn) begin
    if (aw_wait) assume(awvalid && awaddr == awaddr_q && awid == awid_q);
    if (w_wait) assume(wvalid && wdata == wdata_q && wstrb == wstrb_q);
    if (ar_wait) assume(arvalid && araddr == araddr_q && arid == arid_q);
  end
  // write scoreboard: accepted AW and W beats, in order, until their B is taken
  reg [1:0] f_awn = 0, f_wn = 0;
  reg [6:0] f_aw0 = 0, f_aw1 = 0;        // {address, id}
  reg [31:0] f_wd0 = 0, f_wd1 = 0;       // data
  reg [3:0] f_ws0 = 0, f_ws1 = 0;         // strobes
  wire [4:0] e_a = f_aw0[6:2];
  wire [1:0] e_id = f_aw0[1:0];
  wire [1:0] e_resp = e_a[4] ? 2'd3 : e_a[3] ? 2'd2 : 2'd0;   // the response the map requires
  always @(posedge clk)
    if (!aresetn) begin f_awn <= 0; f_wn <= 0; end
    else begin
      if (b_hs) begin f_aw0 <= f_aw1; f_wd0 <= f_wd1; f_ws0 <= f_ws1; end
      if (aw_hs) begin if (f_awn - b_hs == 0) f_aw0 <= {awaddr, awid}; else f_aw1 <= {awaddr, awid}; end
      if (w_hs) begin if (f_wn - b_hs == 0) begin f_wd0 <= wdata; f_ws0 <= wstrb; end else begin f_wd1 <= wdata; f_ws1 <= wstrb; end end
      f_awn <= f_awn + aw_hs - b_hs;
      f_wn <= f_wn + w_hs - b_hs;
    end
  // the watched word: any of the four, fixed for the whole trace, and its four byte lanes
  wire [1:0] f_word = $anyconst;
  reg [7:0] f_sh0 = 0, f_sh1 = 0, f_sh2 = 0, f_sh3 = 0;
  wire f_hit = b_hs && !e_a[4] && !e_a[3] && !f_word[1] && e_a[2] == f_word[0];   // a write to it is answered
  always @(posedge clk)
    if (!aresetn) {f_sh3, f_sh2, f_sh1, f_sh0} <= f_word == 2'd2 ? 32'h1 : f_word == 2'd3 ? 32'h4c495445 : 32'h0;
    else if (f_hit) begin
      if (f_ws0[0]) f_sh0 <= f_wd0[7:0];
      if (f_ws0[1]) f_sh1 <= f_wd0[15:8];
      if (f_ws0[2]) f_sh2 <= f_wd0[23:16];
      if (f_ws0[3]) f_sh3 <= f_wd0[31:24];
    end
  // the read in flight: its address, id, and the watched word's value when it was accepted
  reg f_rn = 0, f_quiet = 0;
  reg [4:0] f_ra = 0;
  reg [1:0] f_rid = 0;
  reg [31:0] f_rsh = 0;
  wire f_rout = f_ra[4];                                        // the read was outside the map
  wire [1:0] f_rresp = f_rout ? 2'd3 : 2'd0;
  wire f_check = f_quiet && !f_ra[4] && f_ra[3:2] == f_word;   // a read of the watched word, no write in flight
  always @(posedge clk)
    if (!aresetn) f_rn <= 0;
    else begin
      f_rn <= ar_hs || f_rn && !r_hs;
      if (ar_hs) begin f_ra <= araddr; f_rid <= arid; f_rsh <= {f_sh3, f_sh2, f_sh1, f_sh0}; f_quiet <= f_awn == 0 && f_wn == 0; end
    end
  always @(posedge clk) if (aresetn) begin
    if (!live) a_reset: assert(!bvalid && !rvalid);                                       // reset
    if (b_wait) a_b_hold: assert(bvalid && bresp == bresp_q && bid == bid_q);              // B holds
    if (r_wait) a_r_hold: assert(rvalid && rresp == rresp_q && rid == rid_q && rdata == rdata_q);   // R holds
    if (bvalid) a_b_resp: assert(f_awn != 0 && f_wn != 0 && bid == e_id && bresp == e_resp);
    if (rvalid) a_r_resp: assert(f_rn && rid == f_rid && rresp == f_rresp);
    if (rvalid && f_rout) a_r_zero: assert(rdata == 32'd0);
    if (rvalid && f_check) a_r_data: assert(rdata == f_rsh);                              // the lane shadows
  end
endmodule