Formal Assume Property

SystemVerilog
,
2

In reply to chipsofsilicon:

  1. Sequence S1 - $rose(A)|=>$fall(A)
    That is NOT a sequence, it is a property
  2. Below is code that I believe expresses what you need. You can change the weights of the distribution to get closer to your environment.

import uvm_pkg::*; `include "uvm_macros.svh" 
module abc;
	bit clk, a, b, c; 
	initial forever #10 clk=!clk;  
    ap_abc : assume property(@(posedge clk)
    		$rose(c) |=> c throughout a ##[0:$] b );  
    // The assume below needs to be analyzed for accuracy per the requirements 
    ap_noA_beforeB2: assume property(@(posedge clk)
    		$rose(c) |=> not(b ##1 a[->1]));   // Is this what is desired? 
    ap_noA_beforeB: assume property(@(posedge clk)
    		$rose(c) |=> not(b ##1 !a[->1]));  
	 initial begin 
     repeat(200) begin 
       @(posedge clk);   
       if (!randomize(a, b, c)  with 
           { a dist {1'b1:=1, 1'b0:=1};
       		 b dist {1'b1:=1, 1'b0:=1};
             c dist {1'b1:=4, 1'b0:=1};
           }) `uvm_error("MYERR", "This is a randomize error")
       end 
       $finish; 
    end 
endmodule

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

  • SystemVerilog Assertions Handbook 4th Edition, 2013 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 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