Hi All,
I’m new to SVA, and I met a simple question.
There’re 2 sigs: req and gnt. when req is true, gnt should respond within [1:3] clock.
I’ve wrote an assertion looks like this:
req |-> ##[1:3] gnt;
but,this assertion cann’t guarantee req and gnt will be a pair. For example,
in this case,the assertion will be triggerd in cycle 1,and success in cycle 4,but req in cycle 3 will also success in cycle 4,so the assertion success. But my intent is to check req in cycle 1 while gnt in cycle 4, and req in cycle 3 while gnt in cycle 7. In other words, the gnt should only be paired with req only once,req in cycle 3 should consider gnt in cycle 7,not gnt in cycle 4,so the assertion result should be failure. How should I write the assertion?
My English is not very good, i don’t know if I explain it clearly.
Thank you
What you’re asking is that each req should have its own corresponding ack.
We all have experienced the following scenario in a bakery or at the paint department in a hardware store. At the store you have one servicing employee and customers come in at different times, often forming a queue. Some customers take a very short time (e.g., they want one bagel, or the item they want is not available – a fail) or they take forever (e.g., wanting many items). So how doe the store handles this? Simple, they have a roll of tickets with incrementing numbers. They also have a board that displays the ticket currently being serviced. A new customer takes a ticket and waits for the store employee who after a service (pass or fail) increments the number on the board and takes on the next customer.
OK, our SVA model will do just that. I have 2 variables: ticket and servicing. In the SVA property, when req==1, the property saves the ticket number, and then increments the ticket for the next attempt of req. The assertion checks for a ack with a servicing number being the same as the ticket that was handed for that attempt. When the assertion terminates (success or failure), the servicing number is incremented.