Synthesizing an AXI-Lite Slave Controller

[Dnay]

Hi everyone,

i´m working on the Synthesizing an AXI-Lite Slave Controller and i have some problem with the specification of the Acknowledgment for the read and write channel and i can´t genrate the verilog code with my sythesizing tool. does someone have any experience on the topic??? please let me know if you have time for a small exchange

[artvvb]

Hi Dnay,

If you post source code, we could potentially take a look and see why it might not be synthesizing. Are you simulating your design?

Thanks,

Arthur

[Dnay]

I've had to write LTL specifications that I first have to convert into verilog with BoSy and then synthetise. But I've got quite a few errors in my specifications and the debugging tool doesn't really help me detect them.

 

do you have experience with LTL Specification to design and modelise such a logic??

Edited April 30 by Dnay

[artvvb]

I'm not familiar with LTL specifications. That said, there's some content on the ZipCPU website about formal verification of AXI interfaces that may help?

[Dnay]

exactly.

I've read the different articles but I still have some grey areas, which is why I'd like to know if anyone has any ideas to shed some light on the subject.

 

[D@n]

I write and maintain the ZipCPU blog.

What questions do you have?

Dan

[Dnay]

Dear Pr Dan Gisselquist,
thank you for your reply and it is an honour for me to be able to talk to you in person. 

In fact I'm working on Synthesizing an AXI-Lite Slave Controller consisting of applying reactive systems to compute such a logic from formal specifications automatically. 

To do this, I'm using your documents to understand how it works and to write the formal specifications and with BoSy generate a verilog code that I'll then implement on a real FPGA with Vivado.

However, I'm having a few problems with the formal specifications I've written because I'm not getting an optimum result even though everything seems correct, which is why I need help to clarify things and help me perfect them.

I have attached to my message a txt file containing all the written specifications in case you have a little time to look at them. 

i thank you in advance for your reply and i would welcome any valuable advice that could help me to make rapid progress. 

Sincerely,

Dnay

 

LTL_AXI_Lite+.txt

Edited May 2 by Dnay

[D@n]

Okay, so ... I've looked at your specifications and ... understand nothing of LTL or the specification language you are using.

Perhaps some pictures might help you understand the concepts, and you can then translate them to LTL?

https://github.com/ZipCPU/wb2axip/blob/master/doc/busprops.pdf

Dan

[Dnay]

Thank you for your reply and your time Professor.  but I'm a bit confused 

you don't understand my LTL Specifications because they're badly formulated or because you simply don't use them. because I've just took the various characteristics of the bus presented in your article and I've translated them into LTL:

However, the link you sent me describes a general bus function but not that of the specific case of Axi lite. 

 

Regards,

Dnay

Edited May 2 by Dnay

[D@n]

I don't understand your LTL because ... I've never used LTL.

Quote

However, the link you sent me describes a general bus function but not that of the specific case of Axi lite.

 

Did you look through the whole slide deck?  There are only 13 slides.  The first 7 are generic, the last 5 or so show how those generic slides apply to AXI-Lite.  Frankly, if you understand the generic bus principles, then translating them to AXI Lite should be pretty easy.

Dan

[Dnay]

Thank you for your reply.

 

apart from the LTL specifications in my document, do you think I've described AXI Lite's operation well enough (I mean the litterally description ), or do I really need to include the other properties in the link you've just sent me to be more consistent?

[D@n]

Looking over the comments in the file you've shared above, they look mostly good.  A couple things I'd note:

• The interconnect may also give you AxPROT pins to ignore.  These pins have the same stability requirements as the AxADDR pins.  You could choose to try to do "smart" things with these pins if you wanted to--like return bus errors if a CPU's instruction prefetch ever tries to access your slave, although I tend to ignore them.
• AWADDR is an input to the slave, not an output
• BRESP and RRESP are also a required outputs.  I typically just tie these to zero.
• WSTRB is a required input.  Be prepared for writes where WSTRB==0--writes where you shouldn't do anything.  Two approaches to this are 1) Only adjust the slaves registers when WSTRB==4'b1111, or 2) adjust sub-words as appropriate when WSTRB != 4'h0.

Dan