Creating Assertions

Step 2: Create Rules by Paraphrasing Intent

Many engineers are overwhelmed by the prospect of adding assertions, mainly because it takes time to think of a rule and then code the associated assertion. Constantly switching between the right-brain activity (exploring associations) and left-brain activity (synthesizing the associated SVA construct) makes the process seem very disjointed.

A better approach is to split the process into two separate steps. First brainstorm as many rules as possible, and simply write each as a phrase much like an RTL comment. Later, take all these phrases and code them as SVAs. By doing this, you will find that you can create a richer set of assertions while streamlining the procedural aspects of coding the assertions.

For our AXI example, we might brainstorm the following rules for the write address bus (these are just a few):

• AWBURST may never be 2'b11 (reserved)
• AWCACHE must never be 4'b010x, 4'b100x, or 4'b110x
• When AWVALID goes high, it must remain high until AWREADY is asserted
• When AWVALID goes high, AWADDR/ID/LEN/SIZE/etc must remain stable until AWREADY
• When an address is accepted (AWVALID & AWREADY) we must see a corresponding response with the same ID (BVALID & BREADY) at some point later in time

Each of the channels shares some of these rules, so many can be reused when creating assertions for the other AXI signals. Many of these rules come directly from the AXI specification - all an engineer needs to do is read the specification and look for phrases that can be interpreted as rules.