/* Ben Cohen Dec 7, 2021 http://www.systemverilog.us/ ben@systemverilog.us */ // This file includes the delay and repeat package along with // a testbench to demonstrate its application. // The package was verified through analysis of the sequences and through random testing // Sequences that use the first_match() function along with a range repeat were reported // not compatible with formal verification tools package sva_delay_repeat_range_pkg; //---------------------------------------------------------------- // ****** DYNAMIC DELAY ##d1 ********** // Implements ##[d1] // Application: sq_1 ##0 dynamic_delay(d1) ##0 sq_2; sequence dynamic_delay(count); int v; (count<=0) or ((1, v=count) ##0 (v>0, v=v-1) [*0:$] ##1 v<=0); endsequence // dynamic_delay //---------------------------------------------------------------- // ****** DYNAMIC DELAY RANGE ##[d1:d2] ********** // Implements ##[d1:d2] ##0 a_sequence // for use in consequent // Application: $rose(a) |-> dynamic_delay_lohi_sq(d1, d2, q) ; sequence dynamic_delay_lohi_sq(d1, d2, sq); int v1, vdiff; ( (1, v1=d1, vdiff=d2-d1) ##0 dynamic_delay(v1) ##0 (vdiff>=0, vdiff=vdiff - 1)[*1:$] ##0 sq); endsequence sequence dynamic_delay_fm_lohi_sq(d1, d2, sq); int v1, vdiff; first_match( (1, v1=d1, vdiff=d2-d1) ##0 dynamic_delay(v1) ##0 (vdiff>=0, vdiff=vdiff - 1)[*1:$] ##0 sq); endsequence // dynamic_delay_fm_lohi_sq //---------------------------------------------------------------- // ****** 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)." //---------------------------------------------------------------- // ****** DYNAMIC REPEAT RANGE sq_1[*range] ##1 b] ********** // Implements a_sequence[*1:range] b_sequence // Application: $rose(a) |-> sq1_rpt_simple_range_sq2(sq_1, d1, sq2_2); //NOTE: RANGE MUST BE GREATER THAN ZERO !!!!!! sequence sq1_rpt_simple_range_sq2(sq1, range, sq2); int v, diff; (range>0, diff=range) ##0 ((diff>0 ##0 sq1, diff=diff-1'b1) [*1:$] ##1 sq2); endsequence sequence sq1_rpt_simple_range_fm_sq2(sq1, range, sq2); int v, diff; (range>0, diff=range) ##0 first_match((diff>0 ##0 sq1, diff=diff-1'b1) [*1:$] ##1 sq2); endsequence //---------------------------------------------------------------- // ****** DYNAMIC REPEAT LO-HI RANGE ********** // Implements a_sequence[*lo:hi] ##1 b_sequence // Application: $rose(a)|-> sq1_rpt_lohi_sq2(sq_1, d1, d2, sq_2); sequence sq1_rpt_lohi_sq2(sq1, d1, d2, sq2); int v, diff; (1, v=d1-1, diff=d2-d1+1) ##0 sq_rpt_simple_count(sq1, v) ##1 // TBD Ben Srini q1_rpt_simple_range_q2(sq1, diff, sq2); sq1_rpt_simple_range_sq2(sq1, diff, sq2); endsequence // sq1_rpt_lohi_sq2 endpackage // sva_delay_repeat_range_pkg // ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ // +++++++++++++++++++ testbench +++++++++++++++++++++ import uvm_pkg::*; `include "uvm_macros.svh" import sva_delay_repeat_range_pkg::*; module top; timeunit 1ns; timeprecision 100ps; bit clk, a, b, c=1, w; int d1=2, d2=5, range=7; sequence sq_a1_2_b; a ##[1:2] b; endsequence sequence sq_c1_4_b; c ##[1:4] b; endsequence sequence sq_2w; ##2 w; endsequence // default clocking @(posedge clk); endclocking initial forever #5 clk=!clk; // ****** DYNAMIC DELAY ##d1 ********** ap_dyn_delay2: assert property(@ (posedge clk) $rose(a) |-> dynamic_delay(d1) ##0 sq_2w); ap_fix2_delay2: assert property(@ (posedge clk) $rose(a) |-> ##2 sq_2w); ap_dyn_delay0: assert property(@ (posedge clk) $rose(a) |-> dynamic_delay(1'b0) ##0 sq_2w); ap_fix_delay0: assert property(@ (posedge clk) $rose(a) |-> ##0 sq_2w); //---------------------------------------------------------------- // ****** DYNAMIC DELAY RANGE ##[d1:d2] ********** ap_dly_2_5_consequent_rng: assert property(@ (posedge clk) $rose(a) |-> dynamic_delay_lohi_sq(d1, d2, sq_c1_4_b)); ap_fix_2to5_consequent: assert property(@ (posedge clk) $rose(a) |-> ##[2:5] sq_c1_4_b ); ap_dly_rng_2_5_antc: assert property(@ (posedge clk) $rose(a) ##0 dynamic_delay_fm_lohi_sq(d1, d2, sq_c1_4_b) |-> sq_2w); ap_fix_2to5_antc: assert property(@ (posedge clk) first_match($rose(a) ##0 (##[2:5] sq_c1_4_b)) |-> sq_2w); //=== // The sub-sequence (vdiff>=0, vdiff=vdiff - 1)[*1:$] ##0 sq) // causes the display of the failure to occur 1 cycle later // when vdiff==0 and sq is a nomatch. // At next cycle, vdiff==-1 and the term vdiff>0 is false. // That's when the error is display (1 cycle laters) // The passes are displayed at the correct cycle. ap_dly_2to2_consequent_rng: assert property(@ (posedge clk) // ** FLAG, but OK $rose(a) |-> dynamic_delay_lohi_sq(d1, 2, sq_c1_4_b)); ap_fix_2to2_consequent: assert property(@ (posedge clk) $rose(a) |-> ##[2:2] sq_c1_4_b ); ap_dly_0to0_consequent_rng: assert property(@ (posedge clk) // ** FLAG, but OK $rose(a) |-> dynamic_delay_lohi_sq(0, 0, sq_c1_4_b)); ap_fix_0to0_consequent: assert property(@ (posedge clk) $rose(a) |-> ##[0:0] sq_c1_4_b ); //------------------------------------------------------------------ // ****** DYNAMIC REPEAT sq_a1_2_b[*d1] ********** ap_rpt_count_2_cons: assert property(@ (posedge clk) $rose(a)|-> sq_rpt_simple_count(sq_a1_2_b, d1) ##1 sq_2w); ap_rpt_2_fix_cons: assert property(@ (posedge clk) $rose(a)|-> sq_a1_2_b[*2] ##1 sq_2w); ap_rpt_count_2_antc: assert property(@ (posedge clk) $rose(a) ##0 sq_rpt_simple_count(sq_a1_2_b, d1) |-> ##1 sq_2w); ap_rpt_2_fix_antc: assert property(@ (posedge clk) $rose(a) ##0 sq_a1_2_b[*2] |-> ##1 sq_2w); // ****** DYNAMIC REPEAT RANGE sq_1[*rang] ##1 b] ********** ap_rpt_rng2_5_antc_all: assert property(@ (posedge clk) $rose(a) ##1 sq1_rpt_simple_range_sq2(sq_a1_2_b, range, sq_c1_4_b) |-> sq_2w); ap_rpt_fix2_5_antc_all: assert property(@ (posedge clk) $rose(a) ##1 (sq_a1_2_b[*1:7] ##1 sq_c1_4_b) |-> sq_2w); ap_rpt_rng2_5_cons: assert property(@ (posedge clk) $rose(a) |-> ##1 sq1_rpt_simple_range_sq2(sq_a1_2_b, range, sq_c1_4_b)); ap_rpt_fix2_5_cons: assert property(@ (posedge clk) $rose(a) |-> ##1 (sq_a1_2_b[*1:7] ##1 sq_c1_4_b)); // first_match() ap_rpt_rng2_5_cons_all_fm: assert property(@ (posedge clk) $rose(a) |-> sq1_rpt_simple_range_fm_sq2(sq_a1_2_b, range, sq_c1_4_b) ##0 sq_2w); ap_rpt_range_fix2_5_cons_fm: assert property(@ (posedge clk) $rose(a) |-> first_match(sq_a1_2_b[*1:7] ##1 sq_c1_4_b) ##0 sq_2w); ap_rpt_rng2_5_antc_fm: assert property(@ (posedge clk) sq1_rpt_simple_range_fm_sq2(sq_a1_2_b, range, sq_c1_4_b) |-> a ); ap_rpt_rng2_5_antc_fm_sequence: assert property(@ (posedge clk) // *** first_match(sq1_rpt_simple_range_sq2(sq_a1_2_b, range, sq_c1_4_b)) |-> a); ap_rpt_fix2_5_antc_fm: assert property(@ (posedge clk) first_match( (sq_a1_2_b[*1:7] ##1 sq_c1_4_b)) |-> a); initial begin repeat(2) @(posedge clk); a <= 1'b0; b<=1'b0; c<=1'b0; w<=1'b0; @(posedge clk); a <= 1'b1; b<=1'b1; c<=1'b1; w<=1'b1; repeat(20) @(posedge clk); repeat(1000) begin @(posedge clk); #2; if (!randomize(a, b, c, w) with { a dist {1'b1:=1, 1'b0:=1}; b dist {1'b1:=1, 1'b0:=1}; c dist {1'b1:=1, 1'b0:=1}; w dist {1'b1:=1, 1'b0:=1}; }) `uvm_error("MYERR", "randomize error"); end #1; repeat(1500) begin @(posedge clk); #2; if (!randomize(a, b, c, w) with { a dist {1'b1:=1, 1'b0:=2}; b dist {1'b1:=3, 1'b0:=2}; c dist {1'b1:=1, 1'b0:=1}; w dist {1'b1:=3, 1'b0:=1}; }) `uvm_error("MYERR", "randomize error"); end repeat(1500) begin @(posedge clk); #2; if (!randomize(a, b, c, w) with { a dist {1'b1:=2, 1'b0:=1}; b dist {1'b1:=1, 1'b0:=2}; c dist {1'b1:=4, 1'b0:=1}; w dist {1'b1:=2, 1'b0:=1}; }) `uvm_error("MYERR", "randomize error"); end $stop; end endmodule