Systemverilog assertion

SystemVerilog
,
4

In reply to wangjiawen:
You’re correct, it’s really a matter of the requirements. As you know, a non-matched antecedent is a vacuous assertion.
Note: b[->1] is equivalent to: !b[*0:] ##1 b b[=1] is equivalent to: !b[*0:] ##1 b ##1 !b[*0:$]
If an antecedent is multithreaded, all threads must be tested with its corresponding consequent for success. b[->1] is single-threaded because it ends when b==1
b[=1] is multi-threaded because after b==1, there are other threads to be test (till infinity) for b==0. If in your case you want ONE “b” followed by ZEROs and ONE “c” followed by ZEROs until you match an intersect type of condition, then you’ll need a first_match() operator. See my example and the comments below:


/* signal A asserts for one cycle, then signal B asserts for one cycle and signal C
 asserts for one cycle(The problem here is: the order of B and C is arbitrary, 
 so we don't know when B and C will be asserted and who will be asserted first), 
 then signal D should asserts right after the latter one of B/C */
 module m;
	`include "uvm_macros.svh"
	import uvm_pkg::*;
    bit clk, a, b, c, d;
    initial forever #10 clk=!clk;  
    ap_abc: assert property(@(posedge clk) // A 2nd "b" could occur before a "c"
	      a ##1 (b[->1] and c[->1]) |-> d);  
    ap_abc2: assert property(@(posedge clk) 
              a ##1 (b[=1] and c[=1]) |-> d);  // MULTI_THREADED !!! 
    ap_abc3: assert property(@(posedge clk) 
	      first_match(a ##1 (b[=1] and c[=1])) |-> d);  // BETTER
                // vacuous if 2nd "b" occurs before a "c"
			 
	initial begin 
		repeat(200) begin 
			@(posedge clk);   
			if (!randomize(a, b, c, d)  with 
	     		{ a dist {1'b1:=1, 1'b0:=7};
				  b dist {1'b1:=1, 1'b0:=2}; 
				  c dist {1'b1:=1, 1'b0:=3};
				  d dist {1'b1:=1, 1'b0:=1};   
				}) `uvm_error("MYERR", "This is a randomize error");
			end 
			$finish; 
		end  
 endmodule : m

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers: