Hi All,
I am writing assume property for FPV. My requirement is, i have input A and B and out C of the design.Lets say A as start pulse and B as end pulse.
I need to construct assume property and the requirement is whenever C is asserted from DUT, I would like to assert A followed by B and expect C to be asserted throughout this window.
A and B will be a single cycle pulse.
A and B can appear in same cycle or few cycles apart.
Expect only one pair of A followed B when C is asserted. Next set of A and B can appear only when rise of C.
I wrote following assume properties
Sequence S1 - $rose(A)|=>$fall(A)
That is NOT a sequence, it is a property
Below is code that I believe expresses what you need. You can change the weights of the distribution to get closer to your environment.
import uvm_pkg::*; `include "uvm_macros.svh"
module abc;
bit clk, a, b, c;
initial forever #10 clk=!clk;
ap_abc : assume property(@(posedge clk)
$rose(c) |=> c throughout a ##[0:$] b );
// The assume below needs to be analyzed for accuracy per the requirements
ap_noA_beforeB2: assume property(@(posedge clk)
$rose(c) |=> not(b ##1 a[->1])); // Is this what is desired?
ap_noA_beforeB: assume property(@(posedge clk)
$rose(c) |=> not(b ##1 !a[->1]));
initial begin
repeat(200) begin
@(posedge clk);
if (!randomize(a, b, c) with
{ a dist {1'b1:=1, 1'b0:=1};
b dist {1'b1:=1, 1'b0:=1};
c dist {1'b1:=4, 1'b0:=1};
}) `uvm_error("MYERR", "This is a randomize error")
end
$finish;
end
endmodule
Thanks Ben for the code. I have updated my sequence and properties as below as per my requirement. I would like to see one pulse of a followed by b whenever c is asserted. But somehow i see 2 pulse of a sometimes and 1 b. Any suggestion to avoid this extra pulse?
// The problem with
property P1;
@(posedge clk) disable iff(~rst_n) $rose(c) |=>c throughout ((s_a and (##[0:$] s_b)));
endproperty
property P2;
// which is same as
property P1;
@(posedge clk) disable iff(~rst_n) $rose(c) |=>c throughout
(($rose(a) ##1 $fell(a)) and (##[0:$] $rose(b) ##1 $fell(b))));
endproperty
property P2;
// with this definition : ##[0:$] $rose(b) ##1 $fell(b
// A sequence like ($rose(a) && !b) fails the ##[0:$] $rose(b) ##1 $fell(b,
// and thus, you wait for another ## cycle until ##[0:$] $rose(b) ##1 $fell(b occurs
Try something like this
import uvm_pkg::*; `include "uvm_macros.svh"
module abc;
bit clk, a, b, c;
initial forever #10 clk=!clk;
sequence s_a; $rose(a) ##1 $fell(a); endsequence
sequence s_b; $rose(b) ##1 $fell(b); endsequence
ap_abc : assume property(@(posedge clk)
$rose(c) |=> c throughout $rose(a) ##1 (!a && !b)[*0:$] ##1 !a && $rose(b) );
ap_a1pulse: assume property (@(posedge clk)
$rose(a) |=> $fell(a));
ap_b1pulse: assume property (@(posedge clk)
$rose(b) |=> $fell(b));
ap_noA_beforeB: assume property(@(posedge clk)
$rose(c) |=> (a && !b[->1] ##0 b[->1]) or (a && b[->1]));
ap_noA_beforeB2: assume property(@(posedge clk)
$rose(c) |=> not(b ##1 a[->1]));
initial begin
repeat(200) begin
@(posedge clk);
#2 if (!randomize(a, b, c) with
{ a dist {1'b1:=1, 1'b0:=2};
b dist {1'b1:=1, 1'b0:=2};
c dist {1'b1:=5, 1'b0:=1};
}) `uvm_error("MYERR", "This is a randomize error")
end
$finish;
end
endmodule
In my book SystemVerilog Assertions Handbook 4th Edition I have a chapter dedicated to the verification of assertions. I presume that since you a formal verification tool, you most likely use that to test your assertions, else, you can use simulation.
Ben Cohen http://www.systemverilog.us/ben@systemverilog.us
SystemVerilog Assertions Handbook 4th Edition, 2016 ISBN 978-1518681448
A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
Component Design by Example ", 2001 ISBN 0-9705394-0-1
VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115