We have detected your current browser version is not the latest one. Xilinx.com uses the latest web technologies to bring you the best online experience possible. Please upgrade to a Xilinx.com supported browser:Chrome, Firefox, Internet Explorer 11, Safari. Thank you!

Showing results for 
Search instead for 
Did you mean: 
Scholar dgisselq
Registered: ‎05-21-2015

AXI demonstration slave core has multiple bugs within it

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:

  • The core drops transaction responses
  • It doesn't guarantee a proper transaction ID in the return response
  • It can be confused and lock up when WLAST is true and WVALID isn't,
  • For some strange reason, the core was built to disable writes during reads.  That one I haven't been able to figure out.

You can find the full writeup here: http://zipcpu.com/formal/2019/05/13/axifull.html

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.

2 Replies
Xilinx Employee
Xilinx Employee
Registered: ‎10-04-2016

Re: AXI demonstration slave core has multiple bugs within it

Hi @dgisselq,

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.



Don’t forget to reply, kudo, and accept as solution.
Scholar dgisselq
Registered: ‎05-21-2015

Re: AXI demonstration slave core has multiple bugs within it


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!


0 Kudos