Creating an assertion for an asynchronous input signal

I’m trying to craft an assertion that meets the following statement:

“If this asynchronous data signal input fell sometime in the last clock cycle AND remains low throughout the following clock cycle, then 2 cycles later the output must also be low”

the “AND remains low throughout the following clock cycle” part is what is stumping me.

I spoke with a coworker and his only thought was that as concurrent assertions run synchronously to a clock, the only way to check throughout a clock cycle for a value would be to have a second much faster clock and sample on that.

I suppose I could manufacture a fast clock to sample on, but as a solution it just seems ugly to me. Any thoughts on a better way to achieve what I’m trying to do?

Thanks!

In reply to silverace99:

You just need to create a little extra logic. I’m not exactly sure if this will meet your requirements, but it should get you started in the right direction.

always begin
       @(negedge signal)
       signal_low = 1;
       fork
          @(posedge signal) signal_low = 0;
          repeat(2) @(posedge clock);
       join_any
       disable fork;
      end

assert property(@(posedge clock) $fell(signal) ##1 signal_low |-> ##2 !my_output);

In reply to dave_59:
A few comments and a possible solution:

  1. Not all assertions need to use SVA. An assertion is a statement that a property holds, regardless of how you define that property
  2. See my paper on the SVA engine and how it can be emulated.
    PAPER: Understanding the SVA Engine + Simple alternate solutions - SystemVerilog - Verification Academy
    Abstract: Understanding the engine behind SVA provides not only a better appreciation and limitations of SVA, but in some situations provide features that cannot be simply implemented with the current definition of SVA. This paper first explains, by example, how a relatively simple assertion example can be written without SVA with the use of SystemVerilog tasks; this provides the basis for understanding the concepts of multithreading and exit of threads upon a condition, such as an error in the assertion. The paper then provides examples that uses computational variables within threads; those variables can cause, in some cases, errors in SVA. The strictly emulation model with tasks solves this issue.
  3. Using your description of the problem and my modeling approach in expressing assertions I came up with the model below

http://SystemVerilog.us/vf/asyn1.sv


// "If this asynchronous data signal input fell sometime in the last clock cycle
//  AND remains low throughout the following clock cycle, 
//   then 2 cycles later the output must also be low"
// the "AND remains low throughout the following clock cycle" part is what is stumping me. 

import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
	timeunit 1ns;     timeprecision 100ps;  
	bit clk, clk2,a, b;  // b is asynchronous 
	bit[2:0] t; // random delay
	event e, f, oke, okf; 
	default clocking @(posedge clk); endclocking
	initial forever #10 clk=!clk; 
	initial forever #3 clk2=!clk2; 
		
	task t_a(); 
		automatic bit b_unstable=0; 
		@(negedge b); 
		fork 
			@(posedge b) b_unstable=1; 
			repeat(1) @(posedge clk);  
		join_any
		a_b1: assert(b_unstable==0); // AND remains low throughout the following clock cycle, 
		if(b_unstable==1'b1) begin 
			->e;
			return;
		end
		repeat(2) @(posedge clk) a_b3: assert(b==0); // then 2 cycles later the output must also be low	
		if(b==1'b1)  ->f;
	endtask
 
	always  @(posedge clk)  begin // If this asynchronous data signal input fell sometime in the last clock cycle
		fork 
			t_a(); 
		join
	end 

	initial begin 
		repeat(200) begin 
			@(posedge clk2);   
			if (!randomize(t, a)  with 
					{ a dist {1'b1:=1, 1'b0:=1};
					{	t >=1};
					}) `uvm_error("MYERR", "This is a randomize error")
			#t b=a;
		end 
		$stop; 
	end 
endmodule   

Sim results:

** Error: Assertion error.

Time: 239 ns Scope: top.t_a.a_b1 File: async1.sv Line: 23

** Error: Assertion error.

Time: 310 ns Scope: top.t_a.a_b3 File: async1.sv Line: 28

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home


Thanks dave and ben for the responses! It’s exactly what I’m looking for.

It seems, as usual, better to handle complexities outside of the assertion rather than trying to make it do all the work.