Need a help on below assertion writing

SystemVerilog
, ,
1

I need help in writing the below assertion.

My requirement is :

After Sig1 asserted, Sig2 should be stable until sig3 asserted.

Thank you…

2

In reply to Bharath@Intel:

 
//Use the 
  property_expr s_until property_expr  
| property_expr until_with property_expr

$rose(Sig1) |=> $stable(Sig2) s_until sig3[->1];

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  • SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
  • 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 978-1539769712
  • 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
  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
    4). FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
3 
	// Try this one also
$rose(s1) |=> first_match($stable(s2) ##[0:$] $rose(s3),$display($stime(),"PASS"));

In reply to Bharath@Intel:

4

In reply to Raghunandan Reddy:
The above property is is error because the requirement is for Sig2 to be be stable at all cycles until sig3 asserted.
// INCORRECT ($rose(s1) |=>
// first_match(stable(s2) ##[0:] $rose(s3),$display($stime(),“PASS”));)

You would need


ap_s123: assert property(@ (posedge clk) $rose(s1) |=> 
                         first_match($stable(s2)[*0:$] ##1 $rose(s3)));

BTW,
An until property of the non-overlapping form (i.e., until, s_until) evaluates to true if property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until at least one tick before a clock tick where property_expr2 (called the terminating property) evaluates to true.

An until property of one of the overlapping forms (i.e., until_with, s_until_with) evaluates to true if property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until, and including a clock tick at which property_expr2 evaluates to true.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
5

Thank you guys for the reply:

I am going to have three solutions and update which one doing good for my requirement:

$rose(Sig1) |=> $stable(Sig2) s_until sig3[->1];
$rose(s1) |=> first_match(stable(s2) ##[0:] $rose(s3),$display($stime(),“PASS”));
ap_s123: assert property(@ (posedge clk) $rose(s1) |=>
first_match(stable(s2)[*0:] ##1 $rose(s3)));

6

In reply to Raghunandan Reddy:

In above code some typo error is there where i forget to mention the continuous repeat operator(*) which ben had rectified in his reply.

 // I can conclude my code should be as below	
property check_1;
		$rose(s1) |=> first_match($stable(s2) ##[*0:$] ##1 $rose(s3),$display($stime(),"PASS"));
endproperty

	CHECK_1: assert property (@(posedge clk) check_1) $display("Assertion pass 1");
7

In reply to ben@SystemVerilog.us:

Thank you ben for your quick feedback