SymbiYosys tutorial · Chapter 6 of 10 · 15 min
Verify an AXI-Lite slave against a protocol checker
This chapter proves easyaxil, an AXI-Lite slave from wb2axip, against faxil_slave, a reusable file of AXI-Lite protocol properties. It uses the repository from Chapter 5. Writing the protocol rules once and reusing them is how wb2axip works: 23 of its 42 job files use faxil_slave.
What is AXI-Lite, and what does easyaxil do?
AXI-Lite is a bus protocol from Arm's AMBA AXI family for single register reads and writes, without bursts. It has five channels, each a valid/ready handshake: write address (AW), write data (W), write response (B), read address (AR) and read data (R).
A slave is the component that answers the requests. easyaxil, in rtl/easyaxil.v, is a slave with four 32-bit registers; its comments describe it as a demonstration of a simple AXI-Lite interface.
What does the protocol checker check?
bench/formal/faxil_slave.v states the AXI-Lite rules once, for any slave. Inside the file, the macro SLAVE_ASSUME means assume and SLAVE_ASSERT means assert. Rules for the signals the master drives are assumptions, so the solver acts as any master that follows the protocol. Rules for the signals the slave drives are assertions, so the proof checks easyaxil.
easyaxil proved against faxil_slave. The solver drives the master side; the checker watches all five channels.The checker also counts outstanding transactions, requests accepted but not yet answered, and outputs the counts: f_axi_rd_outstanding, f_axi_wr_outstanding and f_axi_awr_outstanding. Section "How deep must the induction step be?" uses them.
Run the AXI-Lite proofs
bench/formal/easyaxil.sby
[tasks]
prfreg prf
cvrreg cvr
prfskd prf opt_skidbuffer
cvrskd cvr opt_skidbuffer
prfreglp prf opt_lowpower
prfskdlp prf opt_skidbuffer opt_lowpower
[options]
prf: mode prove
prf: depth 3
cvr: mode cover
cvr: depth 40
[engines]
smtbmc
[script]
read -formal easyaxil.v
opt_skidbuffer: read -formal skidbuffer.v
read -formal faxil_register.v
read -formal faxil_slave.v
--pycode-begin--
cmd = "hierarchy -top easyaxil"
cmd += " -chparam OPT_SKIDBUFFER %d" % (1 if "opt_skidbuffer" in tags else 0)
cmd += " -chparam OPT_LOWPOWER %d" % (1 if "opt_lowpower" in tags else 0)
output(cmd);
--pycode-end--
prep -top easyaxil
[files]
../../rtl/easyaxil.v
opt_skidbuffer: ../../rtl/skidbuffer.v
faxil_slave.v
faxil_register.v
The six tasks prove the slave and cover its behaviour in four configurations: with or without skid buffers on its inputs (OPT_SKIDBUFFER), and with or without the low-power option. From bench/formal, run all six:
$ cd ~/formal/wb2axip/bench/formal
$ sby -f easyaxil.sby
output (DONE lines)
SBY 23:57:50 [easyaxil_prfreg] DONE (PASS, rc=0)
SBY 23:57:50 [easyaxil_cvrskd] DONE (PASS, rc=0)
SBY 23:57:50 [easyaxil_cvrreg] DONE (PASS, rc=0)
SBY 23:57:51 [easyaxil_prfskd] DONE (PASS, rc=0)
SBY 23:57:51 [easyaxil_prfreglp] DONE (PASS, rc=0)
SBY 23:57:51 [easyaxil_prfskdlp] DONE (PASS, rc=0)
All six pass within about two seconds. The tasks run in parallel, so the order of the lines can differ.
How deep must the induction step be?
The proof tasks use depth 3: k-induction with k = 3. To see why the depth matters, run the first proof task at depth 2:
$ sed "s/^prf: depth 3$/prf: depth 2/" easyaxil.sby > easyaxil_depth2.sby
$ sby -f easyaxil_depth2.sby prfreg
output (excerpt)
SBY 23:57:52 [easyaxil_depth2_prfreg] summary: engine_0 (smtbmc) returned pass for basecase
SBY 23:57:52 [easyaxil_depth2_prfreg] summary: engine_0 (smtbmc) returned FAIL for induction
SBY 23:57:52 [easyaxil_depth2_prfreg] DONE (UNKNOWN, rc=4)
| Depth | Base case | Induction step | Verdict |
|---|
| 1 | pass | FAIL | UNKNOWN |
| 2 | pass | FAIL | UNKNOWN |
| 3 | pass | pass | PASS |
At depths 1 and 2, the induction step starts from states that satisfy every assertion for one or two cycles but that reset cannot produce; this is the situation of the counter in Chapter 3, Run 4. At depth 3 no such state exists, and the proof holds for every cycle.
The proof completes at depth 3 because easyaxil adds helper assertions. They state how the checker's outstanding-transaction counts relate to the slave's own outputs:
rtl/easyaxil.v (lines 381–396)
always @(*)
if (OPT_SKIDBUFFER)
begin
assert(faxil_awr_outstanding== (S_AXI_BVALID ? 1:0)
+(S_AXI_AWREADY ? 0:1));
assert(faxil_wr_outstanding == (S_AXI_BVALID ? 1:0)
+(S_AXI_WREADY ? 0:1));
assert(faxil_rd_outstanding == (S_AXI_RVALID ? 1:0)
+(S_AXI_ARREADY ? 0:1));
end else begin
assert(faxil_wr_outstanding == (S_AXI_BVALID ? 1:0));
assert(faxil_awr_outstanding == faxil_wr_outstanding);
assert(faxil_rd_outstanding == (S_AXI_RVALID ? 1:0));
end
Each line ties a count in the checker to a signal in the design, for example: the number of outstanding reads equals 1 while S_AXI_RVALID is high, and 0 otherwise. These are the same kind of helper assertion that completes the counter's proof in Chapter 3, Run 5.
How does easyaxil reuse the skid buffer's properties?
With OPT_SKIDBUFFER set, easyaxil places a skid buffer from Chapter 5 on each of its AW, W and AR inputs. The tasks tagged opt_skidbuffer read skidbuffer.v as well, but this job file does not define SKIDBUFFER.
- In
skidbuffer.v, the macro ASSUME therefore means assert, as Chapter 5, “Why do the input rules switch between assume and assert?”explains. - The skid buffer's input rules, which were assumptions when it was proved alone, become assertions about how easyaxil drives each skid buffer.
- The tasks
prfskd and prfskdlp therefore prove easyaxil and also check that it uses its skid buffers correctly.