I’m trying to code an assertion that when go == 1 (from 0->1) or
when go ==1 (for more than 1 clock) data is held until is checked later when ready==1.
Maybe I shouldn’t create an assertion this way or choose a better control signal.
Could I modify the sva coding to handle this go condition?
property abc ;
logic [WIDTH-1:0] v;
@(posedge clk) disable iff (rst)
(go, v = data) |=> ##[1:$] (ready ==1) ##0 (out == v) );
endproperty
assert_abc_check : assert property (abc)
$info ("@%0d ns : PASS : out = %h , data = %h" , $time, out, data);
else
$info ("@%0d ns : FAIL : out = %h", $time, out);
There are several problems with the way you wrote the property
- Multithreading and data capture When you write (go, v = data) |=> …
At every clocking event go==1 you save into v the value of data. This creates multiple threads. That means that if @cycle1 go==1, and data==5, and then @cycle 2 go==1 and data==7, then what your property is expressing is that at some points in the future (e.g., @ cycle 20 ready==1 && out== 5 (or 7), and then some cycle(s) later (e.g., @cycle30) ready is again ==1, and out == 7 (or 5 if out was 7 @cyle 20). If you are not looking for the first occurrence of go then I would use the $rose; thus ($rose(go), v = data) |=> …[ - Uniqueness This is *exclusivity or uniqueness of each attempted thread sequences).*I explain this issue in my SVA Handbook 4th Edition, I also addressed that topic at
Counting number of events on clock a, while clock o is forbidden - SystemVerilog - Verification Academy
Hint: use the module variables int ticket, now_serving; - **|=> ##[1:] (ready ==1)** This property can **never be false** because of the ##(1:) because if the ending conditions are false, the simulator will keep on checking for naother possible success. Also, Why the |=> ##(1:… ? |=> is same as 1’b1 ##1 |->
I would rewire that property as
property abc ;
logic [WIDTH-1:0] v;
@(posedge clk) disable iff (rst)
($rose(go), v = data) |->
first_match(##[:$] (ready ==1)) ##0 (out == v) );
endproperty
// May prefer this instead
($rose(go), v = data) |->
ready[->1] ##0 (out == v) ); // OK too
- For your info and error displays, I would use UVM messaging. Examples, from my book.
import uvm_pkg::*; `include "uvm_macros.svh"
module uvm_sva_ex; // /ch4/4.2/uvm_sva_ex.sv
bit clk, a, b, c, req, ack;
parameter CLK_HPERIOD = 10;
string tID="UART ";
initial begin : clk_gen forever #CLK_HPERIOD clk <= !clk; end : clk_gen
default clocking def_cb @ (posedge clk); endclocking : def_cb
ap_FULL: assert property(a) else
`uvm_info(tID,$sformatf("%m : error in a %b", a), UVM_FULL); // Line 15
ap_test2: assert property(a) else
`uvm_error(tID,$sformatf("%m : error in a %b", a)); // Line 17
- Value of local variable in messaging: If you want this, you need to write a function. See
Is there a way to use SVA property's local variable value to be used outside property - SystemVerilog - Verification Academy
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