I wanted to write an assertion to check the “out” signal follows the “in” signal when “dat” is equal to check. Both “in” and “out” are not synchronous to the “clk” .The only condition is it should ignore the pulse while “dat” is changing from no check to check and vice versa as I highlighted with the red ink .
Thanks
In reply to DChal:
You can use the following as a baseline. Note that as long as dat==ccheck, “a” must follow “b”.
See the notes on my assumptions.
module top;
timeunit 1ns / 100ps;
`include "uvm_macros.svh"
import uvm_pkg::*;
bit clk, a, b, dis;
int dat, check;
initial forever #10 clk = !clk;
// There is a need to define which time zone to reject.
// For this model, I am assuming that the zone to rejet is 3ns
// after dat!check
// During check, "b" must follow "a" within 2ns
// Am assuming that "a" occurs first ar at the same time as "b"
always begin
@(dat != check) begin
dis=1'b1;
#3;
dis=1'b0;
end
end
property p_ab;
realtime t;
disable iff(dis)
@(a) (check==dat, t=$realtime) |-> @(b) $realtime-t <2ns && $realtime-t >=0;
endproperty
ap_ab: assert property(p_ab);
initial begin
repeat (200) begin
@(posedge clk);
if (!randomize(a, b, dat, check) with {
a dist {1'b1 := 1, 1'b0 := 1};
b dist {1'b1 := 1, 1'b0 := 2};
dat dist {2 := 1, 3 := 2};
check dist {2 := 1, 3:= 1};
})
`uvm_error("MYERR", "This is a randomize error");
end
$finish;
end
endmodule
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
In reply to ben@SystemVerilog.us:
Hi Ben ,
Thanks for replying , I understand that your solution accounts for the pulse rejection when dat is changing from no-check to check , but the other case is it changing from check to no-check which is the second red marker the image.
How can I handle that case ? May be I misunderstood you answer .
Thanks
In reply to DChal:
This model is an improvement, but it still has issues.
module top;
timeunit 1ns / 100ps;
`include "uvm_macros.svh"
import uvm_pkg::*;
bit clk, a, b, dis, check_mode;
int dat, check;
initial forever #3 clk = !clk;
// There is a need to define which time zone to reject.
// For this model, I am assuming that the zone to rejet is 3ns
// after dat!check
// During check, "b" must follow "a" within 2ns
// Am assuming that "a" occurs first ar at the same time as "b"
// Extending the property by 1 or 2 or @(posedge clk) with
// ##1 @(posedge clk) 1'b1 ##1 @(posedge clk) 1'b1;
// allows a disable to occur if (dat != check) soon after
always begin
@(dat != check) begin
dis=1'b1;
#3;
dis=1'b0;
end
end
always_comb check_mode= (dat == check);
property p_ab_pos;
realtime t;
disable iff(dis)
@(posedge a) (check==dat, t=$realtime) |-> @(posedge b) $realtime-t <2ns && $realtime-t >=0
##1 @(clk) 1'b1; // ##1 @(clk) 1'b1;
endproperty
ap_ab_pos: assert property(p_ab_pos);
property p_ab_neg;
realtime t;
disable iff(dis)
@(negedge a) (check==dat, t=$realtime) |-> @(negedge b) $realtime-t <2ns && $realtime-t >=0
##1 @(clk) 1'b1; // ##1 @( clk) 1'b1;
endproperty
ap_ab_neg: assert property(p_ab_neg);
initial begin
repeat (200) begin
repeat(2) @(posedge clk);
if (!randomize(a, b, dat, check) with {
a dist {1'b1 := 1, 1'b0 := 1};
b dist {1'b1 := 1, 1'b0 := 2};
dat dist {2 := 1, 3 := 5};
check dist {2 := 1, 3:= 7};
})
`uvm_error("MYERR", "This is a randomize error");
end
$finish;
end
endmodule
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
Thank you Ben , will try something similar !
In reply to DChal:
A second update that addresses the value of “b” follows “a”. The previous answer addressed the transitions but the values. Note that it can be solved with one assertion using the @(a), @(b) instead of the @(posedge a), @(posedge b).
module top;
timeunit 1ns / 100ps;
`include "uvm_macros.svh"
import uvm_pkg::*;
bit clk, a, b, dis, check_mode;
int dat, check;
initial forever #3 clk = !clk;
// There is a need to define which time zone to reject.
// For this model, I am assuming that the zone to rejet is 3ns
// after dat!check
// During check, "b" must follow "a" within 2ns
// Am assuming that "a" occurs first ar at the same time as "b"
// Extending the property by 1 or 2 or @(posedge clk) with
// ##1 @(posedge clk) 1'b1 ##1 @(posedge clk) 1'b1;
// allows a disable to occur if (dat != check) soon after
always begin
@(dat != check) begin
dis=1'b1;
#3;
dis=1'b0;
end
end
always_comb check_mode= (dat == check);
property p_ab_pos;
realtime t;
bit a_sampled;
disable iff(dis)
@(posedge a) (check==dat, t=$realtime, a_sampled=a) |-> //
@(posedge b) $realtime-t <2ns && $realtime-t >=0
##0 a_sampled==b // @(posedge b) the "b" is its sampled value
##1 @(clk) 1'b1; // ##1 @(clk) 1'b1;
endproperty
ap_ab_pos: assert property(p_ab_pos);
property p_ab_neg;
realtime t;
bit a_sampled;
disable iff(dis)
@(negedge a) (check==dat, t=$realtime, a_sampled=a) |->
@(negedge b) $realtime-t <2ns && $realtime-t >=0
##0 a_sampled==b // @(negedge b) the "b" is its sampled value
##1 @(clk) 1'b1; // ##1 @( clk) 1'b1;
endproperty
ap_ab_neg: assert property(p_ab_neg);
property p_ab_pos_neg;
realtime t;
bit a_sampled;
disable iff(dis)
@(a) (check==dat, t=$realtime, a_sampled=a) |-> //
@(b) $realtime-t <2ns && $realtime-t >=0
##0 a_sampled==b // @(b) the "b" is its sampled value
##1 @(clk) 1'b1; // ##1 @(clk) 1'b1;
endproperty
ap_ab_pos_neg: assert property(p_ab_pos);
initial begin
repeat (200) begin
repeat(2) @(posedge clk);
if (!randomize(a, b, dat, check) with {
a dist {1'b1 := 1, 1'b0 := 1};
b dist {1'b1 := 1, 1'b0 := 2};
dat dist {2 := 1, 3 := 5};
check dist {2 := 1, 3:= 7};
})
`uvm_error("MYERR", "This is a randomize error");
end
$finish;
end
endmodule
Ben