From fa25c6e68241f3557796bebe6f295f167c3e757d Mon Sep 17 00:00:00 2001
From: drewbabel <122849144+drewbabel@users.noreply.github.com>
Date: Thu, 30 Jul 2026 17:25:33 -0700
Subject: [PATCH 1/4] [rtl] Add AXI4-Lite register block

---
 rtl/axil_csr.sv | 95 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 95 insertions(+)
 create mode 100644 rtl/axil_csr.sv

diff --git a/rtl/axil_csr.sv b/rtl/axil_csr.sv
new file mode 100644
index 0000000..8626a32
--- /dev/null
+++ b/rtl/axil_csr.sv
@@ -0,0 +1,95 @@
+`default_nettype none
+
+module axil_csr #(
+    parameter int ADDR_WIDTH = 4,
+    parameter int DATA_WIDTH = 32
+) (
+    input  logic                    clk,
+    input  logic                    rst_n,
+    // Write address
+    input  logic                    s_axi_awvalid,
+    output logic                    s_axi_awready = 1'b0,
+    input  logic [  ADDR_WIDTH-1:0] s_axi_awaddr,
+    input  logic [             2:0] s_axi_awprot,          // Permission bit
+    // Write data
+    input  logic                    s_axi_wvalid,
+    output logic                    s_axi_wready = 1'b0,
+    input  logic [  DATA_WIDTH-1:0] s_axi_wdata,
+    input  logic [DATA_WIDTH/8-1:0] s_axi_wstrb,
+    // Write response
+    output logic                    s_axi_bvalid = 1'b0,
+    input  logic                    s_axi_bready,
+    output logic [             1:0] s_axi_bresp,
+    // Read address
+    input  logic                    s_axi_arvalid,
+    output logic                    s_axi_arready = 1'b0,
+    input  logic [  ADDR_WIDTH-1:0] s_axi_araddr,
+    input  logic [             2:0] s_axi_arprot,          // Permission bit
+    // Read data
+    output logic                    s_axi_rvalid = 1'b0,
+    input  logic                    s_axi_rready,
+    output logic [  DATA_WIDTH-1:0] s_axi_rdata,
+    output logic [             1:0] s_axi_rresp
+);
+
+  localparam int NumRegs = 4;
+  localparam int Lsb = $clog2(DATA_WIDTH / 8);  // Byte lane bits
+  localparam int IdxWidth = ADDR_WIDTH - Lsb;
+
+  logic [DATA_WIDTH-1:0] regs     [NumRegs];
+
+  logic [  IdxWidth-1:0] wr_index;
+  logic [  IdxWidth-1:0] rd_index;
+
+  logic                  wr_xfer;
+  logic                  rd_xfer;
+
+  assign wr_index = s_axi_awaddr[IdxWidth+Lsb-1:Lsb];
+  assign rd_index = s_axi_araddr[IdxWidth+Lsb-1:Lsb];
+
+  assign s_axi_bresp = 2'b00;
+  assign s_axi_rresp = 2'b00;
+
+  assign wr_xfer = s_axi_awready && s_axi_awvalid && s_axi_wready && s_axi_wvalid;
+  assign rd_xfer = s_axi_arready && s_axi_arvalid;
+
+  always_ff @(posedge clk) begin
+    if (!rst_n) begin
+      s_axi_awready <= 1'b0;
+      s_axi_wready  <= 1'b0;
+      s_axi_arready <= 1'b0;
+    end else begin
+      s_axi_awready <= !s_axi_awready && s_axi_awvalid && s_axi_wvalid
+          && (!s_axi_bvalid || s_axi_bready);
+      s_axi_wready <= !s_axi_wready && s_axi_awvalid && s_axi_wvalid
+          && (!s_axi_bvalid || s_axi_bready);
+      s_axi_arready <= !s_axi_arready && s_axi_arvalid && (!s_axi_rvalid || s_axi_rready);
+    end
+  end
+
+  always_ff @(posedge clk) begin
+    if (!rst_n) begin
+      s_axi_bvalid <= 1'b0;
+      s_axi_rvalid <= 1'b0;
+    end else begin
+      if (wr_xfer) s_axi_bvalid <= 1'b1;
+      else if (s_axi_bready) s_axi_bvalid <= 1'b0;
+
+      if (rd_xfer) s_axi_rvalid <= 1'b1;
+      else if (s_axi_rready) s_axi_rvalid <= 1'b0;
+    end
+  end
+
+  always_ff @(posedge clk) begin
+    if (wr_xfer) begin
+      for (int i = 0; i < $bits(s_axi_wstrb); i++) begin
+        if (s_axi_wstrb[i]) regs[wr_index][(i*8)+:8] <= s_axi_wdata[(i*8)+:8];
+      end
+    end
+    if (rd_xfer) s_axi_rdata <= regs[rd_index];
+  end
+
+
+endmodule
+
+`default_nettype wire

From fbdde36cbd132d93d475c341046a657ffb7e53aa Mon Sep 17 00:00:00 2001
From: drewbabel <122849144+drewbabel@users.noreply.github.com>
Date: Thu, 30 Jul 2026 17:25:33 -0700
Subject: [PATCH 2/4] [tb] Add AXI4-Lite register testbench

---
 tb/axil_csr_tb.sv | 267 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 267 insertions(+)
 create mode 100644 tb/axil_csr_tb.sv

diff --git a/tb/axil_csr_tb.sv b/tb/axil_csr_tb.sv
new file mode 100644
index 0000000..85ad08e
--- /dev/null
+++ b/tb/axil_csr_tb.sv
@@ -0,0 +1,267 @@
+`default_nettype none
+
+module axil_csr_tb ();
+
+  int checks = 0;
+  int errors = 0;
+
+  localparam int AddrWidth = 4;
+  localparam int DataWidth = 32;
+  localparam int StrbWidth = DataWidth / 8;
+  localparam int NumRegs = 4;
+  localparam int Lsb = 2;
+
+  logic clk = 1'b0;
+  logic rst_n = 1'b1;
+  logic s_axi_awvalid = 1'b0;
+  logic s_axi_awready;
+  logic [AddrWidth-1:0] s_axi_awaddr = '0;
+  logic [2:0] s_axi_awprot = 3'b000;
+  logic s_axi_wvalid = 1'b0;
+  logic s_axi_wready;
+  logic [DataWidth-1:0] s_axi_wdata = '0;
+  logic [StrbWidth-1:0] s_axi_wstrb = '0;
+  logic s_axi_bvalid;
+  logic s_axi_bready = 1'b0;
+  logic [1:0] s_axi_bresp;
+  logic s_axi_arvalid = 1'b0;
+  logic s_axi_arready;
+  logic [AddrWidth-1:0] s_axi_araddr = '0;
+  logic [2:0] s_axi_arprot = 3'b000;
+  logic s_axi_rvalid;
+  logic s_axi_rready = 1'b0;
+  logic [DataWidth-1:0] s_axi_rdata;
+  logic [1:0] s_axi_rresp;
+
+  logic [DataWidth-1:0] ref_regs[NumRegs];
+  int stall = 0;
+
+  always #5 clk = ~clk;
+
+  axil_csr #(
+      .ADDR_WIDTH(AddrWidth),
+      .DATA_WIDTH(DataWidth)
+  ) dut (
+      .clk(clk),
+      .rst_n(rst_n),
+      .s_axi_awvalid(s_axi_awvalid),
+      .s_axi_awready(s_axi_awready),
+      .s_axi_awaddr(s_axi_awaddr),
+      .s_axi_awprot(s_axi_awprot),
+      .s_axi_wvalid(s_axi_wvalid),
+      .s_axi_wready(s_axi_wready),
+      .s_axi_wdata(s_axi_wdata),
+      .s_axi_wstrb(s_axi_wstrb),
+      .s_axi_bvalid(s_axi_bvalid),
+      .s_axi_bready(s_axi_bready),
+      .s_axi_bresp(s_axi_bresp),
+      .s_axi_arvalid(s_axi_arvalid),
+      .s_axi_arready(s_axi_arready),
+      .s_axi_araddr(s_axi_araddr),
+      .s_axi_arprot(s_axi_arprot),
+      .s_axi_rvalid(s_axi_rvalid),
+      .s_axi_rready(s_axi_rready),
+      .s_axi_rdata(s_axi_rdata),
+      .s_axi_rresp(s_axi_rresp)
+  );
+
+  task automatic do_reset();
+    rst_n = 1'b0;
+    s_axi_awvalid = 1'b0;
+    s_axi_wvalid = 1'b0;
+    s_axi_bready = 1'b0;
+    s_axi_arvalid = 1'b0;
+    s_axi_rready = 1'b0;
+    stall = 0;
+    @(posedge clk);
+    #1 rst_n = 1'b1;
+    @(posedge clk);
+  endtask  // Automatic
+
+  task automatic do_verdict();
+    @(posedge clk);
+    if (errors == 0) begin
+      $display("PASSED: %0d checks", checks);
+    end else begin
+      $display("FAILED: %0d checks, %0d errors", checks, errors);
+    end
+    $finish;
+  endtask  // Automatic
+
+  task automatic check_data(input string name, input logic [DataWidth-1:0] got,
+                            input logic [DataWidth-1:0] exp);
+    checks++;
+    if (got !== exp) begin
+      errors++;
+      $error("t=%0t %s mismatch: got=%h exp=%h", $time, name, got, exp);
+    end
+  endtask  // Automatic
+
+  task automatic check_resp(input string name, input logic [1:0] got);
+    checks++;
+    if (got !== 2'b00) begin
+      errors++;
+      $error("t=%0t %s not OKAY: got=%b", $time, name, got);
+    end
+  endtask  // Automatic
+
+  task automatic idle(input int cycles);
+    repeat (cycles) @(posedge clk);
+  endtask  // Automatic
+
+  // Write transaction
+  task automatic axi_write(input int index, input logic [DataWidth-1:0] data,
+                           input logic [StrbWidth-1:0] strb);
+    #1;
+    s_axi_awaddr  = (AddrWidth)'(index << Lsb);
+    s_axi_awvalid = 1'b1;
+    s_axi_wdata   = data;
+    s_axi_wstrb   = strb;
+    s_axi_wvalid  = 1'b1;
+    do @(posedge clk); while (!(s_axi_awready && s_axi_wready));
+    #1 s_axi_awvalid = 1'b0;
+    s_axi_wvalid = 1'b0;
+
+    for (int i = 0; i < StrbWidth; i++) begin
+      if (strb[i]) ref_regs[index][(i*8)+:8] = data[(i*8)+:8];
+    end
+
+    idle(stall);
+    #1 s_axi_bready = 1'b1;
+    do @(posedge clk); while (!s_axi_bvalid);
+    check_resp("bresp", s_axi_bresp);
+    #1 s_axi_bready = 1'b0;
+  endtask  // Automatic
+
+  task automatic axi_read(input int index, output logic [DataWidth-1:0] data);
+    #1;
+    s_axi_araddr  = (AddrWidth)'(index << Lsb);
+    s_axi_arvalid = 1'b1;
+    do @(posedge clk); while (!s_axi_arready);
+    #1 s_axi_arvalid = 1'b0;
+
+    idle(stall);
+    #1 s_axi_rready = 1'b1;
+    do @(posedge clk); while (!s_axi_rvalid);
+    data = s_axi_rdata;
+    check_resp("rresp", s_axi_rresp);
+    #1 s_axi_rready = 1'b0;
+  endtask  // Automatic
+
+  task automatic read_check(input int index);
+    logic [DataWidth-1:0] got;
+    axi_read(index, got);
+    check_data($sformatf("reg%0d", index), got, ref_regs[index]);
+  endtask  // Automatic
+
+  // Read during write
+  task automatic read_during_write(input int index);
+    logic [DataWidth-1:0] prev;
+    prev = ref_regs[index];
+    #1;
+    s_axi_araddr  = (AddrWidth)'(index << Lsb);
+    s_axi_arvalid = 1'b1;
+    do @(posedge clk); while (!s_axi_arready);
+    #1 s_axi_arvalid = 1'b0;
+    do @(posedge clk); while (!s_axi_rvalid);
+
+    axi_write(index, ~prev, '1);
+    check_data("rdata held", s_axi_rdata, prev);
+
+    #1 s_axi_rready = 1'b1;
+    @(posedge clk);
+    check_data("rdata delivered", s_axi_rdata, prev);
+    check_resp("rresp", s_axi_rresp);
+    #1 s_axi_rready = 1'b0;
+    read_check(index);
+  endtask  // Automatic
+
+  task automatic write_all(input logic [DataWidth-1:0] data, input logic [StrbWidth-1:0] strb);
+    for (int i = 0; i < NumRegs; i++) axi_write(i, data, strb);
+  endtask  // Automatic
+
+  initial begin
+    logic [DataWidth-1:0] data;
+    logic [StrbWidth-1:0] strb;
+    int index;
+
+    $dumpfile("tb.vcd");
+    $dumpvars(0, axil_csr_tb);
+    do_reset();
+
+    // Write then read
+    write_all(32'h0000_0000, '1);
+    for (int i = 0; i < NumRegs; i++) begin
+      axi_write(i, 32'hA5A5_0000 + (DataWidth)'(i), '1);
+      read_check(i);
+    end
+
+    // Register independence
+    write_all(32'hFFFF_FFFF, '1);
+    axi_write(2, 32'h0000_0000, '1);
+    for (int i = 0; i < NumRegs; i++) read_check(i);
+
+    // Single byte lanes
+    write_all(32'hFFFF_FFFF, '1);
+    for (int i = 0; i < StrbWidth; i++) begin
+      axi_write(1, 32'h1122_3344, (StrbWidth)'(1 << i));
+      read_check(1);
+    end
+
+    // No strobes
+    axi_write(3, 32'hDEAD_BEEF, '0);
+    read_check(3);
+
+    // Read during write
+    write_all(32'h1357_9BDF, '1);
+    for (int i = 0; i < NumRegs; i++) read_during_write(i);
+
+    // Random then stalled
+    for (int pass = 0; pass < 2; pass++) begin
+      stall = pass;
+      repeat (200) begin
+        index = $urandom % NumRegs;
+        data  = (DataWidth)'($urandom);
+        strb  = (StrbWidth)'($urandom);
+        axi_write(index, data, strb);
+        read_check(index);
+      end
+      for (int i = 0; i < NumRegs; i++) read_check(i);
+    end
+
+    // Consecutive writes
+    stall = 0;
+    repeat (20) begin
+      index = $urandom % NumRegs;
+      axi_write(index, (DataWidth)'($urandom), '1);
+    end
+    for (int i = 0; i < NumRegs; i++) read_check(i);
+
+    do_verdict();
+  end
+
+  // Watchdog
+  initial begin
+    #200_000_000 $fatal(1, "TIMEOUT: sim exceeded max time");
+  end
+
+  // Payload stability
+  logic reg_bvalid;
+  logic reg_rvalid;
+  logic [DataWidth-1:0] reg_rdata;
+
+  always @(posedge clk) begin
+    reg_bvalid <= s_axi_bvalid;
+    reg_rvalid <= s_axi_rvalid && !s_axi_rready;
+    reg_rdata  <= s_axi_rdata;
+  end
+
+  always @(negedge clk) begin
+    if (rst_n && reg_rvalid) begin
+      check_data("rdata stable", s_axi_rdata, reg_rdata);
+    end
+  end
+
+endmodule
+
+`default_nettype wire

From be9479e22ad0e237b8c45ad674ef76d1cabee7e7 Mon Sep 17 00:00:00 2001
From: drewbabel <122849144+drewbabel@users.noreply.github.com>
Date: Thu, 30 Jul 2026 17:25:34 -0700
Subject: [PATCH 3/4] [formal] Prove AXI4-Lite compliance

---
 formal/axil_csr.sby  |  22 ++
 formal/faxil_slave.v | 805 +++++++++++++++++++++++++++++++++++++++++++
 rtl/axil_csr.sv      |  93 +++++
 3 files changed, 920 insertions(+)
 create mode 100644 formal/axil_csr.sby
 create mode 100644 formal/faxil_slave.v

diff --git a/formal/axil_csr.sby b/formal/axil_csr.sby
new file mode 100644
index 0000000..e1997bf
--- /dev/null
+++ b/formal/axil_csr.sby
@@ -0,0 +1,22 @@
+[tasks]
+prove
+cover
+
+[options]
+prove: mode prove
+cover: mode cover
+cover: depth 40
+
+[engines]
+prove: smtbmc z3
+prove: abc pdr
+cover: smtbmc z3
+
+[script]
+read -formal axil_csr.sv
+read -formal faxil_slave.v
+prep -top axil_csr
+
+[files]
+formal/faxil_slave.v
+rtl/axil_csr.sv
diff --git a/formal/faxil_slave.v b/formal/faxil_slave.v
new file mode 100644
index 0000000..e4a8767
--- /dev/null
+++ b/formal/faxil_slave.v
@@ -0,0 +1,805 @@
+////////////////////////////////////////////////////////////////////////////////
+//
+// Filename:	bench/formal/faxil_slave.v
+// {{{
+// Project:	WB2AXIPSP: bus bridges and other odds and ends
+//
+// Purpose:
+//
+// Creator:	Dan Gisselquist, Ph.D.
+//		Gisselquist Technology, LLC
+//
+////////////////////////////////////////////////////////////////////////////////
+// }}}
+// Copyright (C) 2018-2025, Gisselquist Technology, LLC
+// {{{
+// This file is part of the WB2AXIP project.
+//
+// The WB2AXIP project contains free software and gateware, licensed under the
+// Apache License, Version 2.0 (the "License").  You may not use this project,
+// or this file, except in compliance with the License.  You may obtain a copy
+// of the License at
+// }}}
+//	http://www.apache.org/licenses/LICENSE-2.0
+// {{{
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
+// WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.  See the
+// License for the specific language governing permissions and limitations
+// under the License.
+//
+////////////////////////////////////////////////////////////////////////////////
+//
+`default_nettype	none
+// }}}
+module faxil_slave #(
+	// {{{
+	parameter  C_AXI_DATA_WIDTH	= 32,// Fixed, width of the AXI R&W data
+	parameter  C_AXI_ADDR_WIDTH	= 28,// AXI Address width (log wordsize)
+	// F_OPT_XILINX, Certain Xilinx cores impose additional rules upon AXI
+	// write transactions, limiting how far the write and write address
+	// can be apart.  If F_OPT_XILINX is set, these rules will be applied
+	// here as well.  See in-line for more details.
+	parameter [0:0]	F_OPT_XILINX = 1'b0,
+	// F_OPT_WRITE_ONLY, if set, will assume the master is always idle on
+	// te read channel, allowing you to test/focus on the write interface
+	parameter [0:0]	F_OPT_WRITE_ONLY  = 1'b0,
+	// F_OPT_READ_ONLY, if set, will assume the master is always idle on
+	// the write channel, while asserting that all of the associated returns
+	// and counters are zero
+	parameter [0:0]	F_OPT_READ_ONLY = 1'b0,
+	// F_OPT_BRESP: Allow any type of write response.  If set clear, then
+	// error responses are disallowed.
+	parameter [0:0]	F_OPT_BRESP = 1'b1,
+	// F_OPT_RRESP, if cleared, will disallow error responses
+	parameter [0:0]	F_OPT_RRESP = 1'b1,
+	// F_OPT_ASSUME_RESET, if set, will cause the design to *assume* the
+	// existence of a correct reset, rather than asserting it.  It is
+	// appropriate anytime the reset logic is outside of the circuit being
+	// examined
+	parameter [0:0]			F_OPT_ASSUME_RESET = 1'b1,
+	parameter [0:0]			F_OPT_NO_RESET = 1'b1,
+	//
+	// F_OPT_ASYNC_RESET is for those designs that will reset the channels
+	// using an asynchronous reset.  In these cases, the stability
+	// properties only apply when the async reset is not asserted.
+	// Likewise, when F_OPT_ASYNC_RESET is set, the reset assertions are
+	// applied *on the same clock cycle*, in addition to one cycle later.
+	parameter [0:0]			F_OPT_ASYNC_RESET = 1'b0,
+	parameter 			F_OPT_COVER_BURST = 0,
+	// F_LGDEPTH is the number of bits necessary to count the maximum
+	// number of items in flight.
+	parameter			F_LGDEPTH	= 4,
+	// F_AXI_MAXWAIT is the maximum number of clock cycles the
+	// master should have to wait for a slave to raise its ready flag to
+	// accept a request.  Set to zero for no limit.
+	parameter			F_AXI_MAXWAIT  = 12,
+	// F_AXI_MAXRSTALL is the maximum number of clock cycles the
+	// slave should have to wait with a return valid signal high, but
+	// while the master's return ready signal is low.  Set to zero for no
+	// limit.
+	parameter			F_AXI_MAXRSTALL= 12,
+	// F_AXI_MAXDELAY is the maximum number of clock cycles between request
+	// and response within the slave.  Set this to zero for no limit.
+	parameter			F_AXI_MAXDELAY = 12,
+	//
+	parameter [0:0]			F_OPT_INITIAL = 1'b1,
+
+	//
+	localparam DW			= C_AXI_DATA_WIDTH,
+	localparam AW			= C_AXI_ADDR_WIDTH
+	// }}}
+	) (
+		// {{{
+		input	wire			i_clk,	// System clock
+		input	wire			i_axi_reset_n,
+
+		// AXI write address channel signals
+		// {{{
+		input	wire			i_axi_awvalid,
+		input	wire			i_axi_awready,
+		input	wire	[AW-1:0]	i_axi_awaddr,	// Write address
+		input	wire	[2:0]		i_axi_awprot,	// Protection
+		// }}}
+		// AXI write data channel signals
+		// {{{
+		input	wire			i_axi_wvalid,
+		input	wire			i_axi_wready,
+		input	wire	[DW-1:0]	i_axi_wdata,	// Write data
+		input	wire	[DW/8-1:0]	i_axi_wstrb,	// Write strobes
+		// }}}
+		// AXI write response channel signals
+		// {{{
+		input	wire			i_axi_bvalid,
+		input	wire			i_axi_bready,
+		input	wire	[1:0]		i_axi_bresp,	// Wr response
+		// }}}
+		// AXI read address channel signals
+		// {{{
+		input	wire			i_axi_arvalid,
+		input	wire			i_axi_arready,
+		input	wire	[AW-1:0]	i_axi_araddr,	// Read address
+		input	wire	[2:0]		i_axi_arprot,	// Protection
+		// }}}
+		// AXI read data channel signals
+		// {{{
+		input	wire			i_axi_rvalid,
+		input	wire			i_axi_rready,
+		input	wire	[DW-1:0]	i_axi_rdata,	// Read data
+		input	wire	[1:0]		i_axi_rresp,	// Read response
+		// }}}
+		output	reg	[(F_LGDEPTH-1):0]	f_axi_rd_outstanding,
+		output	reg	[(F_LGDEPTH-1):0]	f_axi_wr_outstanding,
+		output	reg	[(F_LGDEPTH-1):0]	f_axi_awr_outstanding
+		// }}}
+	);
+
+	localparam	MAX_SLAVE_TIMEOUT = (F_AXI_MAXWAIT > F_AXI_MAXDELAY)
+				? (F_AXI_MAXWAIT) : F_AXI_MAXDELAY;
+	localparam	MAX_TIMEOUT = (F_AXI_MAXRSTALL>MAX_SLAVE_TIMEOUT)
+				? (F_AXI_MAXRSTALL) : MAX_SLAVE_TIMEOUT;
+	localparam	LGTIMEOUT = $clog2(MAX_TIMEOUT+1);
+
+//*****************************************************************************
+// Parameter declarations
+//*****************************************************************************
+
+//*****************************************************************************
+// Internal register and wire declarations
+//*****************************************************************************
+
+	// wire	w_fifo_full;
+	wire	axi_rd_ack, axi_wr_ack, axi_ard_req, axi_awr_req, axi_wr_req;
+		// axi_rd_err, axi_wr_err;
+	reg		f_past_valid;
+	reg	[3:0]	f_reset_length;
+	// integer	k;
+
+	assign	axi_ard_req = (i_axi_arvalid)&&(i_axi_arready) && i_axi_reset_n;
+	assign	axi_awr_req = (i_axi_awvalid)&&(i_axi_awready) && i_axi_reset_n;
+	assign	axi_wr_req  = (i_axi_wvalid )&&(i_axi_wready) && i_axi_reset_n;
+	//
+	assign	axi_rd_ack = (i_axi_rvalid)&&(i_axi_rready) && i_axi_reset_n;
+	assign	axi_wr_ack = (i_axi_bvalid)&&(i_axi_bready) && i_axi_reset_n;
+	// assign axi_rd_err = (axi_rd_ack)&&(i_axi_rresp[1]) && i_axi_reset_n;
+	// assign axi_wr_err = (axi_wr_ack)&&(i_axi_bresp[1]) && i_axi_reset_n;
+
+`define	SLAVE_ASSUME	assume
+`define	SLAVE_ASSERT	assert
+
+	//
+	// Setup
+	//
+
+	initial	f_past_valid = 1'b0;
+	always @(posedge i_clk)
+		f_past_valid <= 1'b1;
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Reset properties
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+
+	//
+	// Insist that the reset signal start out asserted (negative), and
+	// remain so for 16 clocks.
+	//
+
+	generate if (F_OPT_ASSUME_RESET)
+	begin : ASSUME_INITIAL_RESET
+		always @(*)
+		if (!f_past_valid)
+			assume(!i_axi_reset_n);
+	end else begin : ASSERT_INITIAL_RESET
+		always @(*)
+		if (!f_past_valid)
+			assert(!i_axi_reset_n);
+	end endgenerate
+
+
+	//
+	// If asserted, the reset must be asserted for a minimum of 16 clocks
+	initial	f_reset_length = 0;
+	always @(posedge i_clk)
+	if (F_OPT_NO_RESET || i_axi_reset_n)
+		f_reset_length <= 0;
+	else if (!(&f_reset_length))
+		f_reset_length <= f_reset_length + 1'b1;
+
+
+	//
+	// If the reset is not generated within this particular core, then it
+	// can be assumed if F_OPT_ASSUME_RESET is set
+	generate if (F_OPT_ASSUME_RESET && !F_OPT_NO_RESET)
+	begin : ASSUME_RESET
+		always @(posedge i_clk)
+		if ((f_past_valid)&&(!$past(i_axi_reset_n))&&(!$past(&f_reset_length)))
+			assume(!i_axi_reset_n);
+
+		always @(*)
+		if ((f_reset_length > 0)&&(f_reset_length < 4'hf))
+			assume(!i_axi_reset_n);
+
+	end else if (!F_OPT_NO_RESET)
+	begin : ASSERT_RESET
+
+		always @(posedge i_clk)
+		if ((f_past_valid)&&(!$past(i_axi_reset_n))&&(!$past(&f_reset_length)))
+			assert(!i_axi_reset_n);
+
+		always @(*)
+		if ((f_reset_length > 0)&&(f_reset_length < 4'hf))
+			assert(!i_axi_reset_n);
+
+	end endgenerate
+
+	//
+	// All of the xVALID signals *MUST* be set low on the clock following
+	// a reset.  Not in the spec, but also checked here is that they must
+	// also be set low initially.
+	always @(posedge i_clk)
+	if ((!f_past_valid && F_OPT_INITIAL)
+				||(f_past_valid && !$past(i_axi_reset_n)))
+	begin
+		`SLAVE_ASSUME(!i_axi_arvalid);
+		`SLAVE_ASSUME(!i_axi_awvalid);
+		`SLAVE_ASSUME(!i_axi_wvalid);
+		//
+		`SLAVE_ASSERT(!i_axi_bvalid);
+		`SLAVE_ASSERT(!i_axi_rvalid);
+	end
+
+	generate if (F_OPT_ASYNC_RESET)
+	begin
+		always @(*)
+		if (!i_axi_reset_n)
+		begin
+			`SLAVE_ASSUME(!i_axi_arvalid);
+			`SLAVE_ASSUME(!i_axi_awvalid);
+			`SLAVE_ASSUME(!i_axi_wvalid);
+			//
+			`SLAVE_ASSERT(!i_axi_bvalid);
+			`SLAVE_ASSERT(!i_axi_rvalid);
+		end
+	end endgenerate
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// xRESP checking
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+
+	always @(*)
+	if ((i_axi_bvalid)&&(!F_OPT_BRESP)&&(F_OPT_INITIAL || i_axi_reset_n))
+		`SLAVE_ASSERT(i_axi_bresp == 0);
+	always @(*)
+	if ((i_axi_rvalid)&&(!F_OPT_RRESP)&&(F_OPT_INITIAL || i_axi_reset_n))
+		`SLAVE_ASSERT(i_axi_rresp == 0);
+	always @(*)
+	if (i_axi_bvalid&&(F_OPT_INITIAL || i_axi_reset_n))
+		`SLAVE_ASSERT(i_axi_bresp != 2'b01); // Exclusive access not allowed
+	always @(*)
+	if (i_axi_rvalid&&(F_OPT_INITIAL || i_axi_reset_n))
+		`SLAVE_ASSERT(i_axi_rresp != 2'b01); // Exclusive access not allowed
+
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Stability properties--what happens if valid and not ready
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+
+	// Assume any response from the bus will not change prior to that
+	// response being accepted
+	always @(posedge i_clk)
+	if ((f_past_valid)&&($past(i_axi_reset_n))
+			&&(!F_OPT_ASYNC_RESET || i_axi_reset_n))
+	begin
+		// Write address channel
+		if ((f_past_valid)&&($past(i_axi_awvalid && !i_axi_awready)))
+		begin
+			`SLAVE_ASSUME(i_axi_awvalid);
+			`SLAVE_ASSUME($stable(i_axi_awaddr));
+			`SLAVE_ASSUME($stable(i_axi_awprot));
+		end
+
+		// Write data channel
+		if ((f_past_valid && (!F_OPT_ASYNC_RESET || i_axi_reset_n))
+				&&($past(i_axi_wvalid && !i_axi_wready)))
+		begin
+			`SLAVE_ASSUME(i_axi_wvalid);
+			`SLAVE_ASSUME($stable(i_axi_wstrb));
+			`SLAVE_ASSUME($stable(i_axi_wdata));
+		end
+
+		// Incoming Read address channel
+		if ((f_past_valid && (!F_OPT_ASYNC_RESET || i_axi_reset_n))
+			&&($past(i_axi_arvalid && !i_axi_arready)))
+		begin
+			`SLAVE_ASSUME(i_axi_arvalid);
+			`SLAVE_ASSUME($stable(i_axi_araddr));
+			`SLAVE_ASSUME($stable(i_axi_arprot));
+		end
+
+		if ((f_past_valid && (!F_OPT_ASYNC_RESET || i_axi_reset_n))
+			&&($past(i_axi_rvalid && !i_axi_rready)))
+		begin
+			`SLAVE_ASSERT(i_axi_rvalid);
+			`SLAVE_ASSERT($stable(i_axi_rresp));
+			`SLAVE_ASSERT($stable(i_axi_rdata));
+		end
+
+		if ((f_past_valid && (!F_OPT_ASYNC_RESET || i_axi_reset_n))
+			&&($past(i_axi_bvalid && !i_axi_bready)))
+		begin
+			`SLAVE_ASSERT(i_axi_bvalid);
+			`SLAVE_ASSERT($stable(i_axi_bresp));
+		end
+	end
+
+	// Nothing should be returned or requested on the first clock
+	generate if (F_OPT_INITIAL)
+	begin : INITIAL_VALUE_CHECKS
+		initial	`SLAVE_ASSUME(!i_axi_arvalid);
+		initial	`SLAVE_ASSUME(!i_axi_awvalid);
+		initial	`SLAVE_ASSUME(!i_axi_wvalid);
+		//
+		initial	`SLAVE_ASSERT(!i_axi_bvalid);
+		initial	`SLAVE_ASSERT(!i_axi_rvalid);
+	end endgenerate
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	// Insist upon a maximum delay before a request is accepted
+	//
+	//
+	////////////////////////////////////////////////////////////////////////
+	//
+	generate if (F_AXI_MAXWAIT > 0)
+	begin : CHECK_STALL_COUNT
+		reg	[LGTIMEOUT-1:0]		f_axi_awstall,
+						f_axi_wstall,
+						f_axi_arstall;
+
+		//
+		// AXI write address channel
+		//
+		// Count the number of times AWVALID is true while AWREADY
+		// is false.  These are stalls, and we want to insist on a
+		// minimum number of them.  However, if BVALID && !BREADY,
+		// then there's a reason for not accepting anything more.
+		// Similarly, many cores will only ever accept one request
+		// at a time, hence we won't count things as stalls if
+		// WR-PENDING > 0.
+		initial	f_axi_awstall = 0;
+		always @(posedge i_clk)
+		if ((!i_axi_reset_n)||(!i_axi_awvalid)||(i_axi_awready)
+				||(i_axi_bvalid))
+			f_axi_awstall <= 0;
+		else if ((f_axi_awr_outstanding >= f_axi_wr_outstanding)
+			&&(i_axi_awvalid && !i_axi_wvalid))
+			// If we are waiting for the write channel to be valid
+			// then don't count stalls
+			f_axi_awstall <= 0;
+		else
+			f_axi_awstall <= f_axi_awstall + 1'b1;
+
+		always @(*)
+			`SLAVE_ASSERT(f_axi_awstall < F_AXI_MAXWAIT);
+
+		//
+		// AXI write data channel
+		//
+		// Count the number of clock cycles that the write data
+		// channel is stalled, that is while WVALID && !WREADY.
+		// Since things can back up if BVALID & !BREADY, we avoid
+		// counting clock cycles in that circumstance
+		initial	f_axi_wstall = 0;
+		always @(posedge i_clk)
+		if ((!i_axi_reset_n)||(!i_axi_wvalid)||(i_axi_wready)
+				||(i_axi_bvalid))
+			f_axi_wstall <= 0;
+		else if ((f_axi_wr_outstanding >= f_axi_awr_outstanding)
+			&&(!i_axi_awvalid && i_axi_wvalid))
+			// If we are waiting for the write address channel
+			// to be valid, then don't count stalls
+			f_axi_wstall <= 0;
+		else
+			f_axi_wstall <= f_axi_wstall + 1'b1;
+
+		always @(*)
+			`SLAVE_ASSERT(f_axi_wstall < F_AXI_MAXWAIT);
+
+		//
+		// AXI read address channel
+		//
+		// Similar to the first two above, once the master raises
+		// ARVALID, insist that the slave respond within a minimum
+		// number of clock cycles.  Exceptions include any time
+		// RVALID is true, since that can back up the whole system,
+		// and any time the number of bursts is greater than zero,
+		// since many slaves can only accept one request at a time.
+		initial	f_axi_arstall = 0;
+		always @(posedge i_clk)
+		if ((!i_axi_reset_n)||(!i_axi_arvalid)||(i_axi_arready)
+				||(i_axi_rvalid))
+			f_axi_arstall <= 0;
+		else
+			f_axi_arstall <= f_axi_arstall + 1'b1;
+
+		always @(*)
+			`SLAVE_ASSERT(f_axi_arstall < F_AXI_MAXWAIT);
+
+	end endgenerate
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	// Insist upon a maximum delay before any response is accepted
+	//
+	// These are separate from the earlier ones, in case you wish to
+	// control them separately.  For example, an interconnect might be
+	// forced to let a channel wait indefinitely for access, but it might
+	// not be appropriate to require the response to be able to wait
+	// indefinitely as well
+	//
+	////////////////////////////////////////////////////////////////////////
+	//
+	generate if (F_AXI_MAXRSTALL > 0)
+	begin : CHECK_RESPONSE_STALLS
+		reg	[LGTIMEOUT-1:0]		f_axi_bstall,
+						f_axi_rstall;
+
+		// AXI write response channel
+		//
+		// Insist on a maximum number of clocks that BVALID can be
+		// high while BREADY is low
+		initial	f_axi_bstall = 0;
+		always @(posedge i_clk)
+		if ((!i_axi_reset_n)||(!i_axi_bvalid)||(i_axi_bready))
+			f_axi_bstall <= 0;
+		else
+			f_axi_bstall <= f_axi_bstall + 1'b1;
+
+		always @(*)
+			`SLAVE_ASSUME(f_axi_bstall < F_AXI_MAXRSTALL);
+
+		// AXI read response channel
+		//
+		// Insist on a maximum number of clocks that RVALID can be
+		// high while RREADY is low
+		initial	f_axi_rstall = 0;
+		always @(posedge i_clk)
+		if ((!i_axi_reset_n)||(!i_axi_rvalid)||(i_axi_rready))
+			f_axi_rstall <= 0;
+		else
+			f_axi_rstall <= f_axi_rstall + 1'b1;
+
+		always @(*)
+			`SLAVE_ASSUME(f_axi_rstall < F_AXI_MAXRSTALL);
+
+	end endgenerate
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	// Xilinx extensions/guarantees to the AXI protocol
+	//
+	//	1. The address line will never be more than two clocks ahead of
+	//		the write data channel, and
+	//	2. The write data channel will never be more than one clock
+	//		ahead of the address channel.
+	//
+	//
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	generate if (F_OPT_XILINX)
+	begin
+		// Rule number one:
+		always @(posedge i_clk)
+		if ((i_axi_reset_n)&&($past(i_axi_reset_n))
+			&&($past(i_axi_awvalid && !i_axi_wvalid,2))
+				&&($past(f_axi_awr_outstanding>=f_axi_wr_outstanding,2))
+				&&(!$past(i_axi_wvalid)))
+			`SLAVE_ASSUME(i_axi_wvalid);
+
+		always @(posedge i_clk)
+		if ((i_axi_reset_n)
+				&&(f_axi_awr_outstanding > 1)
+				&&(f_axi_awr_outstanding-1 > f_axi_wr_outstanding))
+			`SLAVE_ASSUME(i_axi_wvalid);
+
+		always @(posedge i_clk)
+		if ((i_axi_reset_n)
+				&&($past(f_axi_awr_outstanding > f_axi_wr_outstanding))
+				&&(!$past(axi_wr_req)))
+			`SLAVE_ASSUME(i_axi_wvalid);
+
+
+		// Rule number two:
+		always @(posedge i_clk)
+		if ((i_axi_reset_n)&&(f_axi_awr_outstanding < f_axi_wr_outstanding))
+			`SLAVE_ASSUME(i_axi_awvalid);
+	end endgenerate
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	// Count outstanding transactions.  With these measures, we count
+	// once per any burst.
+	//
+	//
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+
+	//
+	// Count outstanding write address channel requests
+	initial	f_axi_awr_outstanding = 0;
+	always @(posedge i_clk)
+	if (!i_axi_reset_n)
+		f_axi_awr_outstanding <= 0;
+	else case({ (axi_awr_req), (axi_wr_ack) })
+		2'b10: f_axi_awr_outstanding <= f_axi_awr_outstanding + 1'b1;
+		2'b01: f_axi_awr_outstanding <= f_axi_awr_outstanding - 1'b1;
+		default: begin end
+	endcase
+
+	//
+	// Count outstanding write data channel requests
+	initial	f_axi_wr_outstanding = 0;
+	always @(posedge i_clk)
+	if (!i_axi_reset_n)
+		f_axi_wr_outstanding <= 0;
+	else case({ (axi_wr_req), (axi_wr_ack) })
+	2'b01: f_axi_wr_outstanding <= f_axi_wr_outstanding - 1'b1;
+	2'b10: f_axi_wr_outstanding <= f_axi_wr_outstanding + 1'b1;
+	default: begin end
+	endcase
+
+	//
+	// Count outstanding read requests
+	initial	f_axi_rd_outstanding = 0;
+	always @(posedge i_clk)
+	if (!i_axi_reset_n)
+		f_axi_rd_outstanding <= 0;
+	else case({ (axi_ard_req), (axi_rd_ack) })
+	2'b01: f_axi_rd_outstanding <= f_axi_rd_outstanding - 1'b1;
+	2'b10: f_axi_rd_outstanding <= f_axi_rd_outstanding + 1'b1;
+	default: begin end
+	endcase
+
+	//
+	// Do not let the number of outstanding requests overflow
+	always @(posedge i_clk)
+		`SLAVE_ASSERT(f_axi_wr_outstanding  < {(F_LGDEPTH){1'b1}});
+	always @(posedge i_clk)
+		`SLAVE_ASSERT(f_axi_awr_outstanding < {(F_LGDEPTH){1'b1}});
+	always @(posedge i_clk)
+		`SLAVE_ASSERT(f_axi_rd_outstanding  < {(F_LGDEPTH){1'b1}});
+
+	//
+	// That means that requests need to stop when we're almost full
+	always @(posedge i_clk)
+	if ((F_OPT_INITIAL || i_axi_reset_n) && f_axi_awr_outstanding == { {(F_LGDEPTH-1){1'b1}}, 1'b0} )
+		assert(!i_axi_awready);
+	always @(posedge i_clk)
+	if ((F_OPT_INITIAL || i_axi_reset_n) && f_axi_wr_outstanding == { {(F_LGDEPTH-1){1'b1}}, 1'b0} )
+		assert(!i_axi_wready);
+	always @(posedge i_clk)
+	if ((F_OPT_INITIAL || i_axi_reset_n) && f_axi_rd_outstanding == { {(F_LGDEPTH-1){1'b1}}, 1'b0} )
+		assert(!i_axi_arready);
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	// Insist that all responses are returned in less than a maximum delay
+	// In this case, we count responses within a burst, rather than entire
+	// bursts.
+	//
+	//
+	// A unique feature to the backpressure mechanism within AXI is that
+	// we have to reset our delay counters in the case of any push back,
+	// since the response can't move forward if the master isn't (yet)
+	// ready for it.
+	//
+	////////////////////////////////////////////////////////////////////////
+	generate if (F_AXI_MAXDELAY > 0)
+	begin : CHECK_MAX_DELAY
+
+		reg	[LGTIMEOUT-1:0]		f_axi_wr_ack_delay,
+						f_axi_rd_ack_delay;
+
+		//
+		// Count the clock cycles a write request (address + data) has
+		// been outstanding and without any response
+		initial	f_axi_wr_ack_delay = 0;
+		always @(posedge i_clk)
+		if ((!i_axi_reset_n)||(i_axi_bvalid)
+				||(f_axi_awr_outstanding==0)
+				||(f_axi_wr_outstanding==0))
+			f_axi_wr_ack_delay <= 0;
+		else if (f_axi_wr_outstanding > 0)
+			f_axi_wr_ack_delay <= f_axi_wr_ack_delay + 1'b1;
+
+		//
+		// Count the clock cycles that any read request has been
+		// outstanding, but without any response.
+		initial	f_axi_rd_ack_delay = 0;
+		always @(posedge i_clk)
+		if ((!i_axi_reset_n)||(i_axi_rvalid)||(f_axi_rd_outstanding==0))
+			f_axi_rd_ack_delay <= 0;
+		else
+			f_axi_rd_ack_delay <= f_axi_rd_ack_delay + 1'b1;
+
+
+		//
+		// Assert that write responses will be returned in a timely
+		// fashion
+		always @(*)
+			`SLAVE_ASSERT(f_axi_wr_ack_delay < F_AXI_MAXDELAY);
+
+		//
+		// Assert that read responses will be returned in a timely
+		// fashion
+		always @(*)
+			`SLAVE_ASSERT(f_axi_rd_ack_delay < F_AXI_MAXDELAY);
+
+	end endgenerate
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	// Assume acknowledgements must follow requests
+	//
+	// The f_axi*outstanding counters count the number of requests.  No
+	// acknowledgment should issue without a pending request
+	// burst.  Further, the spec is clear: you can't acknowledge something
+	// on the same clock you get the request.  There must be at least one
+	// clock delay.
+	//
+	//
+	////////////////////////////////////////////////////////////////////////
+
+	//
+	// AXI write response channel
+	//
+	always @(posedge i_clk)
+	if (i_axi_bvalid && (F_OPT_INITIAL || i_axi_reset_n))
+	begin
+		// No BVALID w/o an outstanding request
+		`SLAVE_ASSERT(f_axi_awr_outstanding > 0);
+		`SLAVE_ASSERT(f_axi_wr_outstanding  > 0);
+	end
+
+	//
+	// AXI read data channel signals
+	//
+	always @(posedge i_clk)
+	if (i_axi_rvalid && (F_OPT_INITIAL || i_axi_reset_n))
+		// No RVALID w/o an outstanding request
+		`SLAVE_ASSERT(f_axi_rd_outstanding > 0);
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	// F_OPT_WRITE_ONLY or F_OPT_READ_ONLY
+	//
+	// Optionally disable either read or write channels (or both??)
+	//
+	//
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	initial	assert((!F_OPT_WRITE_ONLY)||(!F_OPT_READ_ONLY));
+
+	generate if (F_OPT_WRITE_ONLY)
+	begin : NO_READS
+
+		// If there are no read requests (assumed), there should be
+		// no read responses
+		always @(*)
+			`SLAVE_ASSUME(i_axi_arvalid == 0);
+		always @(*)
+			assert(f_axi_rd_outstanding == 0);
+		always @(*)
+			`SLAVE_ASSERT(i_axi_rvalid == 0);
+
+	end endgenerate
+
+	generate if (F_OPT_READ_ONLY)
+	begin : NO_WRITES
+
+		// If there are no write requests (assumed, address or data),
+		// there should be no read responses
+		always @(*)
+			`SLAVE_ASSUME(i_axi_awvalid == 0);
+		always @(*)
+			`SLAVE_ASSUME(i_axi_wvalid == 0);
+		always @(*)
+			assert(f_axi_wr_outstanding == 0);
+		always @(*)
+			assert(f_axi_awr_outstanding == 0);
+		always @(*)
+			`SLAVE_ASSERT(i_axi_bvalid == 0);
+
+	end endgenerate
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	// Cover properties
+	//
+	// We'll use this to prove that transactions are even possible, and
+	// hence that we haven't so constrained the bus that nothing can take
+	// place.
+	//
+	//
+	////////////////////////////////////////////////////////////////////////
+
+	//
+	// AXI write response channel
+	//
+	generate if (!F_OPT_READ_ONLY)
+	begin
+		always @(posedge i_clk)
+			// Make sure we can get a write acknowledgment
+			cover((i_axi_bvalid)&&(i_axi_bready));
+	end endgenerate
+
+	//
+	// AXI read response channel
+	//
+	generate if (!F_OPT_WRITE_ONLY)
+	begin
+		always @(posedge i_clk)
+			// Make sure we can get a response from the read channel
+			cover((i_axi_rvalid)&&(i_axi_rready));
+	end endgenerate
+
+	generate if (!F_OPT_READ_ONLY && F_OPT_COVER_BURST > 0)
+	begin : COVER_WRITE_BURSTS
+
+		reg	[31:0]	cvr_writes;
+
+		initial	cvr_writes = 0;
+		always @(posedge i_clk)
+		if (!i_axi_reset_n)
+			cvr_writes <= 0;
+		else if (i_axi_bvalid && i_axi_bready && i_axi_bresp == 2'b00
+				&& !(&cvr_writes))
+			cvr_writes <= cvr_writes + 1;
+
+		always @(*)
+			cover(cvr_writes == F_OPT_COVER_BURST);
+
+	end endgenerate
+
+	generate if (!F_OPT_WRITE_ONLY && F_OPT_COVER_BURST > 0)
+	begin : COVER_READ_BURSTS
+
+		reg	[31:0]	cvr_reads;
+
+		initial	cvr_reads = 0;
+		always @(posedge i_clk)
+		if (!i_axi_reset_n)
+			cvr_reads <= 0;
+		else if (i_axi_rvalid && i_axi_rready && i_axi_rresp == 2'b00
+				&& !(&cvr_reads))
+			cvr_reads <= cvr_reads + 1;
+
+		always @(*)
+			cover(cvr_reads == F_OPT_COVER_BURST);
+
+	end endgenerate
+
+`undef	SLAVE_ASSUME
+`undef	SLAVE_ASSERT
+endmodule
diff --git a/rtl/axil_csr.sv b/rtl/axil_csr.sv
index 8626a32..11b5c84 100644
--- a/rtl/axil_csr.sv
+++ b/rtl/axil_csr.sv
@@ -89,6 +89,99 @@ module axil_csr #(
     if (rd_xfer) s_axi_rdata <= regs[rd_index];
   end
 
+`ifdef FORMAL
+
+  localparam int LgDepth = 4;
+
+  logic [LgDepth-1:0] f_axi_awr_outstanding;
+  logic [LgDepth-1:0] f_axi_wr_outstanding;
+  logic [LgDepth-1:0] f_axi_rd_outstanding;
+
+  logic f_past_valid = 1'b0;
+  logic wr_done;
+  logic rd_done;
+
+  assign wr_done = s_axi_bvalid && s_axi_bready;
+  assign rd_done = s_axi_rvalid && s_axi_rready;
+
+  always_ff @(posedge clk) f_past_valid <= 1'b1;
+
+  initial begin
+    assume (!rst_n);
+    assume (s_axi_awvalid == 0);
+    assume (s_axi_wvalid == 0);
+    assume (s_axi_arvalid == 0);
+  end
+
+  always @(posedge clk) begin
+    if (rst_n) begin
+      cover (wr_done);
+      cover (rd_done);
+      cover (wr_done && rd_done);  // Same cycle
+      if (f_past_valid) begin
+        cover (s_axi_rvalid && $past(rd_xfer) && $past(rd_index) == f_index);  // Tracked read
+      end
+    end
+  end
+
+  // Solver chosen register
+  (* anyconst *) logic [IdxWidth-1:0] f_index;
+  logic [DATA_WIDTH-1:0] f_shadow;
+
+  always_ff @(posedge clk) begin
+    if (wr_xfer && wr_index == f_index) begin
+      for (int i = 0; i < $bits(s_axi_wstrb); i++) begin
+        if (s_axi_wstrb[i]) f_shadow[(i*8)+:8] <= s_axi_wdata[(i*8)+:8];
+      end
+    end
+  end
+
+  initial assume (f_shadow == regs[f_index]);
+
+  always @(posedge clk) begin
+    assert (f_shadow == regs[f_index]);
+    if (f_past_valid && s_axi_rvalid && $past(rd_xfer) && $past(rd_index) == f_index) begin
+      assert (s_axi_rdata == $past(f_shadow));
+    end
+  end
+
+  faxil_slave #(
+      .C_AXI_ADDR_WIDTH(ADDR_WIDTH),
+      .C_AXI_DATA_WIDTH(DATA_WIDTH),
+      .F_LGDEPTH(LgDepth),
+      .F_OPT_BRESP(1'b0),
+      .F_OPT_RRESP(1'b0),
+      .F_AXI_MAXWAIT(2),
+      .F_AXI_MAXDELAY(1),
+      .F_AXI_MAXRSTALL(0)
+  ) u_faxil (
+      .i_clk(clk),
+      .i_axi_reset_n(rst_n),
+      .i_axi_awvalid(s_axi_awvalid),
+      .i_axi_awready(s_axi_awready),
+      .i_axi_awaddr(s_axi_awaddr),
+      .i_axi_awprot(s_axi_awprot),
+      .i_axi_wvalid(s_axi_wvalid),
+      .i_axi_wready(s_axi_wready),
+      .i_axi_wdata(s_axi_wdata),
+      .i_axi_wstrb(s_axi_wstrb),
+      .i_axi_bvalid(s_axi_bvalid),
+      .i_axi_bready(s_axi_bready),
+      .i_axi_bresp(s_axi_bresp),
+      .i_axi_arvalid(s_axi_arvalid),
+      .i_axi_arready(s_axi_arready),
+      .i_axi_araddr(s_axi_araddr),
+      .i_axi_arprot(s_axi_arprot),
+      .i_axi_rvalid(s_axi_rvalid),
+      .i_axi_rready(s_axi_rready),
+      .i_axi_rdata(s_axi_rdata),
+      .i_axi_rresp(s_axi_rresp),
+      .f_axi_awr_outstanding(f_axi_awr_outstanding),
+      .f_axi_wr_outstanding(f_axi_wr_outstanding),
+      .f_axi_rd_outstanding(f_axi_rd_outstanding)
+  );
+
+`endif
 
 endmodule
 

From 25a1f0029aa2e237d486363b2187c26cd7ebd41c Mon Sep 17 00:00:00 2001
From: drewbabel <122849144+drewbabel@users.noreply.github.com>
Date: Thu, 30 Jul 2026 17:26:29 -0700
Subject: [PATCH 4/4] [docs] Document the AXI4-Lite block

---
 README.md | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index 4aa784d..acf0418 100644
--- a/README.md
+++ b/README.md
@@ -2,12 +2,13 @@
 
 [![CI](https://github.com/drewbabel/eth-datapath/actions/workflows/ci.yml/badge.svg)](https://github.com/drewbabel/eth-datapath/actions/workflows/ci.yml)
 
-Flow control and arbitration blocks for an Ethernet datapath in SystemVerilog, verified with reference-model testbenches and SymbiYosys proofs, with:
+Flow control, arbitration, and control-plane blocks for an Ethernet datapath in SystemVerilog, verified with reference-model testbenches and SymbiYosys proofs, with:
 
 - A credit sender that spends one credit per accepted beat and stalls its source at zero, which removes the need for a `ready` signal from the far end.
 - A receive FIFO that returns one credit per beat drained and presents its output as same-cycle `valid` through a holding register.
 - A round-robin arbiter that rotates its priority mask after each grant and holds a grant across a burst.
 - A synchronous FIFO whose pointers carry an extra wrap bit, separating full from empty with no occupancy counter.
+- An AXI4-Lite register block that honors byte-lane write strobes and answers every request the cycle after it accepts one.
 
 ## Verification
 
@@ -15,19 +16,23 @@ Flow control and arbitration blocks for an Ethernet datapath in SystemVerilog, v
 |--------|--------|
 | `credit_sender` + `credit_fifo` | Reference-model testbenches + two-engine SymbiYosys prove and cover |
 | `rr_arbiter` | Reference-model testbench + SymbiYosys bounded-wait fairness proof |
+| `axil_csr` | Reference-model testbench + SymbiYosys prove and cover against ZipCPU `faxil_slave` |
 | `sync_fifo` | Reference-model testbench |
 
 A credit sits in exactly one of four places, unspent in the sender, in flight forward, occupying a receive slot, or in flight back, and the four counts always sum to `DEPTH`. Receive-FIFO overflow follows from that sum and is unreachable from the receiver alone, which is why the proof instantiates both endpoints together with a model of the wire between them. The wire model neither drops nor duplicates a beat and is otherwise free to deliver on any schedule, so one proof covers every link latency.
 
+Bus compliance on the register block is judged by a third-party property set, Gisselquist's `faxil_slave`, rather than by properties written here. Those properties watch the handshakes and say nothing about stored data, so a shadow copy of one solver-chosen register carries the separate claim that a read returns what the write strobes put there.
+
 ## Implementation
 
-Synthesized for Xilinx 7-series through sv2v and Yosys, at the default `WIDTH` of 8 and `DEPTH` of 16.
+Synthesized for Xilinx 7-series through sv2v and Yosys, at each module's default parameters.
 
 | Module | LUTs | Flip-flops | Distributed RAM (bits) |
 |--------|------|------------|------------------------|
 | `credit_fifo` \* | 7 | 19 | 512 |
 | `credit_sender` | 8 | 5 | 0 |
 | `sync_fifo` | 8 | 18 | 512 |
+| `axil_csr` | 10 | 37 | 2048 |
 | `rr_arbiter` | 20 | 9 | 0 |
 
 \* Includes its `sync_fifo` instance, which holds all the distributed RAM and 18 of the 19 flip-flops.