verilog-axi
verilog-axi copied to clipboard
Updated AXI-lite RAM to pass a formal verification check
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
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