HI
Need to write a assertion ::
1)Pulse 1 should be high for 10~100 clock cycles.
2)Pulse 2 Should be high within Pulse 1 for 1 clock cycle.Pulse 2 should occur only one time.
Please help on this.
Thanks
In reply to syed taahir ahmed:
Restating your requirements:
- Following the rise of “a”, “a” should be stable for 10 to 100 cycles.
- “a” represents an envelope in which a single pulse “b” should occur once.
initial
ap_b_in_a: assert property(@ (posedge clk)
$rose(a)[->1] |-> a[*10:100] intersect b[->1] ##1 b==0[*1:$]);
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
- 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 978-1539769712
- 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
- SVA Alternative for Complex Assertions
Verification Horizons - March 2018 Issue | Verification Academy - SVA: Package for dynamic and range delays and repeats | Verification Academy
- SVA in a UVM Class-based Environment
SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
In reply to ben@SystemVerilog.us:
Hi Ben,
Seems like the property not able to fail for the occurrence of pulse 2 twice in pulse 1, i replicated the scenario in Eda playground ,please have a look.
link:: Edit code - EDA Playground
Thanks
In reply to syed taahir ahmed:
The assertion reflects the requirements:
ref files : http://systemverilog.us/vf/pulses2c.sv
http://systemverilog.us/vf/pulses2c.png
// master_prop states that pulse1 extends between 10 and 100 cycles, and within that region,
// you have ONE occurrence of pulse2=1 and then pulse2==1 possibly being repeated 1 to $.
pulse1[*10:100] intersect( pulse2[->1] ##1 pulse2==0[*1:$])
// That property is ian intersection, thus, with pulse1==1 at all cycles within that range,
// once pulse2==1 and then pulse2=0, THAT intersection is complete and the assertion succeeds.
// All we asked here is that plse2 occurs within pulse1[*10:100] but not within pulse1[*100]
property master_prop;
@ (posedge clk)
disable iff (reset)
$rose(pulse1)[->1] |-> pulse1[*10:100] intersect( pulse2[->1] ##1 pulse2==0[*1:$]);
endproperty
//---------
// Now, what you may be looking for is that pulse1 holds (true) for 100 cycels
// and within that period pulse2 is a single pulse.
property master_prop2;
@ (posedge clk)
disable iff (reset)
$rose(pulse1)[->1] |-> pulse1[*100] intersect( pulse2[->1] ##1 pulse2==0[*1000]);
endproperty
//--------
// However, if you still want pulse1 to be the range 10:100, you could add another assertion
// that once pulse1 occurrs, there should s single pulse2 until pulse1 falls.
ap_continue: assert property(@ (posedge clk) $rose(pulse1)[->1] |->
$fell(pulse1)[->1] intersect(pulse2[->1] ##1 pulse2==0[*1:$]));
Assertions can be tricky! That is why you need to test the complex ones and really understand the meaning behind the syntax.
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
- 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 978-1539769712
- 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
- SVA Alternative for Complex Assertions
Verification Horizons - March 2018 Issue | Verification Academy - SVA: Package for dynamic and range delays and repeats | Verification Academy
- SVA in a UVM Class-based Environment
SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
How about this?
property p1;
$rose(Pulse1) |-> Pulse2[=1] within Pulse1[*10:100];
endproperty
In reply to devil47:
First off, let me correct some errors in my response:
- The following in INCORRECT
rose(pulse1)[->1] |-> pulse1[*10:100] intersect( pulse2[->1] ##1 pulse2==0[*1:]); // BAD
rose(pulse1) |-> pulse1[*10:100] intersect( pulse2[->1] ##1 pulse2==0[*0:]); // OK
$rose(pulse1) |-> pulse1[*10:100] intersect( pulse2[=1] ); // OK - Comments
$rose(pulse1)[->1] should be written as rose(pulse1) becuse the goto operator is meaningless here. b[->1] is equivalent to !b[*0:] ##1 b, thus causing unnecessary attempts. - b[=m] is equivalent to ( b [->m] ##1 !b [*0:$]
On your comments:
// You suggest
$rose(Pulse1) |-> Pulse2[=1] within Pulse1[*10:100];
// Note:
seq1 within seq2) is equivalent to: ((1[*0:$] ##1 seq1 ##1 1[*0:$]) intersect seq2 )
// Thus, your suggestion is equivalent to
$rose(Pulse1) |-> (1[*0:$] ##1 Pulse2[=1] ##1 1[*0:$]) intersect Pulse1[*10:100];
// That is also equivalent to
$rose(a) |->
a[*1:4] intersect( b[->1] ##1 b==0[*0:1000]) );
``` verilog
// Always tests your assertions
// The following model demonstrates that all 3 assertions are equivalent in simulation
module top;
timeunit 1ns/100ps;
`include "uvm_macros.svh"
import uvm_pkg::*;
bit clk, a, b;
default clocking @(posedge clk);
endclocking
initial forever #10 clk=!clk;
initial begin
$timeformat(-9, 1, "ns", 8);
$display("%t", $realtime);
end
ap_within: assert property(@ (posedge clk) $rose(a) |->
b[=1] within a[*1:4]);
ap_ab_eqv: assert property(@ (posedge clk) $rose(a) |->
(1[*0:$] ##1 b[=1] ##1 1[*0:$]) intersect a[*1:4]);
ap_ab1: assert property(@ (posedge clk)
$rose(a) |->
a[*1:4] intersect( b[->1] ##1 b==0[*0:1000]) );
initial begin
repeat(200) begin
@(posedge clk); ##1;
if (!randomize(a, b) with
{ a dist {1'b1:=5, 1'b0:=1};
b dist {1'b1:=1, 1'b0:=3};
}) `uvm_fatal("RAND", "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
- 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 978-1539769712
- 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
- SVA Alternative for Complex Assertions
Verification Horizons - March 2018 Issue | Verification Academy - SVA: Package for dynamic and range delays and repeats | Verification Academy
- SVA in a UVM Class-based Environment
SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy