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:
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?
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.
/* 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
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: