Page 7 
Creating Assertions
Step 3: Code SVA Assertions
Now that we have a list of rules, we will switch over to our left-brain to code the SVA statements. This is made much easier since we already have a description of the rule and simply need to find the best way to express the rule in the SVA language. At this point, engineers have a choice to make: they can either code in the SVA by hand or use a third-party tool such as Zazz to automate the task.
Coding directly in SVA, the assertions from step 2 are as follows (just the SVA sequences are shown):
- AWVALID & AWREADY |-> (AWBURST!=2'b11)
- AWVALID & AWREADY |-> (AWCACHE[3:1]!=3'b010) & (AWCACHE[3:1]!=3'b100) & (AWCACHE[3:1]!=3'b110)
- AWVALID & ~AWREADY |=> AWVALID;
- AWVALID & ~AWREADY |=>$stable({AWADDR,AWID,AWLEN,AWSIZE,AWCACHE,AWSIZE})
The final assertion (not shown above) is more complicated and would probably take someone experienced in SVA to code it. However, all of these assertions are trivial to code using Zazz:
AWBURST and AWCACHE checking (combined)
AWVALID high until AWREADY and stable controls (combined)
