hi,
what is the proper way to assert number of times a signal(s1) changes (either rise or fall) in a time interval (end indicated by rise of signal s2);in a formal environment.
In reply to Veeresh_vs:
What are the requirements? Sig “a” shall change values “n” times between sig “b” and sig “c”.
Is “n” a constant or the value of a variable?
Once the requirements are defined, you can write an assertion in SVA or SV, see my verification Horizons paper (in latest issue)
Hint : use local variable as counter.
Ben systemverilog.us
In reply to ben@SystemVerilog.us:
Here is a potential solution, assuming “n” is a constant at elaboration time.
import uvm_pkg::*; `include "uvm_macros.svh"
module top;
timeunit 1ns; timeprecision 100ps;
bit clk, a, b, c;
let n=4;
default clocking @(posedge clk); endclocking
initial forever #10 clk=!clk;
// Sig "a" shall change values "n" times between sig "b" and sig "c".
ap_abc: assert property( $rose(b) |-> $changed(a)[=n] intersect c [->1]);
// Sig "a" shall ==1 values "n" times between sig "b" and sig "c".
ap_abc2: assert property( $rose(b) |-> a[=n] intersect c [->1]);
initial begin
repeat(200) begin
@(posedge clk);
if (!randomize(a, b, c) with
{ a dist {1'b1:=1, 1'b0:=2};
b dist {1'b1:=1, 1'b0:=6};
c dist {1'b1:=1, 1'b0:=10};
}) `uvm_error("MYERR", "This is a randomize error")
end
$stop;
end
endmodule
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- 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
- 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
See Paper: VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
In reply to ben@SystemVerilog.us:
hi Ben, thanks for the reply.
to clarify… currently i’am assuming ‘n’ to be constant value assigned to a register ;this need to be sampled and assert that s1 has to rise n times within event s2.
In reply to Veeresh_vs:
OK, here is quite a dump of options; you’ll need to analyze those and explore what is correct for you. At the bottom is the total code with a testbench. Below are specific snippets with comments.
// This assertion seems to meet your requirements with the exception that I am using sig c
// instead of an event e
property abc;
int v;
($rose(b), v=n) |-> first_match(
(($changed(a)[=1], v=v-1'b1, $display("%t v_thrd1= %d", $time, v) )[*0:$] ##1 v<=0))
intersect c [->1];
endproperty
ap_abc: assert property(abc);
// The event cause complications because with the ANDing of the 2 threads,
// there is a separate local variable for each thread
property abe; // DOES NOT WORK, DO NOT USE
int v;
($rose(b), v=n) |-> first_match(
(($changed(a)[=1], v=v-1'b1, $display("%t v_thrd1= %d",$time, v) )[*0:$] ##1 v<=0))
// intersect c [->1];
and @e (1, $display("%t v_thrd2= %d", $time, v)) ##0 v<=0;
// NOT THE SAME V, BUT A DIFFERENT COPY
endproperty
// You could create a signal d out of the event e, and use something
// like the top assertion
always @e begin
d<=1'b1;
@(posedge clk) d <= 1'b0;
end
property abe_d;
int v;
($rose(b), v=n) |-> first_match(
(($changed(a)[=1], v=v-1'b1, $display("%t v_thrd1= %d", $time, v) )[*0:$] ##1 v<=0))
intersect d [->1];
endproperty
ap_abe_d: assert property(abe_d);
// Another possibility is to use tasks, as explained in my paper
// https://verificationacademy.com/forums/systemverilog/vf-horizonspaper-sva-alternative-complex-assertions
// Formal tools don't handle this approach.
task automatic t_abe();
automatic int v;
fork
fork1: begin //: th1
if($rose(b)) v=n;
else disable t_abe; //disable fork1;
forever begin : fv1
if ($changed(a)) v=v-1'b1;
@(posedge clk);
end : fv1
end //: th1
fork2: begin //: th2
if(!$rose(b)) disable t_abe; // disable fork2;
@e assert(v==0);
$display("%t v_task= %d", $time, v);
if(v==0) -> ep; else -> ef;
disable t_abe;
//disable fork1;
//disable fork2; // return is illegal here
end //: th2
join
endtask
always @(posedge clk) begin
t_abe();
end
// the testbench
import uvm_pkg::*; `include "uvm_macros.svh"
module top;
timeunit 1ns; timeprecision 100ps;
bit clk, a, b, c, d;
event e, ep, ef;
int n=3;
default clocking @(posedge clk); endclocking
initial forever #10 clk=!clk;
// to clarify.. currently i'am assuming 'n' to be constant value assigned to a register;
//this need to be sampled and assert that s1 has to rise n times within event s2.
// // Sig "a" shall change values "n" times between sig "b" and sig "c".
property abc;
int v;
($rose(b), v=n) |-> first_match(
(($changed(a)[=1], v=v-1'b1, $display("%t v_thrd1= %d", $time, v) )[*0:$] ##1 v<=0))
intersect c [->1];
endproperty
ap_abc: assert property(abc);
property abe_d;
int v;
($rose(b), v=n) |-> first_match(
(($changed(a)[=1], v=v-1'b1, $display("%t v_thrd1= %d", $time, v) )[*0:$] ##1 v<=0))
intersect d [->1];
endproperty
ap_abe_d: assert property(abe_d);
property abe; // DOES NOT WORK, DO NOT USE
int v;
($rose(b), v=n) |-> first_match(
(($changed(a)[=1], v=v-1'b1, $display("%t v_thrd1= %d",$time, v) )[*0:$] ##1 v<=0))
// intersect c [->1];
and @e (1, $display("%t v_thrd2= %d", $time, v)) ##0 v<=0;
// NOT THE SAME V, BUT A DIFFERENT COPY
endproperty
ap_abe: assert property(abe);
always_ff @(posedge clk) begin
if(c) ->e;
end
always @e begin
d<=1'b1;
@(posedge clk) d <= 1'b0;
end
task automatic t_abe();
automatic int v;
fork
fork1: begin //: th1
if($rose(b)) v=n;
else disable t_abe; //disable fork1;
forever begin : fv1
if ($changed(a)) v=v-1'b1;
@(posedge clk);
end : fv1
end //: th1
fork2: begin //: th2
if(!$rose(b)) disable t_abe; // disable fork2;
@e assert(v==0);
$display("%t v_task= %d", $time, v);
if(v==0) -> ep; else -> ef;
disable t_abe;
//disable fork1;
//disable fork2; // return is illegal here
end //: th2
join
endtask
always @(posedge clk) begin
t_abe();
end
/* property testv;
int v;
@(posedge clk) (1, v=7) |=> ##1 (1, $display("v_thrd1= %d", v)) or
(1, $display("v_thrd2= %d", v)) ##2 1;
endproperty
ap_testv: assert property(testv);
// Sig "a" shall change values "n" times between sig "b" and sig "c".
ap_abc: assert property( $rose(b) |-> $changed(a)[=n] intersect c [->1]);
// Sig "a" shall ==1 values "n" times between sig "b" and sig "c".
ap_abc2: assert property( $rose(b) |-> a[=n] intersect c [->1]); */
initial begin
repeat(10000) begin
@(posedge clk);
if (!randomize(a, b, c) with
{ a dist {1'b1:=1, 1'b0:=2};
b dist {1'b1:=1, 1'b0:=6};
c dist {1'b1:=1, 1'b0:=9};
}) `uvm_error("MYERR", "This is a randomize error")
end
$stop;
end
endmodule
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- 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
- 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
See Paper: VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
In reply to ben@SystemVerilog.us:
Not sure if disable of task name disables all running tasks by that name, rather than the individual one. Of so, use
// disable t_abe; // mo
disable fork1;
disable fork2;
Ben Ben@systemverilog.us
In reply to Veeresh_vs:
Since you mentioned formal - your best bet is to write an always block and implement that counter.
Then use an assertion around that counter
Regards
Srini