Some time ago, I posted a set of formal properties which could be used to verify any AXI-lite interface, slave or master. I then applied these properties to the AXI-lite slave core generated by Xilinx’s Vivado and found multiple errors within their core.
This wasn’t enough to convince me, however, to that these properties could be used broadly across many projects and designs. So I built my own AXI-lite slave core using these properties. Using SymbiYosys together with a poor man’s cover sequence, I could demonstrate that my core not only had less latency than Xilinx’s (once the bugs were fixed), but I could also demonstrate that my own AXI-lite core had twice the data throughput.
So it works on two slave cores. What about more complicated designs?
On a whim, I recently built an
that can connect any
N AXI-lite masters to any
M AXI-lite slaves, with up
min(N,M) active connections at any given time. I used both my
and master property
to prove that this
would obey the rules of the road for the bus. (It can also maintain the high
throughput rate of one transaction request or response per clock when using my
own AXI-lite slave core,
but that’s another discussion for another day.)
I then knew that my formal property set would work on not only basic AXI-lite slaves with only one or two transactions ever outstanding, but also on any number of arbitrary AXI-lite slaves driven by any number of arbitrary AXI-lite masters. The only rule for success was that the slaves needed to follow these formal properties.
But this was all my own code. Would these properties apply equally well to the designs of others?
Of course, this is a biased sample set, since no one submits their code to an on-line forum unless they can’t get it to work. Sometimes this means the code is written by a hobbyist who doesn’t care about whether or not his code gets released. At other times, its submitted by a (not always so) junior engineer who is so frustrated by trying to get a design to work that he’s ready to do anything just to get some help.
Personally, I think the problem is compounded by the prevalence of the ARM+FPGA chips as well as the other AXI based architectures which force you to use such a complicated bus interface to your design. In many of the examples I’ve found, the poster is frustrated because he feels like he is connecting his (working) code to a black box that he doesn’t necessarily or completely understand, and worse to one that he can’t examine. What then would you conclude when it doesn’t work?
So I thought I might share today the most common bug I’ve come across while examining the AXI-lite designs of others.
The most common bug
Let me get straight to the point: here’s the bug in Verilog form, as I found it in Xilinx’s AXI-lite example core:
Here’s the same bug (again) in their (full) AXI example slave core, this one taken from Vivado 2018.3:
I won’t continue either of these examples, because the code is already buggy at this point.
While the examples above are shown with respect to the write address and data channels, it can be found on any channel. This includes not only the read address channel, but also the write acknowledgment and read return channels. Specifically, this bug can often be found in any design using a basic handshaking protocol.
Here’s the problem: the rest bus logic depends upon
alone! Both the bus master and the interconnect will move on to the next
state in the bus transaction any time both
*READY are true,
irrespective of whether or not any other slave-imposed conditions are also
valid. Hence, if you condition your response to
on anything other than
*READY, you code may easily miss
Yes, this has bit me too.
Back when I was working on a Cyclone-V design, I discovered that missed or dropped transactions would lock up my design so hard that there would be nothing to do but cycle the power. (No, the reset button didn’t work.) While I can’t say the same would happen in a Xilinx design, I can safely say that the consequences of these mistakes are not benign.
Avoiding the bug
The reason why this bug is common is that a designer will look at the
*READY signals and say to himself, but I only want to act on
these signals if I’m not already busy, or only if some other operation is
Adding conditions to the transaction test, such as what we’ve seen in the examples above, is not the way to solve this problem.
What you want to do instead is to make certain that any time you are not ready
for the next transaction, you are then holding the
*READY line low.
Using formal methods,
this is as easy as adding another property to your proof, or rather one
property for every condition you want to accept on. For example, if we
were looking at the write address channel, and we wanted to condition on
something_else, you’d then want to change your code from,
with the added formal property,
You can also express this same property using an immediate assertion, as in:
Notice how I’m not placing
S_AXI_AWVALID in this check.
is one of the incoming signals to your design–one you have no control over.
It makes more sense, therefore, to check against
S_AXI_AWREADY alone since
this is the one signal in this group that you do have control over.
If this property passes formal
can then remove
something_else from your
if condition with confidence,
something_else will always be true anytime
*READY is true, and
so it no longer needs to be tested by your logic. This will also simplify
your design, leaving more logic resources available for other tasks.
The Second Form
You may also see this same bug in another form. Consider this following snippet of code, also generated automatically by Vivado:
In this case the question you need to ask yourself is, what will
your design do when
S_AXI_AWVALID && S_AXI_AWREADY
are both true at the same time
S_AXI_BVALID && S_AXI_BREADY are true?
There are two options to fix this form of the problem. First, you could
use formal methods
to prove that
S_AXI_BVALID would never be true when
S_AXI_AWREADY was true,
Alternatively, you could write your code to handle both conditions:
This bug is not specific to AXI peripherals by any means. You might also find this bug within Wishbone slave peripherals. Indeed, the basic handshake is a very common design component and it’s important to learn how to do it right.
No, I’m not done discussing the AXI bus just yet. I’d like to come back and discuss AXI some more, should the Lord permit. For example, I’ve just recently managed to formally verify both Xilinx’s AXI (full, not lite) example core as well as my own brand-new AXI (full) slave core, and I think it might be valuable to share this solution with others and to show you how to do it. Further, the formal verification solution I’ve presented for Verilog designs can also be applied to VHDL designs using the Symbiotic EDA Suite, and I’d like to show how to verify a VHDL design using the same tools as well. Indeed, it’s really not all that much harder, but there are a few interesting twists necessary to make it happen.
If these are topics you are interested in, please feel free to contribute to the ZipCPU blog on Patreon.
There hath no temptation taken you but such as is common to man: but God is faithful, who will not suffer you to be tempted above that ye are able; but will with the temptation also make a way to escape, that ye may be able to bear it. (1 Cor 10:13)