SVA and clock domain crossing

SystemVerilog
, , , ,
6

In reply to henrsol:

For reference I solved my $rose(a) firing later than I wanted it to with delaying my clocking edge by #1:

[Ben] Not sure as to why you needed to do this.

property pr_ifAnotBstable(a, b, ckA, ckB);
disable iff(arstWrite | arstRead) 
@(posedge ckA) $rose(a) |->
@(posedge ckB) ##1 !b;
endproperty
assert property 
(pr_ifAnotBstable(fifoEmpty, fifoFull, ckReadDel, ckWriteDel))
else $error("Assertion failed");

[Ben] I have a few comments on style:

  1. Creating properties with arguments is only needed if the properties are reused.
    Otherwise, just write the assertions directly, particularly if the properties do not have local variables. If the property declaration is not reused, do not add arguments. That creates more readable code. The way you have it, as a reader, I am forced to juggle my mind and do argument substitution to understand what the property does.
  2. Name your assertions. Thus,
ap_IfNotStable: assert property(
		disable iff(arstWrite | arstRead) 
		@(posedge ckReadDel) $rose(fifoEmpty) |->
		    @(posedge ckWriteDel) ##1 !fifoFull) else  
	         `uvm_error("FIFO", "Write on empty produced full");
  1. Use the UVM package. Below is a sample of the error messages"

Time: 66 ns Started: 50 ns Scope: async_fifo2 File: async_fifo2.sv Line: 18 Expr: ~fifoFull

UVM_ERROR async_fifo2.sv(25) @ 66: reporter [FIFO] Write on empty produced full

Below is a model that simulates.

import uvm_pkg::*;
`include "uvm_macros.svh"
module async_fifo2; 
  logic fifoEmpty=0, fifoFull=0, ckWrite=0, ckRead=0, ckReadDel, ckWriteDel;
  bit arstWrite, arstRead;
  //I understand a bit more, although asynchronous clocks produces a lot of hard cases for my assertions.
  //For reference I solved my $rose(a) firing later than I wanted it to with delaying my clocking edge by #1:
  assign #1 ckWriteDel = ckWrite;
  assign #1 ckReadDel = ckRead;
  property pr_ifAnotBstable(a, b, ckA, ckB);
	disable iff(arstWrite | arstRead) 
		@(posedge ckA) $rose(a) |->
		@(posedge ckB) ##1 !b;
  endproperty
 
  assert property 
	(pr_ifAnotBstable(fifoEmpty, fifoFull, ckReadDel, ckWriteDel))
		else $error("Assertion failed"); // Lin 18
	//Not pretty, nor particularly clever. But I believe it works for my case.
	
  ap_IfNotStable: assert property(
		disable iff(arstWrite | arstRead) 
		@(posedge ckReadDel) $rose(fifoEmpty) |->
		    @(posedge ckWriteDel) ##1 !fifoFull) else  
	         `uvm_error("FIFO", "Write on empty produced full"); // line 25
  
  initial forever #5 ckWrite=!ckWrite; 
  initial forever #7 ckRead=!ckRead; 
  
  always @(posedge ckWrite) begin 
  	#3;
  	if (!randomize(fifoEmpty, fifoFull))  `uvm_error("FIFO", "randomize error"); 
  end
 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