I am writing an assertion for the following scenario, however i noticed it is not working as intended. can somebody tell me what is wrong here? the assertion doesnt fail when awvalid deasserts one clock cycle before. Also i would like to see the assertion being written with until and throughout.
From AXI spec,
when AWVALID is asserted, then it remains asserted until AWREADY is high.
In reply to rag123:
[spec]When asserted, AWVALID must remain asserted until the rising clock edge after the slave asserts AWREADY
… the slave can assert AWREADY before AWVALID or WVALID, or both, are asserted
[Ben] Do we need the $rose(AWVALID) ?
It has been many years since I looked at the AMBA AXI stuff, thus I cannot go into specifics.
Here are comments and a suggestion that I hope will be helpful.
Your assertion does not a precondition (an antecedent) to start the needed tests.
In 2004 I addressed the AMBA as an example in my PSL book, and I wrote many assertions for that interface. Whether I would write them in the same manner today is debatable. I also DO NOT recommend the use of PSL, as SVA is IMHO far better and more mature.
I am giving you a copy of that chapter and the code. SVA has a lot of similarities to PSL and you should be able to get some inspirations into possible assertions.