Large Repetition No. Causes Slow Compile Time

SystemVerilog
, , ,
4

In reply to sonofthesand:
In general, it is best to write smaller assertions rather than large ones.
Below is how I converted your long assertion to multiple smaller ones. I also used the default clocking. In SystemVerilog, it is recommended to use the “let” instead of `define
You can also use the until, s_until. From my SVA Handbook 4th Edition, An until property of the non-overlapping form (i.e., until, s_until) evaluates to true if property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until at least one tick before a clock tick where property_expr2 (called the terminating property) evaluates to true. Theuntil, s_until operators have an implicit repetition until the terminating condition (i.e., property_expr2) occurs. Specifically, with a strong until (e.g.,s_until), if the simulation completes but the terminating condition is pending, the assertion fails, unlike the weak until where the assertion is evaluated as vacuously true. s_


default clocking @(posedge clk); endclocking
let M=500000; 
assert_seq0to1: assert property(check_on |-> (state==0)[*1:$] ##1 (state == 1));
assert_seq1to2: assert property($changed(state) && (state == 1) |-> (state == 1)[*1:$] ##1 (state == 2)); 
assert_seq2to3: assert property($changed(state) && (state == 2) |-> (state == 2)[*M] ##1 (state == 3));  
assert_seq3to4: assert property($changed(state) && (state == 3) |-> (state == 3)[*1:$] ##1 (state == 4));  
assert_seq4to5: assert property($changed(state) && (state == 4) |-> (state == 4)[*5] ##1 (state == 5)); 

// Use of the until 
Uassert_seq0to1: assert property(check_on |-> (state==0)[*1:$] ##1 (state == 1));
Uassert_seq1to2: assert property($changed(state) && (state == 1) |-> (state == 1) until (state == 2)); 
Uassert_seq2to3: assert property($changed(state) && (state == 2) |-> (state == 2)[*M] ##1 (state == 3));  
Uassert_seq3to4: assert property($changed(state) && (state == 3) |-> (state == 3) until (state == 4));  
Uassert_seq4to5: assert property($changed(state) && (state == 4) |-> (state == 4)[*5] ##1 (state == 5));

I ran the model below on a popular tool, and I had no issue with compilation or simulation speed. We don’t address specific tools at this forum.
The free EDA Playground tools have limitations, as they are targeted for small models. However, you can modify the code and experiment.


import uvm_pkg::*; `include "uvm_macros.svh" 
module top3; 
	bit clk, check_on;  
	bit[2:0] state;
	default clocking @(posedge clk); endclocking
	initial forever #10 clk=!clk;  
	let M=500000; 
	sequence seq1(state, M);
		    (state == 0)      [*1:$] ##1
			(state == 1)      [*1:$] ##1
			(state == 2)      [*M]   ##1
			(state == 3)      [*1:$] ##1
			(state == 4)      [*5]   ##1
			(state == 5)     	 ;
	endsequence
	assert_seq1: assert property(@(posedge clk) check_on |=> seq1(state, M))
			$display("Sequence OK"); else
			$display("Sequence NOT OK");		
	
	assert_seq0to1: assert property(check_on |-> (state==0)[*1:$] ##1 (state == 1));
	assert_seq1to2: assert property($changed(state) && (state == 1) |-> (state == 1)[*1:$] ##1 (state == 2)); 
	assert_seq2to3: assert property($changed(state) && (state == 2) |-> (state == 2)[*M] ##1 (state == 3));  
	assert_seq3to4: assert property($changed(state) && (state == 3) |-> (state == 3)[*1:$] ##1 (state == 4));  
	assert_seq4to5: assert property($changed(state) && (state == 4) |-> (state == 4)[*5] ##1 (state == 5));  
	
	Uassert_seq0to1: assert property(check_on |-> (state==0)[*1:$] ##1 (state == 1));
	Uassert_seq1to2: assert property($changed(state) && (state == 1) |-> (state == 1) until (state == 2)); 
	Uassert_seq2to3: assert property($changed(state) && (state == 2) |-> (state == 2)[*M] ##1 (state == 3));  
	Uassert_seq3to4: assert property($changed(state) && (state == 3) |-> (state == 3) until (state == 4));  
	Uassert_seq4to5: assert property($changed(state) && (state == 4) |-> (state == 4)[*5] ##1 (state == 5));  	
	
	initial  begin 
		  @(posedge clk); 
		  check_on <= 1'b1; 
		  @(posedge clk) check_on <=1'b0;
		  repeat(5)   @(posedge clk) ; 
		  state <= 3'b001; 
		  repeat(5)   @(posedge clk) ; 
		  state <= 3'b010; 
		  repeat(M)   @(posedge clk) ; 
		  state <= 3'b011; 	
		  repeat(8)   @(posedge clk) ; 
		  state <= 3'b100; 
		  repeat(5)   @(posedge clk) ; 
		  state <= 3'b101; 		  	  
	end 	
 
	/* initial begin 
		repeat(4000) begin 
			@(posedge clk);   
			if (!randomize(state, check_on)  with 
					{ state < 6;
					  check_on dist {1'b1:=1, 1'b0:=40};}
				) `uvm_error("MYERR", "This is a randomize error")
		end 
		$stop; 
		end  */ 
endmodule

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