In reply to run2prem:
you suggest to use SV rather than SVA for this particular check.
This is not necessarily true. What I am saying is:
- FOr very complex assertions an approach like the one I describe in my paper is often simpler; it is available at https://verificationacademy.com/news/verification-horizons-march-2018-issue
- That pure SV approach basically computes the antecedent and then fires automatic tasks for the consequent as threads. It overcomes some of the issues with local variables and provides more flexibility since you use the full power of SV. Typical code would look like:
always @ (posedge clk) begin
// local variable declations
// sequential statements (e.g., loops, @ (posedge clk), return, etc
if(vacuous_condition) return;
fork
task_emulating_the_consequent;
join_none
- Understanding the equivalent mechanics and limitations of SVA can help create a better SVA model.
Your code looks like it has the correct approach, but I have an issue with its correctness.
You are looking for the last write cycle. Assuming that that you load the register with 2, 3 or 4 consecutive writes, and WrAddr is an active ONE, then the last write would occur when
$fell(WrAddr_pre)&& WrAddr rather than your WrAddr != WrAddr_pre.
property data_integrity_check ();
logic [7:0]Addr;
logic [7:0] Data;
disable iff (~RG_ResetN)
@(posedge WrClk)
($fell(WrAddr_pre)&& WrAddr ), Addr = WrAddr, Data = WrData) |-> @(posedge RdClk) first_match (##[0:$] (RdEn && (RdAddr == Addr))) ##1 (RdData == Data);
endproperty:data_integrity_check
also
first_match (##[0:$] (RdEn && (RdAddr == Addr))) ##1 (RdData == Data); is equivalent to
(RdEn && RdAddr == Addr)[->1] ##1 (RdData == Data);
Test your assertions with a simple testbench. I use the following as a test template, then fill-in the details. That template is stored in an Autotext and Text Autocompletion in any application using the application available at no cost at https://www.phraseexpress.com/
import uvm_pkg::*; `include "uvm_macros.svh"
module top;
timeunit 1ns; timeprecision 100ps;
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
always @(posedge clk) begin
end
initial begin
bit va, vb;
repeat(200) begin
@(posedge clk);
if (!randomize(va, vb) with
{ va dist {1'b1:=1, 1'b0:=3};
vb dist {1'b1:=1, 1'b0:=2};
}) `uvm_error("MYERR", "This is a randomize error")
a <= va;
b <= vb;
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
- https://verificationacademy.com/news/verification-horizons-march-2018-issue
- http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
- “Using SVA for scoreboarding and TB designs”
http://systemverilog.us/papers/sva4scoreboarding.pdf - “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
https://verificationacademy.com/verification-horizons/october-2013-volume-9-issue-3 - SVA in a UVM Class-based Environment
https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment