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