Assertion/property and default values

SystemVerilog
1

I am wondering if there is a simple way to test this kind of situation:

if <sequence> then
  OUTPUT==1 
else
  OUTPUT==0

So the point is that I want to restrict the OUTPUT signal behaviour only to sequence and otherwise it has to remain in a known state.

My current plan is to try something like this:


sequence seq_0;
  <sequence>
endsequence

p_0 : assert property (
  <sequence> |-> OUTPUT == 1);

p_1 : assert property (
  not <sequence> |-> OUTPUT == 0);

But this seems like a waste of file size and effort of virtually repeating every assertion with negation.

So is there some kind of if/else or other short and quick way to achieve what I am trying to do?

p.s. many people would use just p_0 and then think that everything is ok. But this leaves open all the other scenarios which do not fill the sequence prequisite. So OUTPUT could be toggling on/off like crazy and the designer would have no idea this is happening.

2

In reply to Jarno:

There isn’t any not operator for sequences. Conceptually what you want is the following (not sure if proper syntax):

 <sequence> && out == 1 or out == 0 [*]

This creates a sequences that matches on the first match of the two subsequences joined by the or. Disclaimer: I’m not an SVA expert. Try it out and let us know if it worked.

3

In reply to Tudor Timi:

I understand what you mean by ORing the sequences, but I will probably need consequent experesson as well? The sequence itself is just the antacendent for the assertion to hold or fail.

4

In reply to Jarno:

That’s where the “I’m not an SVA expert” part comes in. I’m not sure how to put it in an antecedent/consequent form. What I did notice just now, though, is that there is an iff operator for properties. Maybe an idea would be to try:



property some_property;
  <sequence>
endproperty

assert (@(posedge clk out == 1 iff some_property);

What’s not really clear from the LRM (to me at least) is when the properties start evaluating. I mean, you need some_property to have already started evaluation by the time you get to the out being high.

5 
//I am wondering if there is a simple way to test this kind of situation:
if <sequence> then
OUTPUT==1 
else
OUTPUT==0
//or basically, what is desiredL 
p_1 : assert property (
not <sequence> |-> OUTPUT == 0); // ILLEGAL CONSTRUCT

This is a bit tricky, but it is possible to do using the implies or the**|->** operators and the sequence endpoint, i.e., the .triggered. The implies can be used if the antecedent is a property instead of a sequence
I explain the implies in my book, and I am making an image of that page in

1205×767 149 KB

Take particular attention to table Table 3.9.5.1 property_expr1 implies property_expr2.
Specifically in p1 implies p2, both p1 and p2 start at the same cycle, and if p1 is false, then the property is vacuous. but if p1 is true, then p2 must be true.
Below is an an example of the solution:
The simulation waveform is at http://systemverilog.us/nosequence.png
Code is at


module notsq; 
	bit clk, out1, a, b, ab_endpt; 
	sequence q_ab; 
		@(posedge clk) a ##1 b; 
    endsequence
    
    ap_notsq: assert property(@(posedge clk) 
    		    !out1 implies not(q_ab.triggered)); 
    ap_notsq2: assert property(@(posedge clk) 
    		     !out1 |-> not(q_ab.triggered)); 
    
    initial forever #10 clk=!clk;
    
    always @(posedge clk) begin : p2
        if (!randomize(a, b, out1)) $error();
    end : p2
endmodule

Also, from my book on the iff

3.9.6 iff
 Rule: [1] The iff property has the following form: property_expr1 iff property_expr2
At every clocking event, there is an evaluation attempt of the iff property that consists of the LHS property expression and the RHS . The RHS and LHS properties are started concurrently and may finish at different times. For an evaluation attempt to be successful, both sides must either evaluate to true or both sides must evaluate to false.
Equivalence: (p1 iff p2) // is equivalent to
((p1 implies p2) and (p2 implies p1)

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115