Large Repetition No. Causes Slow Compile Time

SystemVerilog
, , ,
1

Hi,
Appreciate your support!

I am checking a sequence of a state machine.
One of the state requires me to check how long it stays in that state (state = 2).


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

define tcnt 1000
define state xxx.state
assert_seq1: assert property(@(posedge clk) check_on |=> seq1(`state,`cnt))
      $display("Sequence OK"); else
	$display("Sequence NOT OK");

I need to increase tcnt to more than 100K, but the compile time is also increasing significantly.
Does anyone know why?
Is there a better way?

2

In reply to sonofthesand:
With the tool I used,
Tried your model at Edit code - EDA Playground
I did not experience the long compilation time.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

3

In reply to ben@SystemVerilog.us:

In reply to sonofthesand:
With the tool I used,
Tried your model at Edit code - EDA Playground
I did not experience the long compilation time.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

That is strange.

May I ask how would you code such an assertion?

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

5

In reply to ben@SystemVerilog.us:

Thank you Ben, appreciate it.

I came up with another method too by using variable


sequence seq1(wu_state, M);
    int cnt;
    (state == 0,cnt=0) [*1:$] ##1
    (state == 1)       [*1:$] ##1
    (state == 2,cnt++) [*1:$]  ##0
	(M==cnt)       ##1
    (state == 3)       [*1:$] ##1
    (state == 4)       [*5]   ##1
    (state == 5)       ;
  endsequence

What do you think?

6

In reply to sonofthesand:


// Your solution is OK, but is harder to read. However, I still prefer smaller assertions instead of one large one. 
sequence seq1(wu_state, M);  // Your OK solution 
    int cnt;
    (state == 0,cnt=0) [*1:$] ##1
    (state == 1)       [*1:$] ##1
    (state == 2,cnt++) [*1:$]  ##0
	(M==cnt)       ##1
    (state == 3)       [*1:$] ##1
    (state == 4)       [*5]   ##1
    (state == 5)       ;
  endsequence

My preferred solution,with smaller assertions, more easily identifies which transition failed. It is also easier to read. For example, I read this in English for my solution with smaller assertions:
@ check_on, I stay in state0 until state1.
If in state1, I stay on state1 until state2
If in state2, I stay on state2 for M cycles and then go to state3.
…
Your solution makes a very long sentence, and the use of the variable makes it even more difficult to explain in plain English. It is more subjected to errors because of the complexity. KISS ((acronym)


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));

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

7

In reply to ben@SystemVerilog.us:

Thanks for the advise.

I have a problem with your solution though.
The state may change before check_on is high.
This causes miss trigger of assert_seq1to2 and the ones below

8

In reply to sonofthesand:

In reply to ben@SystemVerilog.us:
I have a problem with your solution though.
The state may change before check_on is high.
This causes miss trigger of assert_seq1to2 and the ones below

Since I don’t have a full set of requirements, I initially thought that *check_on

  • is more like a go instead of a mode. Ifcheck_on is a mode that remains hi till state5 (i.e., is an envelope), then you can still use small assertions:

assert_seq0to1: assert property($rose(check_on) |-> (state==0)[*1:$] ##1 (state == 1));
assert_seq1to2: assert property(check_on && $changed(state) && (state == 1) |-> 
                                (state == 1)[*1:$] ##1 (state == 2)); 
assert_seq2to3: assert property(check_on && $changed(state) && (state == 2) |-> 
                                (state == 2)[*M] ##1 (state == 3));  
assert_seq3to4: assert property(check_on && $changed(state) && (state == 3) |-> 
                                (state == 3)[*1:$] ##1 (state == 4));  
assert_seq4to5: assert property(check_on && $changed(state) && (state == 4) |-> 
                                (state == 4)[*5] ##1 (state == 5));

As I said before, all the experts on SVA (I have talked to many, including those on the IEEE SVA committee since I am also one of them) do recommend smaller assertions.
KISS !!!
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr