property poreset_clock_check; // Poorly written assertion!!!
int v_t;
@(posedge clk) ($fell(PORESET_B),v_t=0) |->
(1, v_t=v_t+1)[*0:$] ##0 $rose(PORESET_B) |-> (v_t >= 32);
endproperty
ap_poreset_clock_check: assert property(poreset_clock_check);
There are several things wrong with the above assertion:
[list=1]
[*] (1, v_t=v_t+1)[*0:$] ##0 $rose(PORESET_B) includes an empty match.
Note: a[0] is an empty match, and
empty ##0 seq is a no match. The point is that this aspect of the property adds no meaning to the specification, and should be avoided.
Note that (empty ##1 seq) is same as (seq)
[] You cannot have a $fell(PORESET_B) and a rose(PORESET_B) in the same cycle, thus why use the |->? It is a confusing specification, and is meaningless.
**Avoid meaningless terms in an assertion**
[*] v is of type int, and adding a 1 to an int, though OK. However, if v were a vector (e.g., bit[4:0]) adding an integer 1 can lead to errors. I, general I prefer to use 1'b1.
See http://systemverilog.us/int_arith.pdf for an explanation of the error.
[*] The property of the form (x[*0:] ##1 z |-> w) must check ALL terms of the antecedent for it to succeed. Thus, you would need a first_match
Below is code that reflects the needed corrections.
import uvm_pkg::*;
`include "uvm_macros.svh"
module min;
bit clk, PORESET_B;
initial forever #5 clk=!clk;
property poreset_clock_check;
int v_t;
@(posedge clk) ($fell(PORESET_B),v_t=0) |=>
first_match( (1, v_t=v_t+1'b1)[*1:$] ##0 $rose(PORESET_B)) |-> (v_t >= 32);
endproperty
ap_poreset_clock_check: assert property(poreset_clock_check);
always @(posedge clk)
if (!randomize(PORESET_B) with {PORESET_B dist {1'b1:=5, 1'b0:=95};})
`uvm_error("MYERR", "This is a randomize error");
endmodule
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
- SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
- 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