Formal Verification of AXI-Lite Crossbar about axi HOT 16 CLOSED

It should be working (in terms of AXI compliance). The main problem was that it never was a crossbar but only one master could be active at a time. We are working towards a reimplementation.

from axi.

There were actually several issues associated with non-compliance. This is only one of them.

from axi.

What was the exact path you could observe?

from axi.

There were several. For example rvalid coming from a slave returning combinatorially to the master.

from axi.

If you want you can cut those paths using an src/axi_cut.sv. I do not know what the rationale behind this sentence is though.

from axi.

I do not know what the rationale behind this sentence is though.

Are you asking about the rationale behind one of my sentences, or the sentence in the specification?

from axi.

The one in the spec. That would always induce a mandatory cycle delay in the crossbar, rather undesirable as a default imho.

from axi.

It's actually worse than that. It introduces not one but two mandatory cycle delays into the crossbar--one on the address channel and another on the return channel.

My best guess of the rational (since I didn't write the spec) is to keep any AXI logic off of the critical path in any time constrained system--helping you run at higher logic speeds. Hence, if all the AXI logic outputs are registered, vs combinatorial, ... you get the idea. The sad reality though is that it adds an additional level of complexity to any AXI design.

from axi.

Thanks for your inputs regarding formal verification of our modules, we highly appreciate them! We have just merged a new AXI4-Lite crossbar (#41), which actually is a fully-connected crossbar. Would you be interested in providing formal verification inputs on it?

from axi.

Have you made the deliberate decision to allow outputs, such as the return values to the requesting masters, depend combinatorially upon the inputs from the slaves? I'm particularly discussing the R* channel, where the master can receive the data return on the same clock as the slave returns it. I haven't checked any of the other channels for the same bug.

Other than that issue, I'm not seeing anything more.

Dan

from axi.

Have you made the deliberate decision to allow outputs, such as the return values to the requesting masters, depend combinatorially upon the inputs from the slaves?

Yes, one can opt-in to breaking all combinatorial paths by inserting axi_lite_cuts (as Florian pointed out).

Other than that issue, I'm not seeing anything more.

Great to hear! Is your formal verification setup for AXI-Lite available open-source?

from axi.

The AXI-lite properties are all open source, yes. However, I did build a wrapper around this module to instantiate those properties, and an SBY file that would bring in all of the various inputs. I have not shared that wrapper with anyone. We can discuss sharing that if you see yourself repeating this work.

The SystemVerilog extensions used by this AXI-lite crossbar are not supported by the open source version of SymbiYosys, but rather the commercial Symbiotic EDA Suite.

Dan

from axi.

It would be great to have formal verification properties for the modules in this repository (as a complement to the already existing, stimuli-based testbenches). Do you know if the input files for the commercial Symbiotic EDA suite can be shared under open-source licenses?

from axi.

Sure, that's not a problem. The AXI-lite master properties are already open source and can be found here, next to their associated AXI-lite slave properties.

As for the other files, what would you recommend as the best place to put them? They would be unique to this particular design.

from axi.

How about creating a new directory formal in test? Would we add your wb2axip repository as a submodule (*) there to have access to the other properties, and add the files that are unique for this repository directly? Would you be willing to contribute them?

@zarubaf What do you think?

(*) As far as I can judge, the Apache 2.0 license of your repo should be compatible with the Solderpad 0.51 license (which is based on Apache 2.0) of our repo, but I am not a lawyer.

from axi.

@ZipCPU What do you think? Would you be willing to contribute your formal verification properties for the modules in this repository in a PR?

from axi.