Reset Assertion

SystemVerilog
1

I wanted to write an assertion in which

  1. When Reset goes from 1 to 0, ElecIDle=1
    2.From there EleIdle should be 1 till Reset=0,It should not change in between,

Can anybody please help

2

In reply to naaj_ila:

I wanted to write an assertion in which

  1. When Reset goes from 1 to 0, ElecIDle=1
    2.From there EleIdle should be 1 till Reset=0,It should not change in between

On your 2nd requirement, you most likely mean
"2.From there EleIdle should be 1 till another fall(Reset),It should not change in between

 
 initial begin // Needed to create only ONE assertion 
   wait($fell(Reset)); 
   ap_reset2idle: assert property(@(posedge clk) 
           $fell(Reset) |-> ElecIDle[*1:$] ##1 $fell(Reset));  
 end

// Typical application of reset, from my 4th Edition SVA book
module m10_19; // /ch10/10.19/m10_19.sv m10_19.png
  bit clk, reset_n, system_ready;
  default clocking cb_clk @ (posedge clk); endclocking
  initial begin
    wait(system_ready);  // You need to assess the need for this. 
      a1: assume property(   // you can also use assert property 
      ##1 $rose(reset_n) |-> always reset_n);
     // The ##1 is needed to detect the $rose
  end

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

  • SystemVerilog Assertions 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
3

In reply to ben@SystemVerilog.us:

In reply to naaj_ila:
On your 2nd requirement, you most likely mean
"2.From there EleIdle should be 1 till another fall(Reset),It should not change in between

 
initial begin // Needed to create only ONE assertion 
wait($fell(Reset)); 
ap_reset2idle: assert property(@(posedge clk) 
$fell(Reset) |-> ElecIDle[*1:$] ##1 $fell(Reset));  
end
// Typical application of reset, from my 4th Edition SVA book
module m10_19; // /ch10/10.19/m10_19.sv m10_19.png
bit clk, reset_n, system_ready;
default clocking cb_clk @ (posedge clk); endclocking
initial begin
wait(system_ready);  // You need to assess the need for this. 
a1: assume property(   // you can also use assert property 
##1 $rose(reset_n) |-> always reset_n);
// The ##1 is needed to detect the $rose
end

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

  • SystemVerilog Assertions 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

Thanks a lot for the reply,
It worked for me with soem modifications,
wait($fell(Reset)); is giving compiel error
so modifed as @(negedge Reset).

Previously i coded the same way but i did not waited for 1st falling of Reset.
From 0ns Reset=0,when clock started, assertion started from that point(But Reset didnot fall)and started failing.
I dinot understood why assertion started ?

4

In reply to naaj_ila:

It worked for me with some modifications,
wait($fell(Reset)); is giving compile error
so modified as @(negedge Reset).

[1] The wait($fell(Reset)) should have worked and IS LEGAL.
From 1800:15.5 Named events
“Processes can wait for a named event to be triggered either via the @ operator or
by the use of the wait() construct to examine their triggered state.”
I used Questa and wait($fell(Reset)); worked OK. Talk to your simulator vendor if that did not work.

[2] So you modified it to:


   initial begin // Needed to create only ONE assertion 
     @(negedge Reset); 
     ap_reset2idle_neg: assert property(@(posedge clk) 
           $fell(Reset) |-> ElecIDle[*1:$] ##1 $fell(Reset));  
   end

Previously i coded the same way but i did not waited for 1st falling of Reset.
From 0ns Reset=0,when clock started, assertion started from that point(But Reset didnot fall)and started failing.
I dinot understood why assertion started ?

Your simulator incorrectly took Reset==0 at initial time to be falling.
Below is my simulation result, along with code
http://systemverilog.us/m10_19.png
Note that at time 0, the simulator did not fire the @(negedge Reset) or the wait($fell(Reset))
You can try my model, which is at
http://SystemVerilog.us/m10_19bb.sv

1353×614 113 KB

On a side note, why are you using an active ONE reset instead of an active ZERO reset. Usually, the active ZERO reset is used because that signal is generated off a capacitor that hold the signal low for a while during power-up.

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

  • SystemVerilog Assertions 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