if i use above assertion it will run only once, if i replace overlapping(|->) implication operator with the non-overlapping implication(|=>) operator it runs continuously.
please explain me the reason behind running the assertion continuously?
first_match(some_sequence): The first_match operator matches only the first of possibly multiple matches for an evaluation attempt of its operand sequence. This allows all subsequent matches to be discarded from consideration. This is significant when a sequence is used in the antecedent of an assertion because when a range is used in the antecedent, it can create multiple threads, each triggering the evaluation of the consequent when matched, and all threads must hold for the assertion to hold. This can cause significant performance impacts and possible unexpected errors.
From my SVA book: applying the first_match operator has significant (positive) effect on the evaluation of the enclosing sequence. Consider the following example:
ap_never_succeed: assert property(
($rose(a) ##[2:$] b) |=> c);
The assertion ap_never_succeed is equivalent to
ap_equivalent_to_ap_never_succeed: assert property(
($rose(a) ##2 b)or
($rose(a) ##3 b)or
…
($rose(a) ##n b)|=> c); // where n is infinity
For the ap_equivalent_to_ap_never_succeed assertion to succeed, all threads must succeed, and there are an infinite number of threads; specifically, these threads include:
($rose(a) ##2 b) |=> c // thread 1
($rose(a) ##3 b) |=> c // thread 2
…
($rose(a) ##n b)|=> c // thread n
If any of these threads fails, then the assertion fails; however success cannot be achieved. With the first_match method, only the first match of the sequence is considered, and all other threads are ignored. Thus, in the assertion ap_FM_can_succeed a first match of the antecedent is considered for the evaluation of the consequent.
ap_FM_can_succeed: assert property(
first_match(rose(a) ##[2:] b) |=> c); Files Ch2/2.5/S1B_FM.sv, S1B_FM_wave.bmp, S1B_FM_
Your code: first_match(reset==0) |-> (datain ==0);
The first_match(expression) is same as expression because the sequence is a single term.
@ (posedge clk) reset==0 |-> (datain ==0); Says for an assertion of this property, at every (posedge clk) there is a new attempt at the evaluation of the property.
reset==0) |-> (datain ==0); Says that if @ (posedge clk) reset==0, then in that same clocking event the sampled value (datain ==0). This does not take into account the effect of the reset.
If reset is active low (typical), and at power up stays low for a few milliseconds until power to the circuit settles up the the needed level (e.g., 5V), then you could do onbe of the following options:
initial begin
wait(power_ready);
ap_reset: assert property(@ (posedge clk) reset==0 |=> datain ==0);
// Can also use an immediate assert statement
if(reset==0) assert (datain ==0);
end
I Understood the concept of first_match , But my question why if I replace overlapping operator with non-overlapping antecedent triggers many time.
i am writing assertion for this condition
module reset_check(input bit[31:0] datain);
bit temp_clk;
bit clk;
bit reset;
always temp_clk = #5ns ~templ_clk;
assign clk = (set_clk)?temp_clk:0;
initial begin
reset =1'b1;
set_clk =1'b0;
#20ns;
reset= 1'b0;
#30ns;
set_clk =1'b1;
// Some Other code
end
default clocking utmi_clk @(posedge clk) endclocking;
property pro_check_after_reset;
// If i use this condition assertion runs only one time
first_match(reset==0) |-> (datain ==0);
// If i use this condition assertion runs many time
first_match(reset==0) |=> (datain ==0);
endproperty
assert property(pro_check_after_reset);
endmodule
If you understood the meaning of first_match, you would not still be trying to use it.
What you mean by “triggers many time”. Do you mean it “fails each posedge clk”? Where is the assertion statment in relation to reset_check module? There is no posedge clk anytime reset==0, so it would never trigger.
It would really help to provide a mininal example that duplicates the results you are seeing.
I try to figure out the process from “ap_equivalent_to_ap_never_succeed”
to “every thread must succeed to succeed the assertion” ?
ap_never_succeed: assert property(
(rose(a) ##[2:] b) |=> c);
The assertion ap_never_succeed is equivalent to
ap_equivalent_to_ap_never_succeed: assert property(
($rose(a) ##2 b)or
($rose(a) ##3 b)or
…
($rose(a) ##n b)|=> c); // where n is infinity
For the ap_equivalent_to_ap_never_succeed assertion to succeed, all threads must succeed, and there are an infinite number of threads; specifically, these threads include:
($rose(a) ##2 b) |=> c // thread 1
($rose(a) ##3 b) |=> c // thread 2
…
($rose(a) ##n b)|=> c // thread n
My understanding of “all thread must succeed to succeed the assertion”
looks like below, there are “and” between them
//my understanding
ap_equivalent_to_ap_never_succeed_mod: assert property(
($rose(a) ##2 b) and
($rose(a) ##3 b) and
…
($rose(a) ##n b)|=> c); // where n is infinity
and the original “ap_equivalent_to_ap_never_succeed”
should be “one of threads succeed will succeed the assertion”
In my understanding,
“##[2:$]” means “between cycle-2 and cycle-infinity, there should be at least one…”
Could anyone tells me where my misunderstandings are?
ap_never_succeed: assert property(
($rose(a) ##[2:$] b) |=> c);
// The assertion ap_never_succeed is equivalent to
ap_equivalent_to_ap_never_succeed: assert property(
($rose(a) ##2 b)or // NOTE: The ORing is in the antecedent
($rose(a) ##3 b)or
…
($rose(a) ##n b)|=> c); // where n is infinity
// Thus for failure, all you need is any of the antecedent thread to match and
// its corresponding consequent to be a nonmatch
// If any antecedent of thoses threads is a nonmatch, then that thread is vacuously TRUE.
// You wrote "//my understanding
/* ap_equivalent_to_ap_never_succeed_mod: assert property(
($rose(a) ##2 b) and
($rose(a) ##3 b) and
…
($rose(a) ##n b)|=> c); // where n is infinity */
// [Ben] NO, you are incorrect. With your ANDind assumption of
// ANDing all threads of the antecedent, if any thread of the antecedent is a nonmatch
// then the assertion is vacously trrue.
// (1 and 1 and 0 and 1 ... and (whatever) |=> 1 // is vacuously true
//For the ap_equivalent_to_ap_never_succeed assertion to succeed, all threads must succeed,
// and there are an infinite number of threads; specifically, these threads include:
// ANOTHER way of seeing the treads
(($rose(a) ##2 b) |=> c) and // thread 1 property
(($rose(a) ##3 b) |=> c) and // thread 2 property
…
(($rose(a) ##n b)|=> c) // thread n
// "all thread must succeed to succeed the assertion"
// The ANDing is in the equivalent property threds
// I had the ORing in the antecedent threads.
// Different way of looking at it.
// Thus for failure, all you need is any of the antecedent thread to match and
// its corresponding consequent to be a nonmatch
// If any antecedent of thoses threads is a nonmatch, then that thread is vacuously TRUE.
I think I misunderstood this part.
Your explanation is very clear.
NO to your question.
first_match(a_sequence) means that when a match occurs, there is no evaluation of other possible matches FOR THAT ä_sequence. The first_match does not address the consequent in your example.
It only addresses the first match of a sequence that is multi-threaded. In your example
first_match (rose(a) ##[2:] b), if the thread ($rose(a) ##[2] b) is a match, then the other threads (e.g., ($rose(a) ##[3] b), … ($rose(a) ##[N] b)) are not evaluated.
The property where the antecedent thread that matches evaluates its consequent.
All those previous antecedent threads that had no match cause the property for those cases to be vacuous.
first_match($rose(a) ##[2:$] b)|=> c; // IS SAME AS
first_match(
($rose(a) ##2 b) or // thread 1 property
($rose(a) ##3 b) or or // thread 2 property
…
($rose(a) ##n b)) |=> c) // thread n
ANALOGY: I have 3 decks of cards and every 3 seconds I show you a new card.
You are looking for the sequence ACE card followed by KING card. Thus, for 30 seconds I show you a new cards with NO ACEs, but some KINGs.
At time 33 I show you an ACE followed at time 36 by a KING card. THAT is your first match because the ACE folloed by KING came up and it meets the match you were looking for. The fact that the decks may have other ACEs or KINGs is of no significance here. Now the ACE/KING sequence is a precondition (antecedent) for you to win the game. After the ACE you need to check the consequent (maybe lunch is served immediately after that ACE/KING sequence?)
If no lunch, the assertion fails.
:)
Hi Ben,
How about two antecedent of sequence match at the same time?
First_match(Seq a or seqb ) |-> c ,I mean seq a seq b are true at the same cycle
How to know which one is first
In reply to peter:
You DO NOT have 2 antecedents in *first_match(seqa or seqb ) |-> c ,
*You only have ONE antecedent that has 2 sequence threads, both of which start at the same time.
For the property to succeed, the consequent property that follows any of the first matched thread of the antecedent (seqa or seqb) must be true.
If seqa and seqb match in the same cycle, the same thing happens (i.e., the consequent property that follows the any of first matched thread of the antecedent (seqa or seqb) must be true.
Ir does not matter as to which one succeeded first. A tool will short-circuit all other sequence threads evaluation after it found a first match.
In my paper "Reflections on Users’ Experiences with SVA
I describe what a thread is: Thread: A thread is a search path for the property’s success within an evaluation attempt that starts at the leading clocking event of the property. For example, a bus request that is acknowledged within 1 to 2 cycles has 2 threads: request followed by acknowledge in 1st cycle, or a request followed by acknowledge in 2nd cycles. A sequence is multi-threaded if it includes any of the following operators: and, intersect, or, range delay (e.g., ##[1:3] a), consecutive range repetition (e.g., a[*1:3]), and non-consecutive repetition (e.g., a[->1], a[=1]).
Adding more to the thread definition, that word addresses both: 1) threads in sequences, and 2) threads in properties. That is confusing. Some clarifications:
(seqa or seqb ) |-> c; // property has ONE antecedent and ONE consequent
// * antecedent has 2 sequence threads, seqa and seqb
// * The antecedent is a single sequence (see 1800 as to what represents a sequence)
// * The property has 2 property threads including:
// seqa |-> c, seqb |-> c
// * For the assertion to both property threads must be true and none must fail.
// * A vacuous property is true vacuously
// * For a nonvacuous assertion PASS there must be at least ONE property thread that is
// nonvacuous, and no property thread that fails.
// * A first_march(multithreaded_sequence) picks the first thread and excludes the other threads
// for the evaluation of the property.
Hi Ben,
You mentioned that A first_march(multithreaded_sequence) picks the first thread and excludes the other threads.
Do you mean that if the first thread is true and other threads are false, that property will be true?
For (seqa or seqb ) |-> c; it has two threads. In 1800, I can not find some statements or example discussing about this. Do you see it in 1800?
Thank you