“Signal a is low, before next time signal a is asserted signal b may only rise for one clock cycle”
I know it can be easily tested with auxiliary code but I want to use just SVA to test it.
I was able to test for when b is high for only one clock cycle but the assertion fails if b is never asserted before next a.
property a_f;
@(posedge clk) disable iff(rst)
!a |=> ((b[=1]) ##1 !b[*0:$]) intersect (!a[*0:$] ##1 a) ;
endproperty
a1: assert property(a_f);
Thanks,
In reply to devil47:
property a_f;
@(posedge clk) disable iff(!rstn)
!a |=> ( ((b[=1]) ##1 !b[*0:$]) or (!b[*0:$]) ) intersect (!a[*0:$] ##1 a) ;
endproperty
a1: assert property(a_f);
In reply to Rahulkumar Patel:
In reply to Rahulkumar Patel:
In reply to devil47:
property a_f;
@(posedge clk) disable iff(!rstn)
!a |=> ( ((b[=1]) ##1 !b[*0:$]) or (!b[*0:$]) ) intersect (!a[*0:$] ##1 a) ;
endproperty
a1: assert property(a_f);
1) b[=1] is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$]
2) thus, ( ((b[=1]) ##1 !b[*0:$]) is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$] ##1 !b[*0:$]); also equivalent to
b[=1]
3) !a |=> ( ((b[=1]) ##1 !b[*0:$]) or (!b[*0:$]) ) intersect (!a[*0:$] ##1 a) ; // equivalent to
!a |=> ( b[=1] or (!b[*0:$]) ) intersect (!a[*0:$] ##1 a) ; // equivalent to
// b[=1] or (!b[*0:$] says an accurrance of b or no occurrence of b
// basically true at all cycles, like 1[*0:$]
4) !a |=> ( (1[*0:$]) ) intersect (!a[*0:$] ##1 a) // equivalent to
!a |=> a[->1] // equivalent to
$rose(a) |-> 1
Essentially,
!a |=> ( ((b[=1]) ##1 !b[*0:$]) or (!b[*0:$]) ) intersect (!a[*0:$] ##1 a) ;
gets reduced to
$rose(a)
requirements: “Signal a is low, before next time signal a is asserted signal b may only rise for one clock cycle”
$rose(b) |=> strong( a[->1] ##1 $rose(b)[->1]);
ap_b: assert property(@ (posedge clk) $rose(b) |=> !b );
initial
ap_a_IS_0_at_start: assert property(@ (posedge clk)
!a ##1 b[->1] ##1 !b ); // the very first occurrence
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr