Hello,
Can I please get some help in writing an assertion with this question :-
signal1 will be high for few number of clock cycles, signal2 can only be high for one clock cycle when signal1 is high, we don’t care about signal2 when signal1 is not high.
In reply to Ashmika:
Requirement :
Sig1 will be high for a few numbers of clock cycles. // Number of clocks are unknown
sig2 can only be high for one clock cycle while sig1 is high.
sig2 toggles do not care if sig1 is not high.
property
@(posedge clk)
$rose(sig1) |-> sig2[->1] ##1 !sig2[*1:$] intersect sig1[*1:$];
endproperty
In reply to kddholak:
Thank you for replying
But can you tell me why do use this :-
sig2[->1] ##1 sig2[*1:$]
this means it’s expecting sig2 too be high more atleast 1 clock cycle
requirement is just 1 clock cycle
In reply to Ashmika:
[quote]In reply to kddholak:
Thank you for replying
But can you tell me why do use this :-
sig2[->1] ##1 sig2[*1:] => corrected the typo. sig2[->1] ##1 !sig2[*1:]
In reply to Ashmika:
signal2 can only be high for one clock cycle
I am assuming you expect sig2 to be high on only 1 posedge of clock .On next posedge Sig2 should be low .
Since you are interested in checking Sig2 only when Sig1 is high :
property prop ;
@(posedge clk)
$rose(sig2) && sig1 |=> $fell( sig2 ) ;
endproperty
EDIT : Both Sig1 and Sig2 could be asserted on same posedge hence :
property prop ;
@(posedge clk)
first_match( ( $rose(sig2) && sig1 ) or ( $rose(sig2) && $rose(sig1) ) ) |=> $fell( sig2 ) ;
endproperty
In reply to MICRO_91:
Comments about the replies:
Requirement :
Sig1 will be high for a few numbers of clock cycles. // Number of clocks are unknown
sig2 can only be high for one clock cycle while sig1 is high.
sig2 toggles do not care if sig1 is not high.
property
@(posedge clk)
$rose(sig1) |-> sig2[->1] ##1 !sig2[*1:$] intersect sig1[*1:$];
endproperty
I see an ambiguity in the requirement sig2 can only be high for one clock cycle while sig1 is high. Does that mean that there ONE sig2 between $rose(sig1) and ($fell(sig1))?
rose(sig1) |-> sig2[->1] ##1 !sig2[*1:] intersect sig1[*1:$];
when the sequence sig2 ##1 !sig2occurs, the consequent is satisfied.
However, it fails to check if sig2 occurs again for one or more cycles when sig1 remains high for more cycles.
How about something like:
Edit code - EDA Playground // code
EPWave Waveform Viewer // wave
module my_module;
bit clk, sig1, sig2;
int pass, fail;
initial forever #1 clk = !clk;
ap_sig1_2: assert property( @(posedge clk)
$rose(sig1) |-> (sig1 && sig2)[=1] intersect
##1 !(sig1)[->1]) pass=pass+1; else fail=fail+1;
initial begin
$dumpfile("dump.vcd"); $dumpvars;
#2 @(posedge clk) sig1 <= 1;
repeat(2) @(posedge clk);
sig2 <=1; @(posedge clk) sig2 <= 0;
repeat(2) @(posedge clk);
sig1 <= 0;
#4 $finish;
end
endmodule
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
or Cohen_Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog
In reply to ben@SystemVerilog.us:
I was also suggested the following that also works.
Edit code - EDA Playground // code
EPWave Waveform Viewer // wave
ap_sig1_2b: assert property(@(posedge clk)
$rose(sig1) |-> (sig1[*] intersect sig2[=1]) ##1 !sig1)
pass=pass+8; else fail=fail+8;
initial begin
In reply to ben@SystemVerilog.us:
Hi Ben ,
(1)
I see an ambiguity in the requirement sig2 can only be high for one clock cycle while sig1 is high. Does that mean that there ONE sig2 between $rose(sig1) and ($fell(sig1))?
My interpretation was that only if both sig1 and sig2 are high then , sig2 should be de-asserted at next posedge of clk . Hence I used **$fell( sig2 )** in the consequent
(2) Consider scenario where sig1 is high throughout from posedge T1 to T10 .
My understanding is that Sig2 could be asserted and de-asserted multiple times during this time.
However if we use $rose(sig1) as the antecedent we would miss out on 2nd $rose(Sig2).
(3) Out of curiosity , what is considered the left sequence_expr for intersect operator ?
property prop;
@(posedge clk)
$rose(sig1) |-> sig2[->1] ##1 !sig2[*1:$] intersect sig1[*1:$];
endproperty
Is it **!sig2[*1:$]** OR the entire sequence : **sig2[->1] ##1 !sig2[*1:$] ?**
In reply to Ashmika:
I split that to two properties as below. Untested though.
// Sig1 will be high for a few numbers of clock cycles.
// Number of clocks are unknown
// sig2 can only be high for one clock cycle while sig1 is high.
$rose (sig1) |-> sig1 until_with sig2;
$rose (sig2) |=> !sig2;
// sig2 toggles do not care if sig1 is not high.
Good luck
Srini
In reply to ben@SystemVerilog.us:
In reply to MICRO_91:
Comments about the replies:
I see an ambiguity in the requirement sig2 can only be high for one clock cycle while sig1 is high. Does that mean that there ONE sig2 between $rose(sig1) and ($fell(sig1))?
rose(sig1) |-> sig2[->1] ##1 !sig2[*1:] intersect sig1[*1:$];
when the sequence sig2 ##1 !sig2occurs, the consequent is satisfied.
However, it fails to check if sig2 occurs again for one or more cycles when sig1 remains high for more cycles.
How about something like:
Edit code - EDA Playground // code
EPWave Waveform Viewer // wave
module my_module;
bit clk, sig1, sig2;
int pass, fail;
initial forever #1 clk = !clk;
ap_sig1_2: assert property( @(posedge clk)
$rose(sig1) |-> (sig1 && sig2)[=1] intersect
##1 !(sig1)[->1]) pass=pass+1; else fail=fail+1;
initial begin
$dumpfile("dump.vcd"); $dumpvars;
#2 @(posedge clk) sig1 <= 1;
repeat(2) @(posedge clk);
sig2 <=1; @(posedge clk) sig2 <= 0;
repeat(2) @(posedge clk);
sig1 <= 0;
#4 $finish;
end
endmodule
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
or Cohen_Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog
https://rb.gy/f3zhh
Hi Ben.
I think I might miss something with “intersect”. In the below property you gave, Let us say if (sig1 && sig2)[=1] happens at T5 and sig2 drops at T6, !(sig1)[->1] happens at T10. At which point they intersect ?
Thanks
ap_sig1_2: assert property( @(posedge clk)
$rose(sig1) |-> (sig1 && sig2)[=1] intersect
##1 !(sig1)[->1]) pass=pass+1; else fail=fail+1;
In reply to MICRO_91:
On item 1, I wrote the model with my understanding of the requirements. If there is are different requirements, then the model needs to change.
In any case, the nice thing about writing SVA is that it puts on the dots on the requirements.
on
(3) Out of curiosity , what is considered the left sequence_expr for intersect operator ?
rose(sig1) |-> sig2[->1] ##1 !sig2[*1:] intersect sig1[*1:$];
This is resolved in 1800 by the definition of
1800: 16.9.1 Operator precedence Operator precedence and associativity are listed in Table 16-1 . The highest precedence is listed first. Table 16-1—Operator precedence and associativity
Here ## has higher precedence than intersect. Thus,
sig2[->1] ##1 !sig2[*1:] is computed first. In other words,
sig2[->1] ##1 !sig2[*1:] intersect sig1[*1:]
is same as
(sig2[->1] ##1 !sig2[*1:]) intersect sig1[*1:$]
In reply to VE:
ap_sig1_2: assert property( @(posedge clk)
$rose(sig1) |-> (sig1 && sig2)[=1] intersect
##1 !(sig1)[->1]) pass=pass+1; else fail=fail+1;
!(sig1)[->1] happens at T10. At which point they intersect ?
[Ben] the intersection would be when sig1==0 at T10