SVA and clock domain crossing

SystemVerilog
, , , ,
1

Hi,

Background: I am trying to verify my fully asynchronous FIFO using SVA. The read clock domain can indicate that the FIFO is empty and the write clock domain can indicate that the FIFO is full. My design allows the circuit to indicate that it is both empty and full for the time that it takes to synchronize a signal from one domain to another, this takes two (receiving domain) clock cycles. Thus the FIFO can indicate that it is both full and empty from posedge ckA to two posedge ckB later. My trouble is in allowing this using SVA. The code I am using now is:


  property pr_ifAnotBstable(a, b, ckA, ckB);
     disable iff(arstWrite | arstRead) 
     @(posedge ckA) $rose(a) |->
     @(posedge ckB) ##1 !b;
  endproperty

This causes the assertion to sample rose on ckA, then wait one ckA, then wait two ckB before asserting the statement. What i want is: sample rose on ckA, then wait two ckB before asserting the statement. How can I do this?

Side note: I have tried with |=> and |-> ##1 (clock handovers), but this changes nothing. From Doulos’ documentation[1] it seems to me that I am doing this correctly, but that Questasim has a different definition of how this should be handled. When I try using |-> ##3 (which is supposed to be an illegal assignment) it diligently waits three ckA. This is according to [1] wrong, but this is not really a problem.

I am using Questasim 10.2b.

[1] Figure 7, Asynchronous Behaviors Meet Their Match with SystemVerilog Assertions, Doug Smith, Doulos

2 
@(posedge ckA) $rose(a) |->
     @(posedge ckB) ##1 !b;

[Ben] this is equivalent to:

@(posedge ckA) $rose(a) |->
     @(posedge ckA) @(posedge ckB) ##1 !b;

This causes the assertion to sample rose on ckA, then wait one ckA, then wait two ckB before asserting the statement.

[Ben] NO. This causes the assertion to sample rose on ckA, then at next ckB b==0.

What i want is: sample rose on ckA, then wait two ckB before asserting the statement. How can I do this?

@(posedge ckA) $rose(a) |->
     @(posedge ckB) ##2 !b;

This causes the assertion to sample rose on ckA, then at second posedge of ckB b==0.

Ben Cohen http://www.systemverilog.us/

  • SystemVerilog Assertions Handbook, 3rd Edition, 2013
  • A Pragmatic Approach to VMM Adoption
  • Using PSL/SUGAR … 2nd Edition
  • Real Chip Design and Verification
  • Cmpt Design by Example
  • VHDL books
3

In reply to ben@SystemVerilog.us:

Thank you for your answer!

I don’t quite understand why


@(posedge ckA) $rose(a) |->
     @(posedge ckA) @(posedge ckB) ##1 !b;

produces “sample rose on ckA, then wait one ckB before asserting the statement”, and not “sample rose on ckA, wait posedge ckA. Then, at the next posedge of ckB, wait one more posedge of ckB before asserting the statement”. I would be grateful if you could elaborate.

As you say

@(posedge ckA) $rose(a) |->

does not produce a double ckA, I’ve been reading my waveforms all wrong and my problem lies elsewhere. The signal a rises at the clockedge of ckA and I suppose that because of the preponed sampling the $rose(a) does not fire before the next posedge. Although

@(posedge ckB) ##1 !b;

seems to produce a double ckB wait. The waveform below shows the assertion starting at the clock edge after I want it to. The green lines indicate what I want to happen. How can I move the start of the assertion?

ckA = ckRead, ckB = ckWrite, a = fifoEmpty, b=fifoFull

Produced by:


     @(posedge ckA) $rose(a) |->
     @(posedge ckB) ##1 !b;
4

In reply to henrsol:

My apologies, I made a mistake. 1800’2012, 16.13.1 Multiclocked sequences explains the process, which is confusing, I agree.

The single delay indicated by ##1
is understood to be from the end point of the first sequence, which occurs at a tick of the first clock, to the nearest strictly subsequent tick of the second clock, where the second sequence begins

That means, in your case, for

@(posedge ckA) $rose(a) |->
     @(posedge ckB) ##1 !b;

after the @(posedge ckA) $rose(a), you wait till the nearest (posedge ckB), and then after ##1 of (posedge ckB) signal b must be ==0.

If clk0 and clk1 are not identical, then the clocking event for the sequence changes after ##1. If clk0 and clk1 are identical, then the clocking event does not change after ##1, and the above sequence is equivalent to the singly clocked sequence @(posedge clk0) sig0 ##1 sig1

In that case after the @(posedge ckA) $rose(a), since the nearest (posedge ckB) is 0( there is no wait), and then after ##1 of (posedge ckB) signal b must be ==0.

The zero delay
indicated by ##0 is understood to be from the end point of the first sequence, which occurs at a tick of the first clock, to the nearest possibly overlapping tick of the second clock, where the second sequence begins.

That means, in your case, for

@(posedge ckA) $rose(a) |->
     @(posedge ckB) ##0 !b;

after the @(posedge ckA) $rose(a), you wait till the nearest (posedge ckB), and then signal b must be ==0. If the clocks are identical (at that edge), then after the @(posedge ckA) $rose(a), NO wait, signal b must be ==0. Below are models I created.

1105×663 56.3 KB

http://SystemVerilog.us/mclk2.sv

1105×663 56.3 KB

http://SystemVerilog.us/mclk3.png
http://SystemVerilog.us/mclk3.sv

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
5

In reply to ben@SystemVerilog.us:

Thank you! I think 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:


logic ckWriteDel, ckReadDel;
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");

Not pretty, nor particularly clever. But I believe it works for my case.

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
7

In reply to ben@SystemVerilog.us:

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

Seeing as the two clocks are asynchronous I needed to check that b would be low two ckB cycles after a rose on the ckA edge. Therefore, I needed to move the sampling of a in $rose(a) to a scheduling region after ‘Observed’, so that I could evaluate the change when it happens and not on the next ckA edge(possibly very slow relative to ckB). Failing to do this in some clever way, I merely moved the checking edge until after the change had resolved itself, while making sure that I also wanted to move the checking of the ckB events.

Thank you for your kind advice.

The property is used twice, as_ifFullNotEmpty and as_ifEmptyNotFull.

I have been feeling the lack of a proper way of reporting(my last project involved UVM), and I hadn’t thought to use only the reporting part of UVM. Does adding the whole UVM package, to an otherwise simple testbench, add any unwanted overhead? Is there a particular subset that one could import?

If you don’t mind, I’ll slip in another question: What are your thoughts on the necessity of the cover property statement. Questa seems to be able to count the number of activations of an assertion when this option(-assertion_debug?) is set, but this doesn’t seem as “loud” as a cover property. Right now I am doing it like this:


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

cv_ifEmptyNotFull: cover property 
  (pr_ifAnotBstable(fifoEmpty, fifoFull, ckReadDel, ckWriteDel));

/Henrik

8

In reply to henrsol:

The property is used twice, as_ifFullNotEmpty and as_ifEmptyNotFull.

This is a personal preference, but inline assertions (instead of using properties with arguments) are easier to read, and review. That assertion is not that complex that it calls for using arguments, an opinion, of course.

I hadn’t thought to use only the reporting part of UVM. Does adding the whole UVM package, to an otherwise simple testbench, add any unwanted overhead? Is there a particular subset that one could import?

I am not a software developer, but UVM is just a set of libraries and routines. When the simulator includes it, I presume that it occupies memory. I just did a test of that model with and without UVM package, and I saw a difference of about 70 MB on my PC. The simulation slowdown would be when calling the routines. I don’t believe that `uvm_error is much work intensive than a $display; you most likely would not see it.

on the necessity of the cover property statement

The cover statement for properties is not needed since Questa gives you the same info anyway.
The results of coverage statement for a property contain:
 Number of times attempted
 Number of times succeeded
 Number of times succeeded because of vacuity

However, the cover sequence is useful to insure that you covered enough test sequences, for example
cv_full_and_push: cover sequence(@(posedge clk) first_match(fifo_full ##[1:$] push));
Results of coverage for a sequence include:
 Number of times attempted
 Number of times matched (each attempt can generate multiple matches). In addition, statement_or_null gets executed for every match. If there are multiple matches at the same time, the statement gets executed multiple times, one for each match.
Ben

9

In reply to ben@SystemVerilog.us:

This may be of use (OR it may not)…I have spent a lot of time looking of models of SVA with CDC on line and I found very few solutions that really covered all the corner conditions. There was one paper in 09 that was very well done but the SVA for CDC was just part of the whole. So I set put the following paper together to document SVA for CDC. Below is the link to the paper and the slides. Hopefully this can add some additional light on your issues.

The Trick is to find a solution that works for both RTL and GLS. Id you want to skip all the work up to the solution go to SLIDE 15. Unfortunately, the slides came after the paper so there were a little extra improvements shown there.

LCDM-ENG (DVCon15)
http://lcdm-eng.com/papers/DVCon%202015%20Assertions%20for%20CDC_Final_Slides.pdf

dm