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?

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

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

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.

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??

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