Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Updated AXI-lite RAM to pass a formal verification check #11

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Conversation

ZipCPU
Copy link

@ZipCPU ZipCPU commented Nov 6, 2020

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

@Bald-Badger
Copy link

Bald-Badger commented Apr 3, 2022

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants