verilog-axi icon indicating copy to clipboard operation
verilog-axi copied to clipboard

Updated AXI-lite RAM to pass a formal verification check

Open ZipCPU opened this issue 4 years ago • 1 comments

These few updates were required to get your AXI-lite design to pass a formal verification check.

At issue is the fact that BVALID (or RVALID for that matter) cannot be set prior to both AWVALID && AWREADY and WVALID && WREADY have passed. According to the AXI space,

The slave must wait for both ARVALID and ARREADY to be asserted before it asserts RVALID to indicate that valid data is available

and again,

The slave must wait for AWVALID, AWREADY, WVALID, and WREADY to be asserted before asserting BVALID.

These changes bring the design back into compliance.

You may also need to remove the PIPELINE_OUTPUT option, since this slave is only legal if PIPELINE_OUTPUT is set.

Dan

ZipCPU avatar Nov 06 '20 22:11 ZipCPU

OH maybe that's the problem that caused my Cyclone V SoC design got hung on an AXI read to this module...

I'll get back after I test these changes

Edit: the SoC design passed after the change. please consider audit and accept this Pull

Bald-Badger avatar Apr 03 '22 18:04 Bald-Badger