[rtl] Add AXI4-Lite register block

README.md

@@ -2,32 +2,37 @@
 
 [![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
 
 | Module | Method |
 |--------|--------|
 | `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.

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