Assertion to check for the toggle (0->1) of a signal

Hi all,

I am trying to write a assertion for the below check.

I have a test in which a signal goes high at any random point of time.
I have to check this using assertions whether it is going high at any time during simulation or not and if not then print an error.
I wrote the below one.

/////////////////////////////////////////////////////////
define true 1 property signal_check; @(posedge clk) disable iff (rst) true |-> ##[0:$] $rose(sig1); endproperty

assert_check: assert property (signal_check)
$display(“Concurrent assertion assert_check passed”);
else
$error(“Concurrent assertion assert_check failed”);
///////////////////////////////////////////////////////

When the signal (sig1) goes ‘0’ to ‘1’ then it works fine, but if the signal does not goes high (0->1) then the error message is not getting printed.
Could you please suggest any idea to get it resolved.

thanks & regards,
sanjoy

In reply to sanjay864u:
You need the strong ( sequence_expr ). I would then code this simply as:


assert_check: assert property (@(posedge clk) s_eventually $rose(sig1));

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

  • 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 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,

Thank you for your suggestion.
I tried the same you suggested.
But I am getting the below error.
“Operator ‘eventually’ not supported.”
could you please suggest some other way?

thanks & regards,
sanjoy

In reply to sanjay864u:

QuestaSim DOES support the s_eventually; you must have an older version.
Talk to your support group. In any case, you can do this:

assert_check: assert property (
     @(posedge clk) strong(##[1:$] $rose(sig1)) );

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

  • 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 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 used the below code you had suggested to check the toggle of a signal.

assert_check: assert property (@(posedge clk) s_eventually $rose(sig1));

But I an facing an issue with this.

Suppose, 0 to n clock cycles are there in my simulation and the $rose(sig1) is coming after x clock cycles.

Then this assertion is showing errors for the (n-x) clock cycles, because after x clock cycles also it is expecting $rose(sig1) to come, but ideally it should check only once of $rose(sig1) throughout the signal.

Please suggest.

thanks & regards,
sanjoy

In reply to sanjay864u:
I am not sure I totally understand your question, but if you just want one occurrence of the assertion use the initial statement.


import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
	bit clk, a;
	logic sig1;  
	default clocking @(posedge clk); endclocking
	initial forever #10 clk=!clk;   
	
	initial assert_check: assert property (
     @(posedge clk) strong(##[1:$] $rose(sig1)) );

 initial begin 
 	 repeat(30) @(posedge clk) ; 
 	 sig1 =0;
     repeat(200) begin 
       @(posedge clk);   
       #2 if (!randomize(a, sig1)  with 
           { a dist {1'b1:=1, 1'b0:=3};
             sig1 dist {1'b1:=1, 1'b0:=20};

           }) `uvm_error("MYERR", "This is a randomize error")
       end 
       $finish; 
    end 
endmodule  

simulation resuts:

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

  • 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 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,

What about if I want to see that signal sig2 should change only once during simulation after sig1 asserted and error should fire if changed more than once.

@(posedge clk) strong(##[1:$] $rose(sig1)) );

This assertion only check once and it will be finished.

In reply to pvpatel:

In reply to ben@SystemVerilog.us:
What about if I want to see that signal sig2 should change only once during simulation after sig1 asserted and error should fire if changed more than once.
@(posedge clk) strong(##[1:$] $rose(sig1)) );
This assertion only check once and it will be finished.

Your above sequence (used as a property) does not meet your requirements as it makes no mention of sig2. Also, with what you wrote, if sig1 occurs after 1 million cycles, your assertion creates 1 million separate threads. The simulator may do some optimization.
Thus, for a single firing, put the assertion in an initial block.
assertions typically have an antecedent and a consequence. Something like:


  ap_s1s2: assert property (@(posedge clk) $rose(sig1) |-> s_eventually sig2 );
 ap_s1s2b: assert property (@(posedge clk) $rose(sig1) |->  strong(##[*0:$] sig2)); 
 ap_s1s2c: assert property (@(posedge clk) $rose(sig1) |->  strong(sig2[->1])); 

FOr and error should fire if changed more than once, consider the use of the cover
bit my_error; // If true, fire a message
cp_s1s2b: cover property (@(posedge clk) $rose(sig1) |->  (sig2[->2]) my_error <= 1'b1; 

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

  • 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 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:

Thank you Ben, I understand your point. But my requirement is,

Signal B should be only changed 1 time during Signal A’s assertion and de-assertion. Signal A may be asserted- de-asserted many time during simulation.

Regards,
Pratik

In reply to pvpatel:

As a general rule, it is best to use multiple small assertions than one complex one. It looks like in this case you have:

  • one assertion that is inside an initial statement and is initiated after a precondition.

initial begin
@(go) assert_check: assert property (…) ;
end

  • other assertions that are attempted at every clock edge

In reply to ben@SystemVerilog.us:

hai, ben.
here you are calling the assertion in the initial block right? initial block will execute only once at zero simulation time correct? then does the assertion checks only for first time?

please correct me if i am wrong in any way

In reply to vickyvinay:

An assertion is initiated at every leading clocking event.
An initial statement has ONE leading clocking event, thus it is initiated once.
A concurrent assertion instantiated directly in a unit has an implicit “always”.
A concurrent assertion instantiated inside an initial or always does not have this implicit always.
Ben systemverilog.us