05-16-2019 05:13 AM
I've recently been working on building formal verification properties for AXI transactions. When testing them on your demonstration AXI4 full slave core, as created by Vivado 2018.3, I found the following bugs:
Based upon my own experience, these are the sorts of bugs that might cause an AXI interface to lock up hard.
Let me know if there's anything more I can do.
P.S. For those needing an example of a formally verified AXI slave core, this one passes all of my checks.
06-11-2019 01:34 PM
Thanks for letting us know about these issues with the demo core. I have filed a CR to get these resolved in a future release of Vivado.
Please confirm the following.
The code on Github at this location: https://github.com/ZipCPU/wb2axip/blob/master/bench/formal/xlnxfull_2018_3.v
is the same code that the "Create and Package New IP" wizard generates. You haven't made any changes to it.
06-11-2019 01:50 PM
Thank you for looking into this!
Superficial changes have been made, mostly to the white-space, and then formal properties have been added to the end. Please feel free to compare the two below.
Please see the original and modified attached.
Thank you so much!