Have a basic RTL scenario where some signals need to be checked for condition, before checking for toggling of a particular signal within few cycles.
sequence phs_s;
$rose(ll) and (!ww) and (!pp) and (!rr);
endsequence: phs_s
sequence acs_s;
$rose(pp) and $stable(ww) and $stable(ll) and $stable(dd);
endsequence: acs_s
// Check If ee is released once within [single pulse for one cycle] next few cycles and with max of NCY.Once it reaches within, need to check
// if the count is set to default value.
property dd_rd_vd;
@(posedge clk) (phs_s ##1 acs_s) |=> (ee)[|->1] within ##[1:NCY] ##1 (count==0);
endproperty: delayed_chk
assert property (dd_rd_vd) else `uvm_error("ERR", "Assertion failed")
Is this syntactically correct and if so any other much simpler way ?
In reply to desperadorocks:
The sequence containment within specifies a sequence occurring within another sequence. Note: (seq1 within seq2) is equivalent to: ((1[*0:] ##1 seq1 ##1 1[*0:]) intersect seq2 )
You need
module top;
import uvm_pkg::*; `include "uvm_macros.svh"
import sva_delay_repeat_range_pkg::*;
bit clk, a, b, c=1, w;
int d1=2, d2=5, ncy=5;
sequence q_s;
a;
endsequence
initial forever #10 clk=!clk;
let NCY = 5; // NCY is a constant.
ap_FIXED: assert property(@(posedge clk) $rose(a) |=>
strong(b[->1] within 1'b1[*NCY] ##1 c==0));
//*** IF NCY is a variable then you could use my package
//*** SVA Package: Dynamic and range delays and repeats, See link below in my signature
// ****** DYNAMIC REPEAT q_s[*d1] **********
// Application: $rose(a) |-> q_dynamic_repeat(q_s, d1) ##1 my_sequence;
ap_DYNAMIC: assert property(@(posedge clk) $rose(a) |=>
strong(b[->1] within q_dynamic_repeat(1'b1, ncy) ##1 c==0));
// An occurrence of b within ncy cycles
// then at next cycle after ncy c==0
initial begin
repeat(100) 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(150) 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
$stop;
end
endmodule
Also, similarly wanted to check the opposite case i.e. the 2nd half shouldn’t happen, then check if the count is 0 and error is triggered. Can that be written as ?
In reply to desperadorocks:
The problem with the following is that the not(sequence) is a property
not((ee)[->1] within 1'b1[*NCY]) ##1 (count==0 && error == 1));
It is illegal to use the sequential operators (e.g., ##1) after a property. Thus,
A_property ##1 a_sequence // is illegal
// You could do the following instead
property dd_rd_vd;
@(posedge clk) (phs_s ##1 acs_s) |=>
not(ee[->1] within 1'b1[*NCY]) and
(1'b1[*NCY] ##1 count==0 && error == 1);
endproperty: not_delayed_chk
// the consequent is the ANDing of 2 properties
BTW, you have a tendency to use way too many (())
ee[->1] is more readable than (ee)[->1]
Same is true for count==0 && error == 1, no () needed.
**NOTE:**IEEE 1800-2009 provided the capability of defining a property that follows a sequence by zero or one cycle delay, starting from the end point of the sequence. This capability is introduced with the followed-by operators #-# ****and #=# that concatenates a sequence and a property. The followed-by operators are of the following forms for the definition of a property:
sequence_expr #-# property_expr // concatenation with zero cycle delay
sequence_expr #=# property_expr // concatenation with one cycle delay
The equivalence of sequence_expr #-# property_expr is defined as: [1]
not (sequence_expr |-> not property_expr)
and the equivalence of sequence_expr #=# property_expr is:
not (sequence_expr |=> not property_expr)