Assertion and stable value from the beginning

SystemVerilog
1

Hello all,

I am trying to write a property/assertion for situation like this:

if ENABLE = 0 always from the init, then OUTPUT = 0

So in otherwords, I want to check the OUTPUT during the time ENABLE has not gone high for the first time. What’s the correct way? I already tried this (but obviously it’s not working…):

fifo_empty_a : assert property (@(posedge clk) disable iff (!rst_n)
  ##[0:$] ENABLE == 0
  |->
  ##0 OUTPUT == 0);

I am a SVA newbie, so pardon me for my ignorance ;)

2

In reply to Jarno:

Also just to clarify, I am now talking about formal checking and not “in-simulation”.

3

In reply to Jarno:

Can you please elaborate on the question?

4

In reply to Ashith:

So the problem is, how do I say “ENABLE == 0” from the very start of the simulation/formal check?

Currenty the example SVA that I posted above works for clock tick t0, t1, t2 … but the formal tools still consider also clock ticks t-1, t-2 etc.

If I try $stable(ENABLE), the $stable is valid only for ticks t-1, t0, t1 etc. But again the tool toggles ENABLE in t-2 and finds an error…

In other words, I am interested about the ENABLE only when it’s 0 for the first time (and 0 is the init value after the reset). If it later on toggles between 0 and 1, I don’t care anymore.

5

I am trying to write a property/assertion for situation like this:

if ENABLE = 0 always from the init, then OUTPUT = 0

So in other words, I want to check the OUTPUT during the time ENABLE has not gone high for the first time. What’s the correct way? I already tried this (but obviously it’s not working…):

fifo_empty_a : assert property (@(posedge clk) disable iff (!rst_n)
##[0:$] ENABLE == 0
|->
##0 OUTPUT == 0);

First, and most important comment: NEVER, NEVER, NEVER start an antecedent with the sequence
##[0:] a |-> ... // or ##[1:] or ##anything
Many issues if you do that:

  1. The property can never succeed because all sequences of the antecedent must succeed for the property to succeed.
##[0:$] a  // is same as 
 ##0 a or ##1a or ##2 a or .... ###n a
  1. It creates multiple unnecessary threads.
    Instead just use the variable directly, e.g.,
// ##[0:$] a |-> ... // <-- DO NOT DO THIS 
a |-> ... // DO THIS 
$rose(a) |-> ... // or THIS

For your problem, you could use something like the following:

module test_1time (
		input clk, started, enb, rst_n,
		output x_out); 
	 
     
	fifo_empty_a : assert property (@(posedge clk) disable iff (!rst_n)
                          !started ##0 (enb== 0, set_started(1))  |-> x_out==0); 
	
	// So in other words, I want to check the OUTPUT during the time ENABLE has not gone high 
	// for the first time. What's the correct way? I already tried this (but obviously it's not working...):
	// n other words, I am interested about the ENABLE only when it's 0 for the first time 
	// (and 0 is the init value after the reset). If it later on toggles between 0 and 1, I don't care anymore.
	
	am_1time: assume property(@(posedge clk) $rose(enb) |-> started==1); 
	am_started: assume property(@(posedge clk) $rose(started) |-> started==1); 
	
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
6

Jarno,
Since you say Formal engine, I strongly suggest you avoid long temporals and use “auxiliary” code or “modelling code” to assist SVA code.

Consider:



  bit first_rise_in_enb_detected;

  always_ff @(posedge clk iff !first_rise_in_enb_detected) begin
    if (!enb)
       first_rise_in_enb_detected = 0;
    else
       first_rise_in_enb_detected = 1;
  end

  assert property (@(posedge clk) !first_rise_in_enb_detected |-> out_put == 0);

You may need to tweak the logic and make it synthesizable to please your FV engine (is it Questa Formal?). Do let me know if you need further assistance.

Good Luck
Srini
http://www.verifworks.com

7

In reply to Srini @ CVCblr.com:

Love when co-authors disagree! With this code:

module test_1time2 (
		input clk, started, enb, rst_n,
		output x_out); 
	bit first_rise_in_enb_detected;
 
  always_ff @(posedge clk iff !first_rise_in_enb_detected) begin
    if (!enb)
       first_rise_in_enb_detected = 0;
    else
       first_rise_in_enb_detected = 1;
  end
 
  ap_xout: assert property (@(posedge clk) !first_rise_in_enb_detected |-> x_out == 0);
endmodule

the formal verification tool will toggle enb within the evaluation of the assertions. Thus, the variable first_rise_in_enb will toggle multiple times within the evaluations, and ap_xout assertion will be evaluated multiple times. You need assume statements to constraint the behavior of enb.
This is what I did with

am_1time: assume property(@(posedge clk) $rose(enb) |-> started==1); 
am_started: assume property(@(posedge clk) $rose(started) |-> started==1);

:)
Ben SystemVerilog.us

8

In reply to ben@SystemVerilog.us:

Ben,
Of-course we love confrontations :-) But in this case I don’t see one. We are augmenting each other well. My code was to show the core of “checking”, all around needed for a formal tool needs to be done by user. FYI - some FV tools don’t treat assume as is by default and require config/TCL files to do so. Unless the OP says which tool/version he uses it will be difficult to freeze. But I hope he can take it from here.

With due regards,
Srini

9

In reply to Srini @ CVCblr.com:

Thank you guys for good answers! Already here’s much info that is not written into the SVA books and on-line helps ;)

I shall try out these methods and then if all is ok, close this item.

I did not mention tools used, since this is a commercial forum and I am not sure what the rules say. But in principle this is a general question and therefore applicaple to all Mentor tools as well.

10

In reply to ben@SystemVerilog.us:

Change
fifo_empty_a : assert property (@(posedge clk) disable iff (!rst_n)
!started ##0 (enb== 0, set_started(1)) |-> x_out==0);

To
fifo_empty_a : assert property (@(posedge clk) disable iff (!rst_n)
!started |-> x_out==0);
I had the function call for simulation. Not needed

11

In reply to Jarno:

You’re welcome. On tools, I believe it’s ok to mention tools as long as you don’t mention how to use, or which is better, or competitive features restricted under NDA agreement.
Btw, I made a slight correction in my above response.

12

In reply to ben@SystemVerilog.us:

Sorry for the delay. I still haven’t had the time to check the solutions, but I think there’s a feature in Srinis proposal:

  always_ff @(posedge clk iff !first_rise_in_enb_detected) begin
    if (!enb)
       first_rise_in_enb_detected = 0;
    else
       first_rise_in_enb_detected = 1;
  end

Above code resets first_rise_in_enb_detected when enb==0. So if enb toggles, so will also first_rise_in_enb_detected.

So I would bet my money on this:

if (enb)
  first_rise_in_enb_detected=1 // basic latch forever

And init the first_rise_in_enb_detected to 0 at declaration.