How Can I Disable an Assertion Once It Passes Using a Local Variable?

This question is related to another one I asked a while back regarding holding off an assertion. I have an property that has 2 chained implications. I want to make the first implication vacuously pass, thereby skipping the assertion from then on, after the assertion passes once. Here’s the code:

sequence sw_op_antecedent_seq;
	@(posedge CE_bar) ((Address == sw_op_seq_addr1) && (OE_bar == 0)) ##1
	                  ((Address == sw_op_seq_addr2) && (OE_bar == 0));
	endsequence

sequence sw_op_consequent_seq;
	@(posedge CE_bar) ((Address == sw_op_seq_addr3) && (OE_bar == 0)) ##1
	                  ((Address == sw_op_seq_addr4) && (OE_bar == 0)) ##1
	                  ((Address == sw_op_seq_addr5) && (OE_bar == 0));
	endsequence

sequence sw_op_autostore_dis_seq;
	@(posedge CE_bar) ((Address == sw_op_autostore_dis) && (OE_bar == 0));
	endsequence

property sw_op_setup_prop;
	@(negedge OE_bar) disable iff (rst !== 1)
		sw_op_antecedent_seq |=> sw_op_consequent_seq;
	endproperty

property sw_op_autostore_dis_prop;
	bit sw_op_done = 0;
	@(negedge OE_bar) disable iff (rst !== 1)
  1.  	sw_op_antecedent_seq |=> sw_op_consequent_seq |=> sw_op_autostore_dis_seq;
    
  2.  		((sw_op_antecedent_seq, sw_op_done = 1) and !sw_op_done) |=> sw_op_consequent_seq |=> sw_op_autostore_dis_seq;
    
  3.  		(sw_op_antecedent_seq and !sw_op_done) |=> sw_op_consequent_seq |=> (sw_op_autostore_dis_seq, sw_op_done = 1);
     endproperty
    

    assert property…

Option 1) works to an extent. The assertion correctly PASSED. Options 2) and 3) do not compile and give the error “** Error: …/…/verif/tb/src/lmgi/assertions/nvsram_if_asserts.sv(582): (vlog-2048) Directive ‘nvsram_sw_op_autostore_dis_assert’ has multiple leading clocks for its maximal property. Please fix the clocking issues.”, which points to the assert property statement. This looks like perfectly legal code to me. I need this functionality for multiple uses. Any suggestions?

You need to read 1800’12 16.10 Local variables

d) In the case of and and intersect, a local variable that flows out of at least one operand shall flow out of the composite sequence unless it is blocked. A local variable is blocked from flowing out of the composite sequence if either of the following statements applies:

I explain this in my book. Basically, When two sequences are ANDed or INTERSECTed, each sequence produces its own thread. However, unlike the ORing of two sequences, the and/intersect of two sequences produces a single end point at the termination of the threads. This means that the two threads merge into a single starting point; this contrasts to the Oring of two sequences where each thread is carried separately to the next sequence.
If the sequence makes assignments to local variables, then each of the sequence involved in the ANDing or INTERSECTing carries its own individual and separate copy of the local variables. However, only those local variables that are NOT assigned in both threads flow out of the sequence. So what does that mean?

[code] property p1_ok;
bit v;
@(posedge clk) (a ##1 b, v=1) and @(posedge clk) v |=> d; // line 13
endproperty
assert property(p1_ok);
** Error: qst2.sv(13): Local variable v referenced in expression where it does not flow.
** Error: qst2.sv(15): The sva directive is not sensitive to a clock. Unclocked directives are not supported.
// Though there one local variable declaration called “v”, in reality, because of there are 2 threads separated by the AND operator, there exits 2 separate local variables, one v_for_thread1, and one v_for_thread2.
Will get back to you for more comments, but that is the issue.

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

/* This question is related to another one I asked a while back regarding holding off an assertion. I have an property that has 2 chained implications. I want to make the first implication vacuously pass, thereby skipping the assertion from then on, after the assertion passes once. Here’s the code: */

Your requirements are not very clear. From your attempt at the assertions with

2) ((sw_op_antecedent_seq, sw_op_done = 1) and !sw_op_done) |=> sw_op_consequent_seq |=>
                       sw_op_autostore_dis_seq;

I have the following comments about your understandings of assertions and what you expect:

  1. You’re setting sw_op_done = 1 at the endpoint of that sequence with the intent that the next attempt at this assertion will be disable. If this is your goal, what you’re doing is totally wrng because:
    a) At every leading clocking event a new attempt is made at the assertion, and if that attempt is successful, then any local variable for that assertion is tied to that assertion, and is independent from any previous or new thread previously started or started in the future. Thus, you “and !sw_op_done” does nothing for you, except create an error since it does not have a clocking event for starting it.
    b) What I think you want is the following assertion wriiten in English first (BTW, for comlex assertions, write your requirements in English first):
    At the first successful endpoint of sequence1 of my assertion, prevent other new attempts of that assertion, and cancel any in-progress assertion until my assertion terminates with a pass or fail.
    To do something like this, you’ll need an external signal that enables those assertions that need to be started, and to make vacuous those that started. Thus, I am thinkng of something like the following:
bit go; \
function void setgo(bit x); 
	 go=x; 
endfunction 
ap_sw_op_autostore_dis : assert property ( @(posedge CE_bar)
		(sw_op_antecedent_seq, setgo(1))   |=> sw_op_consequent_seq |=>
                       sw_op_autostore_dis_seq;

sequence sw_op_antecedent_seq;
 @(posedge CE_bar) (go && (Address == sw_op_seq_addr1) && (OE_bar == 0)) ##1
    ((Address == sw_op_seq_addr2) && (OE_bar == 0));
endsequence
sequence sw_op_consequent_seq;
   @(posedge CE_bar) (go && (Address == sw_op_seq_addr3) && (OE_bar == 0)) ##1
     ((Address == sw_op_seq_addr4) && (OE_bar == 0)) ##1
     ((Address == sw_op_seq_addr5) && (OE_bar == 0));
endsequence
sequence sw_op_autostore_dis_seq;
   @(posedge CE_bar) ((Address == sw_op_autostore_dis) && (OE_bar == 0));
endsequence

BTW, if the tool supports the property “reject_on ( expression_or_dist ) property_expr”, you can use that to cancel any ongoing assertion.

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

  • SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6

In reply to ben@SystemVerilog.us:

On another thing, to insure exclusivity, don’t forget the $rose function. Thus,

($rose(Address == sw_op_seq_addr1) && (OE_bar == 0)) ##1
((Address == sw_op_seq_addr2) && (OE_bar == 0));

On my solution with teh “go” varable, it needs some work n the polarites, an the number of passible go variables you need. It’s a bit tricky.
Ben