Hi all,
I want to write an assertion with this flow:
A is going down for 100ns.
B toggle 20 times, only when A in low.
I need to check that the last edge of B happen at least 20ns before A go to high.
How can I catch the last edge?
Can I write a loop of 20 iterations?
Tried some options of loops, but nothing worked.
Thanks
If you donât have a clock for signals A and B, you can use tasks.
If you have clocks, then you can use SVA
I am showing 2 untested solutions, but they look OK
// A is going down for 100ns.
// B toggle 20 times, only when A in low.
// I need to check that the last edge of B happen at least 20ns before A go to high.
bit a, b;
task automatic toggle;
$realtime b_now;
b_now=$realtime;
int count;
fork
begin // check b
forever begin // while (a==0)
@(b) count++ ;
b_now=$realtime;
end
end
begin
@(posedge a)
am_tdiff: assert($realtime - b_now == 20ns);
am_numb: assert(count==20);
end
join_any
endtask
always @(negedge a) toggle();
//-----------
bit a, b, clk;
property p;
realtime v;
int count;
@(posedge clk) ($fell(a), v=$realtime, count=0) |->
(@(clk) (1, v=$realtime)[*1:$] intersect a[->1]) ##0
$realtime - b_now == 20ns ##0 count==20;
endproperty
Thanks,
I tried to do it, but understand that the require is different a bit.
A is going down - donât know for how long.
B should toggle 22 times
I need to check that from last edge of B there are at least 8ns before A will be high.
Tried to rewrite the code you gave, but still not work to me.
could you help me please?
Thanks.
Show your code and testbench
Explain the requirements in more details.
This is the code, Iâm sure something wrong, but donât know what.
the requires:
Iâm implementing SPI protocol, once CS fall, the SCLK toggle 22 times and after CS rise again.
I want to check from last edge of the clock, CS is stable at least for 8ns.
Thanks
module spi_assertios ();
logic assert_clk = 0;
always #1ns assert_clk = ~assert_clk;
property wait_clock();
realtime v,b;
int count;
(1, v=$realtime, count=0) |->
(@(posedge spi_qspi_vif.SCLK) (1, b=$realtime)[*1:$] intersect spi_qspi_vif.CS[->1]) ##0
$realtime - b == 8ns ##0 count==22;
@(negedge spi_qspi_vif.SCLK);
endproperty
assert_Thss : assert property (@(posedge assert_clk) @(negedge spi_qspi_vif.CS) -> (wait_clock()) |-> )$display("Assertion assert_Thss Passed");
else $display("Assertion assert_Thss Failed");
endmodule
who can please help me?
Show us a simple module with no interfaces. Generate 2 sets of stimulus: one that passes and one that should fail.
Hi Ben,
where is count changes in the property you shared
bit a, b, clk;
property p;
realtime v;
int count;
@(posedge clk) ($fell(a), v=$realtime, count=0) |->
(@(clk) (1, v=realtime)[*1:] intersect a[->1]) ##0
$realtime - b_now == 20ns ##0 count==20;
endproperty
Sorry, it should have been
bit a, b, clk;
property p;
realtime v;
int count;
@(posedge clk) ($fell(a), v=$realtime, count=0) |->
(@(clk) (1, v=$realtime, cout++)[*1:$] intersect a[->1]) ##0
$realtime - b_now == 20ns ##0 count==20;
endproperty
Ben, two quick questions
(1) As the requirement in âB toggle 20 times, only when A in lowâ, shouldnât âbâ be part of lhs of intersect operator ?
(2) Can lhs & rhs of intersect operator have different clocking event ?
(2) Can lhs & rhs of intersect operator have different clocking event ?
No. But, OK FOR THIS
@(posedge clk0) x ##0 @(posedge clk1)
(seq1 intersect seq2) ##0 @(posedge clk0) seq3
Hi Ben,
(A) The requirement at the top of this thread mentions
A is going down for 100ns.
B toggle 20 times, only when A in low.
I need to check that the last edge of B happens at least 20ns before A go to high.
As we want to check that âbâ should toggle 20 times when âaâ is low,
shouldnât we check for âbâ in lhs of intersect operator ?
property p;
realtime v;
int count;
@(posedge clk) ($fell(a), v=$realtime, count=0) |->
(@(clk) <seq_expr_involving_b>[*1:$] intersect a[->1]) ##0 $realtime - b_now == 20ns ##0 count==20;
endproperty
The requirement that âbâ should toggle 20 times when âaâ is low has 2 possible interpretations
(1) Change in âbâ is is checked on each posedge of clk
(2) Change in âbâ is is detected asynchronously
Limitation with (1) is that if âbâ were to toggle twice b/w 2 posedges of clk Tx & Ty,
sampled value of âbâ at Ty would be same as the previous clock Tx (as âbâ changed twice)
I feel a more robust solution would be (2) as it detects transition in âbâ between 2 clock edge as well
(B)
I found an older post where the logical reasons behind legality are mentioned.
For multiclocked âintersectâ, itâs acceptable if the lhs & rhs sequence start at different clocks (similar to multiclocked âandâ)
However, the issue with multiclocked âintersectâ is that the ending of the 2 sequences canât be guaranteed with non-identical clocks (for multiclocked âandâ the 2 sequences could end at different clocks)
See http://systemverilog.us/vf/a20bnota.pdf
task automatic t();
int count=0, pass=0;
realtime vnow=$realtime, vend;
fork
begin @(posedge a); end
begin forever begin
@(b) count++;
vend=$realtime;
end
end
join_any;
am_ab: assert($realtime-vend <- 20ns && count ==20);
am_a2a: assert($realtime-vnow == 100ns);
endtask
always @(posedge a) t();
I found an [older post]
where the logical reasons behind legality are mentioned.
Correct, multiclocking is is illegal in intersect
ap: assert property(@ (posedge clk) a[*5] and @(b) b[*4] );
Directive âapâ has multiple leading clocks for its maximal property.
ap: assert property(@ (posedge clk) a[*5] and @(posedge clk) 1 ##0 @(b) b[*4] );
OK
Ben,
On testing the code from above pdf
bit clk , a = 1 , b ;
always #5 clk = !clk;
property p;
realtime v;
int count;
($fell(a), v=$realtime, count=0) |-> @(clk) ( ($changed(b), count++)[*1:$] intersect a[->1] )
##0 @(posedge clk) $realtime - v == 20ns ##0 count==20;
endproperty
ap:assert property( @(posedge clk) p);
initial begin
#14; a = 0; // Antecedent matches at T:15 & consequent starts evaluation
#06; b = !b; // T: 20 'b' toggles for the 1st time
// Assume that 'b' toggles 19 more times before 'a' is asserted
#2 $finish();
end
Assertion fails at T:15 as lhs of intersect is false whereas rhs matches due to !a[*1]
( RHS a[->1] is equivalent to !a[$0:$] ##1 a )
For intersect to pass both lhs & rhs should match at T:15 i.e the starting clocking event
I believe property âpâ is incorrect since it expects $changed(b) to match on every clocking event i.e @(clk)
Since this thread already has a lot of replies I am thinking to create a new one to discuss possible solution using concurrent assertion.
Will share the link here once I post it
EDIT :: using-go-to-v-s-non-consecutive-repetition-within-intersect-operator
($fell(a), v=$realtime, count=0) |-> @(clk) ( ($changed(b), count++)[*1:$] intersect a[->1] )
##0 @(posedge clk) $realtime - v == 20ns ##0 count==20;
Asserting on an illegal multiply clocked temporal expression. The clock flow cannot change in the RHS of âintersectâ operator.
Ben,
On edalink I donât see the compilation/elaboration error that you have mentioned.
I observe the fail action block executes at T:15 as per expectations for the two stimulus
Am I missing something ?
Hi Ben,
Wanted to check with you on 2 quick changes
(1) As the task t() should be called only when âaâ is deasserted, shouldnât we write $fell(a) ?
always@(posedge clk) begin
if( $fell(a) ) // Infers clocking event from procedural block
t(); // Call task 't' only when $fell(a) is true
endtask
(2) Within the task, shouldnât we write $rose(a,@(posedge clk)) instead of @(posedge clk) ?
@(posedge clk) would unexpectedly unblock for 0 â X or 0 â Z transition whereas
$rose(a,@(posedge clk) ) would be true only when there 0/X/Z to 1 transition
task automatic t();
int count,pass; // Default value of 0
realtime vnow = $realtime; // Used in 'alow_2_ahigh'
realtime vend = 0; // Will be at default incase 'b' doesn't transition at all
fork
begin
wait( $rose(a,@(posedge clk) ); // Replaced @(posedge a) !!
end
begin
forever begin
@(b) count++;
vend = $realtime();
end
end
join_any;
disable fork; // Added
if( count > 0 ) // True if 'b' toggled at least once
// Check that 'b' toggled 20 times and last toggle of 'b' was at least 20ns prior to $rose(a)
am_ab: assert( ($realtime-vend >= 20ns) && count ==20);
else
$error("Signal b did not toggle between $fell(a) & $rose(a)");
// Check that 'a' was de-asserted for 100ns
alow_2_ahigh: assert($realtime-vnow == 100ns);
endtask
[You] (1) As the task t() should be called only when âaâ is deasserted, shouldnât we write $fell(a) ?
[Ben] Yes, minor mistake, buyt the approach is good
[You]
($fell(a), v=$realtime, count=0) |-> @(clk) ( ($changed(b), count++)[*1:$] intersect a[->1] )
##0 @(posedge clk) $realtime - v == 20ns ##0 count==20;
Asserting on an illegal multiply clocked temporal expression. The clock flow cannot change in the RHS of âintersectâ operator.
On edalink I donât see the compilation/elaboration error that you have mentioned.
[Ben] I have a tool that doesnât like it.
We donât lalk about tools.
In any case, these tyes of problems are not frequent and can be handled with automatic tasks/