A Bus Interface: APB and AXI4-Lite

module apb_req_f(input clk, presetn, start, wr, input [3:0] addr, input [31:0] data, input pready,
  output reg psel = 0, output reg penable = 0, output reg pwrite = 0, output reg [3:0] paddr = 0,
  output reg [31:0] pwdata = 0, output [3:0] pstrb);
  assign pstrb = pwrite ? 4'hF : 4'h0;
  always @(posedge clk)
    if (!presetn) begin psel <= 0; penable <= 0; end
    else if (!psel) begin
      if (start) begin psel <= 1; pwrite <= wr; paddr <= addr; pwdata <= data; end   // SETUP
    end else if (!penable) penable <= 1;                                           // ACCESS
    else if (pready) begin                                                         // done
      penable <= 0; psel <= start;                                                 // next SETUP at once, or IDLE
      if (start) begin pwrite <= wr; paddr <= addr; pwdata <= data; end
    end
    else paddr <= addr;   // bug: the address follows the input while the access waits
endmodule
module apb_fv #(parameter CPL = 1, MAXW = 0)(input clk, presetn, psel, penable, pwrite,
  input [3:0] paddr, input [31:0] pwdata, input [3:0] pstrb, input pready);
  reg setup_q = 0, wait_q = 0, done_q = 0;          // last cycle: SETUP, a waited ACCESS, a completion
  reg [3:0] paddr_q = 0, pstrb_q = 0;
  reg [31:0] pwdata_q = 0;
  reg pwrite_q = 0;
  reg [2:0] waits = 0;                               // wait states so far in this access
  always @(posedge clk) begin
    setup_q <= presetn && psel && !penable;
    wait_q  <= presetn && psel && penable && !pready;
    done_q  <= presetn && psel && penable && pready;
    paddr_q <= paddr; pwdata_q <= pwdata; pstrb_q <= pstrb; pwrite_q <= pwrite;
    waits <= presetn && psel && penable && !pready ? waits + 3'd1 : 3'd0;
  end
  // Requester rules (IHI 0024E 3.1, 3.2, 4.1)
  wire r_access = !(setup_q || wait_q) || psel && penable;                // SETUP and a waited ACCESS go on to ACCESS
  wire r_enable = !penable || psel && (setup_q || wait_q);                // PENABLE only after SETUP
  wire r_stable = !(setup_q || wait_q) || paddr == paddr_q && pwrite == pwrite_q && pwdata == pwdata_q && pstrb == pstrb_q;
  wire r_strobe = !(psel && !pwrite) || pstrb == 4'd0;                    // no strobes on a read
  // Completer rule: at most MAXW wait states
  wire c_wait = !(psel && penable && !pready) || waits < MAXW;
  always @(posedge clk) if (presetn) begin
    if (CPL) begin
      assume(r_access); assume(r_enable); assume(r_stable); assume(r_strobe);
      assert(c_wait);
    end else begin
      assert(r_access); assert(r_enable); assert(r_stable); assert(r_strobe);
      assume(c_wait);
    end
  end
endmodule

module req_top(input clk, presetn, start, wr, input [3:0] addr, input [31:0] data, input pready);
  wire psel, penable, pwrite;
  wire [3:0] paddr, pstrb;
  wire [31:0] pwdata;
  apb_req_f dut(.clk(clk), .presetn(presetn), .start(start), .wr(wr), .addr(addr), .data(data), .pready(pready),
    .psel(psel), .penable(penable), .pwrite(pwrite), .paddr(paddr), .pwdata(pwdata), .pstrb(pstrb));
  apb_fv #(.CPL(0), .MAXW(0)) fv(.clk(clk), .presetn(presetn), .psel(psel), .penable(penable), .pwrite(pwrite),
    .paddr(paddr), .pwdata(pwdata), .pstrb(pstrb), .pready(pready));
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(!presetn); end else begin assume(!!presetn); end
  end
`endif
endmodule