Creating Assertions

Step 4: Debug Assertions (con't)

As an example, let's code the assertion "AWVALID must remain asserted until AWREADY and AWLEN must remain stable throughout this time." The designer might envision intent as shown in the sketch below:

Using Zazz to construct the assertion, it might look like the diagram below*. It says that when AWVALID is asserted, the assertion should wait until AWREADY is asserted, and then apply two constraints throughout this time: AWVALID must remain true and AWLEN must remain stable (the other control signals are omitted for simplicity).

Using the SVA Debug feature, Zazz generates some stimulus and allows the engineer to see how the assertion behaves, as shown in the image below:

We see that the assertion is failing on several scenarios. The problem is that the $stable on AWLEN should not apply on the first cycle but instead, only on subsequent cycles. It also shows that the assertion triggers multiple attempts on the same event (which may not be the desired behavior for some assertions).