I need to code assertions for the following scenario
once valid is deasserted idle should not be asserted before x_delay cycles.
Here x_delay is from a register which can change mid simulation and also can be 0,
Another point, valid can be asserted back before idle is asserted check has to be disabled now,
Untested code, but looks very promising for your needs.
I user Perplexity.ai to clarify the case when valid drops but rises again before
idel has a chance to rise. There I did a ync_accept_on the property, making it vacuous.
// SVA Package: Dynamic and range delays and repeats
// SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy Provides a library and model solutions
// I need to code assertions for the following scenario
// once valid is deasserted, idle should not be asserted before x_delay cycles.
// Here x_delay is from a register which can change mid simulation and also can be 0,
// Another point, valid can be asserted back before idle is asserted check has to be disabled now,
// REPHRASE: VALID may rise again before IDLE has a chance to rise. In this scenario, IDLE should not rise.
// The check for IDLE rising should be disabled when VALID rises again before IDLE has asserted.
// valid 1 1 1 1 1 0 0 1 1 1 0 0 0 0 0 0 0 0
// idle 0 0 0 0 0 0 0 0 0 0 0 0 0 1
// accept_on ( expression_or_dist ) property_expr
module m;
import sva_delay_repeat_range_pkg::*;
/* //----------------------------------------------------------------
// ****** DYNAMIC REPEAT q_s[*d1] **********
// Implements a_sequence[*count]
// Application: $rose(a) |-> sq_rpt_simple_count(sq_1, d1)
sequence sq_rpt_simple_count(sq, count);
int v=count;
(1, v=count) ##0 ( v>0 ##0 sq, v=v-1) [*1:$] ##0 v<=0;
endsequence // sq_rpt_simple_count
//Note: "The sequence_expr of a sequential property shall not admit an empty match (see 16.12.22)." */
bit clk, idle, valid, reset_n=1;
bit[2:0] range=3;
assert property (@ (posedge clk)
disable iff (!reset_n)
sync_accept_on ( $rose(valid, @(posedge clk)) )
$fell(valid) |-> sq_rpt_simple_count(! idle, range) ##1 idle);
endmodule
Link to the list of papers and books that I wrote, many are now donated.
https://systemverilog.us/vf/Cohen_Links_to_papers_books.pdf
Another option without the accept_on is to make the property true if there is a new valid within the range
$fell(valid) |-> (sq_rpt_simple_count(! idle, range) ##1 idle) or // an idle after a range
(($rose(valid), v=range-1) ##1 (v<=0, v=v-1)[*1:$]); // valid within the range
// The whole model
// SVA Package: Dynamic and range delays and repeats
// https://rb.gy/a89jlh Provides a library and model solutions
// I need to code assertions for the following scenario
// once valid is deasserted, idle should not be asserted before x_delay cycles.
// Here x_delay is from a register which can change mid simulation and also can be 0,
// Another point, valid can be asserted back before idle is asserted check has to be disabled now,
// REPHRASE: VALID may rise again before IDLE has a chance to rise. In this scenario, IDLE should not rise.
// The check for IDLE rising should be disabled when VALID rises again before IDLE has asserted.
// valid 1 1 1 1 1 0 0 1 1 1 0 0 0 0 0 0 0 0
// idle 0 0 0 0 0 0 0 0 0 0 0 0 0 1
// accept_on ( expression_or_dist ) property_expr
module m;
import sva_delay_repeat_range_pkg::*;
/* //----------------------------------------------------------------
// ****** DYNAMIC REPEAT q_s[*d1] **********
// Implements a_sequence[*count]
// Application: $rose(a) |-> sq_rpt_simple_count(sq_1, d1)
sequence sq_rpt_simple_count(sq, count);
int v=count;
(1, v=count) ##0 ( v>0 ##0 sq, v=v-1) [*1:$] ##0 v<=0;
endsequence // sq_rpt_simple_count
//Note: "The sequence_expr of a sequential property shall not admit an empty match (see 16.12.22)." */
bit clk, idle, valid, reset_n=1;
bit[2:0] range=3;
ap_0: assert property (@ (posedge clk)
disable iff (!reset_n)
sync_accept_on ( $rose(valid, @(posedge clk)) ) // vacuous pass if rose of valid
$fell(valid) |-> sq_rpt_simple_count(! idle, range) ##1 idle); // an idle after a range
property p1;
int v;
disable iff (!reset_n)
@ (posedge clk)
$fell(valid) |-> (sq_rpt_simple_count(! idle, range) ##1 idle) or // an idle after a range
(($rose(valid), v=range-1) ##1 (v<=0, v=v-1)[*1:$]); // valid within the range
endproperty
ap_1: assert property (p1);
endmodule
Link to the list of papers and books that I wrote, many are now donated.
https://systemverilog.us/vf/Cohen_Links_to_papers_books.pdf
// 1. Idle should not be asserted before x_delay cycles after valid deassertion
property no_idle_before_delay;
@(posedge clk)
$fell(valid) |-> (idle == 0) [*0:$past(x_delay)];
endproperty
// 2. Disable check if valid is reasserted before idle
property disable_check_on_valid;
@(posedge clk)
$rose(valid) |-> (!($rose(idle) && check == 0))[*];
endproperty
$past(x_delay) is illegal because x_delay is not a static number known at elaboration time. It’s in a variable.
Explain “check”, how generated?
Explain the assertion. Have doubts
Hi Ben,
I tested the following
bit clk , idle , valid = 1 ;
int unsigned x_delay ;
always #5 clk = !clk;
sequence sq_rpt_simple_count(sq, count);
int v=count;
(1, v=count) ##0 ( v>0 ##0 sq, v=v-1) [*1:$] ##0 v<=0;
endsequence // sq_rpt_simple_count
//Note: "The sequence_expr of a sequential property shall not admit an empty match (see 16.12.22)."
assert property (@ (posedge clk) sync_accept_on ( $rose(valid, @(posedge clk)) ) $fell(valid) |-> sq_rpt_simple_count(!idle, x_delay) ##1 idle ) $display("T:%0t Pass",$time);
else $display("T:%0t Fails",$time);
initial begin
#4; valid = 0;
`ifdef M1
// 'x_delay' is 0 i.e $fell(valid) and $rose(idle) are both True at T:5
x_delay = 0 ;
idle = 1 ;
`elsif M2
// $fell(valid) is True at T:5. 'x_delay' is 2. However $rose(valid) is true at T:15 before $rose(idle)
// Should result in Vacuous Pass or disabling of the check
x_delay = 2 ;
#10 ; valid = 1 ; // T:14
#10 ; idle = 1 ; // T:24
`endif
#2; $finish();
end
(a) For +define+M1 ::
As ‘x_delay’ can be 0 which is equivalent to $fell(valid)|->$rose(idle);
However due to ( v > 0 ) the assertion fails at T:5 whereas the expectation is that is should pass
(b) For +define+M2 ::
Check has to be disabled since valid is asserted back before idle is asserted whereas the assertion passes at T:15 due to sync_accept_on
Thanks for doing the simulation.
Updates at EDA Playground
// SVA Package: Dynamic and range delays and repeats
// https://rb.gy/a89jlh Provides a library and model solutions
// I need to code assertions for the following scenario
// once valid is deasserted, idle should not be asserted before x_delay cycles.
// Here x_delay is from a register which can change mid simulation and also can be 0,
// Another point, valid can be asserted back before idle is asserted check has to be disabled now,
// REPHRASE: VALID may rise again before IDLE has a chance to rise. In this scenario, IDLE should not rise.
// The check for IDLE rising should be disabled when VALID rises again before IDLE has asserted.
// valid 1 1 1 1 1 0 0 1 1 1 0 0 0 0 0 0 0 0
// idle 0 0 0 0 0 0 0 0 0 0 0 0 0 1
// accept_on ( expression_or_dist ) property_expr
module m;
// import sva_delay_repeat_range_pkg::*;
//----------------------------------------------------------------
// ****** DYNAMIC REPEAT q_s[*d1] **********
// Implements a_sequence[*count]
// Application: $rose(a) |-> sq_rpt_simple_count(sq_1, d1)
sequence sq_rpt_simple_count(sq, count);
int v=count;
(1, v=count) ##0 ( v>0 ##0 sq, v=v-1) [*1:$] ##0 v<=0;
endsequence // sq_rpt_simple_count
//Note: "The sequence_expr of a sequential property shall not admit an empty match (see 16.12.22)."
bit clk, idle, valid=0, reset_n=1;
bit[2:0] range=2, p0, f0, p1, f1, p2, f2, p3, f3;
int unsigned x_delay ;
ap_0: assert property (@ (posedge clk)
disable iff (!reset_n)
sync_accept_on ( $rose(valid, @(posedge clk)) ) // vacuous pass if rose of valid
$fell(valid) |-> sq_rpt_simple_count(! idle, range) ##1 idle) p0++; else f0++; // an idle after a range
property p1b;
int v;
disable iff (!reset_n)
@ (posedge clk)
$fell(valid) |-> (sq_rpt_simple_count(! idle, range) ##1 idle) or // an idle after a range
(($rose(valid), v=range-1) ##1 (v<=0, v=v-1)[*1:$] ##1 idle) or
$rose(idle); // a valid within the range
endproperty
ap_1: assert property (p1b) p1++; else f1++;
always #5 clk = !clk;
/* sequence sq_rpt_simple_count(sq, count);
int v=count;
(1, v=count) ##0 ( v>0 ##0 sq, v=v-1) [*1:$] ##0 v<=0;
endsequence // sq_rpt_simple_count */
//Note: "The sequence_expr of a sequential property shall not admit an empty match (see 16.12.22)."
ap_v2: assert property (@ (posedge clk)
sync_accept_on ( $rose(valid, @(posedge clk)) ) $fell(valid) |->
sq_rpt_simple_count(!idle, x_delay) ##1 idle ) begin p2++; $display("T:%0t Pass",$time); end
else begin f2++; $display("T:%0t Fails",$time); end
ap_v2_fix: assert property (@ (posedge clk)
sync_accept_on ( $rose(valid, @(posedge clk)) ) $fell(valid) |->
sq_rpt_simple_count(!idle, x_delay) ##1 idle or $rose(idle) ) begin p3++; $display("T:%0t Pass",$time); end
else begin f3++; $display("T:%0t Fails",$time); end
initial begin
$dumpfile("dump.vcd");
$dumpvars;
repeat(2) @(posedge clk);
valid <=1;
x_delay <= 0 ;
repeat(2) @(posedge clk);
valid <= 0;
// `ifdef M1
// 'x_delay' is 0 i.e $fell(valid) and $rose(idle) are both True at T:5
// x_delay <= 0 ;
idle <= 1 ;
repeat(5) @(posedge clk);
valid <= 1;
idle <= 0;
repeat(2) @(posedge clk);
//`elsif M2
// $fell(valid) is True at T:5. 'x_delay' is 2. However $rose(valid) is true at T:15 before $rose(idle)
// Should result in Vacuous Pass or disabling of the check
x_delay <= 2 ;
@(posedge clk) valid <= 0 ; // T:14
@(posedge clk); idle <= 1 ; // T:24
// `endif
repeat(5) @(posedge clk);
#2; $finish();
end
endmodule
See waveforms and comments in the following images
