System verilog assertion writing multiple statments in sequence

Hi,

I am new to assertions,

I have a snippet of code written below in property,(in property i am nt finding any issue)

I want to change it into sequence.

sequence Rx_reset_timer(int dll_duration);

if(dll_duration == 0)
($fell(RXSTRBP_DLLRESET_B) ##11 $rose(PCS_DLLRESET_B))
else if(dll_duration == 1)
($fell( RXSTRBP_DLLRESET_B) ##12 $rose(PCS_DLLRESET_B))
else if(dll_duration == 2)
($fell( RXSTRBP_DLLRESET_B) ##16 $rose(PCS_DLLRESET_B))
else if(dll_duration == 3)
($fell( RXSTRBP_DLLRESET_B) ##25 $rose(PCS_DLLRESET_B))
else 1’b0;

endsequence : Rx_reset_timer

if and else if coding style is allowed or not?
i am finding a comilation error… at this line if(dll_duration == 0)

-Regards,
-RAJA.

What you defined above is not a sequence but a property.

sequence: A linear sequence is a finite list of SystemVerilog Boolean expressions in a linear order of increasing time. The linear sequence is said to match along a finite interval of consecutive clock ticks provided the first Boolean expression evaluates to true at the first clock tick, the second Boolean expression evaluates to true at the second clock tick, and so forth, up to and including the last Boolean expression evaluating to true at the last clock tick. A single Boolean expression is an example of a simple linear sequence, and it matches at a single clock tick provided the Boolean expression evaluates to true at that clock tick. More complex sequential behaviors are described by SystemVerilog sequences. A sequence always evaluates to true or false at its end point; thus if a sequence has a match, that match is true. A sequence is multi-threaded if it includes any of the following operators: and, intersect, or, range delay, consecutive range repetition, non-consecutive repetition (i.e., [=] operator. A sequence that is interpreted as a property is never vacuous.

What are your goals? Below are examples of usage, code simulates.

module test_if_st;
	bit clk, a, b, c, d, cond1, cond2;
    ap_test: assert property(@(posedge clk)
    	if(a)  b ##1 c 
    	else if(b) c ##2 d);
    
    ap_1: assert property(@(posedge clk) 
    		$rose(cond1) |-> if(a)  b ##1 c ); 
    // don't forget the $rose or $fell  in the antecedents
    // they are needed in most cases
    ap_2: assert property(@(posedge clk) 
    		cond2 |-> if(b) c ##2 d); 
    		
    ap_3: assert property(@(posedge clk) 
    		cond1 |-> if(a)  b ##1 c 
    	              else if(b) c ##2 d); 
    		
    initial forever #5 clk = ! clk; 
    initial begin 
    	repeat(50) begin 
    	  @(posedge clk); 
    	  if (!randomize(a, b, c,d)) $error(); 
    	end 
    end 
 endmodule

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

In reply to ben@SystemVerilog.us:

Hi Ben,

I am new to SVA. Can you explain how you tell the original code is a property, not a sequence.

Thanks.
Fiona

In reply to Fiona Feng:

The syntax you used specified a sequence with the sequence … endsequence
The property syntax is property … endproperty
A property uses sequences and properties.
A sequence can be used as a property wherever a property is used.

Study 1800 or a good book on SVA,
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


  1. https://verificationacademy.com/forums/systemverilog/vf-horizonspaper-sva-alternative-complex-assertions
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    October 2013 | Volume 9, Issue 3 | Verification Academy
  5. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

In reply to Fiona Feng:

Because your expressions contain property operators. Implication (if/else, |->} can only be used in a property. Sequence operators (##N) can be used in a property, but not the other way around.

In reply to dave_59:

Hi Dave,

Thanks. I got it.