Blog: An Introduction to Assertion-Based Verification – Part 2

Welcome to the second part of our introduction to Assertion-Based Verification
—

In part one of our ‘look at assertions’, we introduced assertions and showed that both the PSL and SVA properties are similar and resemble design requirements.

 

We developed the basic terms and ideas of assertions and discussed sequences, properties, assertions and covers and how they form design properties. We also learned how a property is defined and how it follows the principles of temporal logic. Finally, we began to build some practical assertions to understand what we introduced and discussed.

 

In the second and final part of the assertion journey, we will develop the use of implication in assertions and its importance in assertions, as well as use in simulation. You may need to have a big pot of coffee and a packet of hob nobs at the ready, as we are going to get a little ‘Dr. Spock’ with implication and vacuous truths!

 

The Use of Implication

The final part of building sequences we will look at is ‘implication’.

 

Let’s remind ourselves of traditional logical implication of p implies (=>) q.

 

Here p and q are propositional variables that stand for any propositions in a given language. In a statement of the form “if p then q”, the first term, p , is called the antecedent and the second term, q , is called the consequent, while the statement as a whole is called either the conditional or the consequence.

 

Assuming that the conditional statement is true, then the truth of the antecedent is a sufficient condition for the truth of the consequent. While the truth of the consequent is a necessary condition for the truth of the antecedent.

 

Where the antecedent (p) is false the implication of the consequent (q) must be true, which gives rise to what is known as a ‘vacuous truth’ where the consequence is ‘true’ irrespective of the consequent.

 

Property languages support ‘temporal implication’ in its standard form:

 

Antecedent Implication_Symbol Consequent

 

 

A property with implication has three possible behaviours during verification:

 

• Vacuous pass (antecedent is false)
• Non-vacuous pass (antecedent and consequent are true) and
• Fail (antecedent is true, consequent is false)

A vacuous pass is crucial in efficient simulation of assertions with longer sequences, as if the trigger event specified as the antecedent does not happen then the remainder of the sequence is not evaluated and the assertion passes without alarm!

 

There are different types of implication known as ‘overlapping implication’ and ‘non- overlapping implication’.

 

The consequent of overlapping implication starts at the time point where the antecedent ends and is represented by the symbol ‘|->’

 

The consequent of non-overlapping implication starts one cycle after the end of the antecedent and is represented by the symbol ‘|=>’

 

Let’s see a real assertion in action:

 

Consider a typical design property ‘The Acknowledgement signal ‘ACK’ should be active for 1 to 3 clock cycles following the Request ‘REQ’ signal, provided that the signal ‘RESET’ is not active’

 

Let’s see what this would look like in PSL and SVA.

 

In PSL:

 

property req_ack is

 

always( ( {(REQ=‘1’)} |-> {(ACK=‘0’)[*1 to 3]; (ACK=‘1’)} )

 

async_abort RESET=‘1’ )@rising_edge(CLK);

 

assert (req_ack) report “No timely ACK after REQ!“;

 

In SVA:

 

property req_ack;

 

     @(posedge CLK) disable iff (RESET)

 

     (REQ==1) |-> (ACK==0)[*1:3] ##1 (ACK==1);

 

endproperty

 

assert property(req_ack) else $error(“No timely ACK after REQ!“);

 

Clocking (sampling) event                                   Asynchronous reset handling

 

Notice that we have used our clocking (sampling) event and reset handling mentioned earlier.

 

We can see this assertion (with implication) from a simulation screenshot:

 

Note that there are up to 4 concurrent evaluation threads which creates a workload for the simulator, so we should look into this further.

 

The assertion example we introduced above has one disadvantage. If REQ is high for more than one clock cycle then the property starts a new evaluation thread on each clocking event.

 

This behaviour may lead to redundant multiple violation messages when the assertion fails and unnecessary slowdown of the simulation.

 

To avoid this situation, edge detection functions can be used: ‘rose() / fell()’ in PSL / VHDL and ‘$rose() / $fell()’ in PSL / Verilog and SVA.

 

Those functions compare the previous and current sample to detect an edge.

 

If the edge detection is not convenient then a more selective condition should be selected for implication of the antecedent.

 

So with that in mind, let’s rewrite the property from our example above to make the assertion more efficient, using edge detection functions:

 

In PSL:

 

property req_ack is

 

     always( ( {rose(REQ)} |-> {(ACK=‘0’)[*1 to 3]; rose(ACK)} )

 

              async_abort RESET=‘1’ )@rising_edge(CLK);

 

assert (req_ack) report “No timely ACK after REQ!“;

 

In SVA:

 

property req_ack;

 

     @(posedge CLK) disable iff (RESET)

 

     $rose(REQ) |-> (ACK==0)[*1:3] ##1 $rose(ACK);

 

endproperty

 

assert property(req_ack) else $error(“No timely ACK after REQ!“);

 

Remember that the results depend upon the sampled values of arguments.

 

So we can look at the updated simulation screenshot:

 

This time we only have 2 concurrent evaluation threads – much better than using the clocked edge (no edge) detection.

 

Note that the second thread contains vacuous passes only (small workload for the simulator).

 

Before we move on, let’s just recap on the general assertion ‘tips’:

 

• Always select appropriate clocking / sampling
• Specify how to handle resets or similar signals if required
• If the tested property has a ‘trigger event’ specify it as antecedent of temporal implication (avoid unnecessary threads)
• For critical events in properties, use edge detection instead of level detection

 

Asserts Versus Covers

We have talked a lot about the assert, but what about covers?

 

We have seen that assert statements monitor your design to verify that some desired behaviour will always happen, or that certain undesired behaviours never happen.

 

Assertions will raise an alarm when the asserted property fails.

 

Cover statements monitor your design to check if certain critical behaviours were exercised.

 

Monitored behaviours can be ‘good’ (e.g. the successful completion of a transaction), or ‘bad’ (e.g. a transmission error and design reaction to it).

 

Covers print a message and increment a count when the behaviour was detected.

 

A mute assertion means that ‘everything is ok’ and a mute cover means ‘we have incomplete verification’.

 

The use of implication in coverage properties may trigger false results, therefore the use of plain sequences will be a better choice in the following example of a state machine with state register M1:

 

In PSL:

 

sequence std_seq(const max) is

 

     {(M1=init);(M1=idle)[*1 to max];(M1=act1)[*1 to max];

 

               (M1=act2);(M1=act3)[*1 to max];(M1=idle)};

 

property slow_path is std_seq(4)@falling_edge(CLK);

 

cover (slow_path) report “Slow execution path covered!“;

 

In SVA:

 

sequence std_seq(max);

 

     (M1==INIT)##1(M1==IDLE)[*1:max]##1(M1==ACT1)[*1:max]##1

 

               (M1==ACT2)##1(M1==ACT3)[*1:max]##1(M1==IDLE);

 

endsequence

 

property slow_path; @(negedge CLK) std_seq(4); endproperty

 

cover property(slow_path) $warning(“Slow execution path covered!“);

 

Here we are testing that the state register M1 starts from the ‘init’ state and enters the ‘idle’ state on the next clock cycle, remaining there for a certain amount of clock cycles before moving to the ‘act1’ state, where it will remain for a certain amount of cycles before moving to the state ‘act2’, and then in the next cycle ‘act3’ and remain there for a certain amount of cycles before returning to the ‘idle’ state.

 

Note that the use of parameters in this example promotes reuse.

 

We can see the functional coverage from the simulation screenshot:

 

# KERNEL: Warning: Cover ‘slow_path’ (Slow execution path covered!) COMPLETED at time: 110ns (11 clk), C:\PRO_Designs\PSL\VHDLembed\src\machine.vhd(51), scope: machine_tb.UUT, start-time: 20ns (2 clk)

 

We can see in the assertion simulation result that there are only two threads of property evaluation, which is good.

 

We can see new symbols – the red down-arrow at the top denotes a failed cover property evaluation.

 

The green ball at the top denotes successful cover property evaluation.

 

We see a failure at time 20, due to there being no transition from state ‘init’ to state ‘idle’.

 

At the same time as the failure occurs, a new evaluation starts that succeeds at time 110.

 

Let’s summarise with some ‘tips’ for covers:

 

• Properties checked by cover statements should avoid implication; while vacuous passes was desired behaviour in assertions, it would trigger false positives in functional coverage
• Simulators have options to enable or disable vacuous pass counting in assertions and covers but those features are tool specific and their use reduces code portability
• If you have a property with implication and have to use it in a cover, consider replacing the implication with a suitable fusion, concatenation or cycle delay

And for some final pearls of ABV wisdom:

 

• Learn rudimentary linear temporal logic (LTL) if you plan to work seriously with assertions
• Don’t jump into deep water – start with some simpler assertions
• Label all assertion-related declarations: you will be happy you did it when the debugging time comes!
• Implication is your friend in assertion properties – not always so in cover properties
• Do not exaggerate: write only properties that really require checking (critical ones)
• Use tool features where available as relying on pure language reporting is portable, but can flood you with way too much data

In Conclusion

For the sake of ‘simplicity’, we have focused on the basic features of properties and assertions. There is a lot more to learn about them, and you may recall I said at the beginning, that they need to be understood in order to see how they can be integrated effectively into a verification methodology.

 

That said however, even with the basic knowledge we have covered, you can still create surprisingly useful and powerful properties. As complexity increases in your design, then properties, assertions and coverage are unavoidable; You will encounter them at some point in the future, if not already. Don’t be afraid of assertions and coverage – remember that they resemble the design specification, so you are halfway there!

 

Whilst we said that assertions are very similar for both languages, you may not be in a position to have a mixed language simulator, so the great news for VHDL is that VHDL-2008 supports PSL, therefore a single language simulator isn’t an issue.