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 NxM AXI-lite interconnect that can connect any N AXI-lite masters to any M AXI-lite slaves, with up to min(N,M) active connections at any given time. I used both my AXI-lite slave and master property sets to prove that this interconnect 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?

So, just for fun and to give these properties some exercise, I’ve been wandering Xilinx’s Forums, just looking for an example AXI-lite core that can be formally verified.

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:

always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
	// reset the circuit
else if (S_AXI_AWVALID && S_AXI_AWREADY && something_else)
	// design is already buggy

Here’s the same bug (again) in their (full) AXI example slave core, this one taken from Vivado 2018.3:

	always @( posedge S_AXI_ACLK )
	begin
	  if ( S_AXI_ARESETN == 1'b0 )
	    begin
		// Some reset code
	    end
	  else
	    begin
	      if (~axi_awready && S_AXI_AWVALID && ~axi_awv_awr_flag)
	        begin
	          // Address latching code
	        end
	      else if (axi_wready && S_AXI_WVALID && something_else)
	// The design is now broken

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.

Perhaps the reason why this bug is so common is because it’s prevalent in Xilinx’s example code. For example, here it is again in the example AXI-lite slave generated from Vivado 2018.3:

	always @( posedge S_AXI_ACLK )
	begin
	  if ( S_AXI_ARESETN == 1'b0 )
		// Some reset code
	  else
	    begin
	      if (axi_awready && S_AXI_AWVALID && ~axi_bvalid &&
				axi_wready && S_AXI_WVALID)
		// Again, the design is now broken

Here’s the problem: the rest bus logic depends upon *VALID and *READY alone! Both the bus master and the interconnect will move on to the next state in the bus transaction any time both *VALID and *READY are true, irrespective of whether or not any other slave-imposed conditions are also valid. Hence, if you condition your response to the bus on anything other than *VALID and *READY, you code may easily miss transactions.

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 *VALID and *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 complete.

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,

always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
	// reset the circuit
else if (S_AXI_AWVALID && S_AXI_AWREADY && something_else)
	// design is already buggy

to

always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
	// reset the circuit
else if (S_AXI_AWVALID && S_AXI_AWREADY)
	// Design continues ...

with the added formal property,

assert property (@(posedge S_AXI_ACLK)
	S_AXI_ARESETN && S_AXI_AWREADY
	|-> something_else);

You can also express this same property using an immediate assertion, as in:

always @(*)
if (S_AXI_ARESETN && S_AXI_AWREADY)
	assert(something_else);

Notice how I’m not placing S_AXI_AWVALID in this check. S_AXI_AWVALID 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 verification, you can then remove something_else from your if condition with confidence, knowing that 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:

always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
	// Reset code
else if (S_AXI_AWVALID && S_AXI_AWREADY)
	// Accept a transaction
else if (S_AXI_BVALID && S_AXI_BREADY)
	// Code is now buggy

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,

assert property (@(posedge S_AXI_ACLK)
	S_AXI_ARESETN && S_AXI_AWREADY
	|-> !S_AXI_BVALID);

Alternatively, you could write your code to handle both conditions:

always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
	// Reset condition
else case({S_AXI_AWREADY && S_AXI_AWVALID,
		S_AXI_BVALID && S_AXI_BREADY })
2'b00: // Logic when nothing happens
2'b01: // Logic when a return is accepted
2'b10: // Logic when a new request is made
2'b11: // Logic for when both a new request is made
	// and the last one is accepted
endcase

Conclusion

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.