Simulation slows downs with running assertion reference clock with higher frequency

SystemVerilog
,
1

I’ve my assertions up and running but when I change the reference clock for assertions from 40MHz to 1000MHz it slows the simulation down.
Usually the simulation takes < 1hr to run but now it takes more than a day.

[Q1]. These are the different types of properties I’m using please let me know if the way I’m writing is causing the issue or it is because of the clock

  1. $rose(a) |-> ##[4000:6000] $fell(b)
  2. a ##0 $fell(b) |-> ##[8000:10000] $fell(c)
  3. a ##0 $rose(b) ##0 first_match(##[0:20000] $rose(clk1)) |-> first_match(##[80:1000] $rose(clk2) ) // to check if clk2 rises after clk1 within a specific time
  4. posedge clk;
    (1, sampled_time=$realtime) |-> ##1 ($realtime - sampled_time <= period_min && $realtime - sampled_time >= period_max)
  5. d |-> e
  6. f |-> (a && b && c && d )
  7. not($fell(g) || !g)

[Q2]. Is there a way to find which assertion takes more time to process ?

2
  1. Obviously, increasing the clock frequency from 40 to 1000 increases the number of attempts and thread calculations by a factor of 25.
    I am not a vendor, but at every clocking event you have a calculation of the $fell(b).
  2. $rose(a) |-> ##[4000:6000] $fell(b).
    I believe that the following solution (not for formal) would be more efficient, particularly when you are testing may assertions with similar range tests.
 int count;
  always @(posedge clk) count<= count+1; 
 task automatic t_b4000_6000(int range); 
   int ct_now=count; 
    @(negedge b) am_amax: assert(count-ct_now <= range);
  endtask
  
  assert property(@(posedge clk) $rose(a) |-> (1, t_b4000_6000(6000-4000)));
         // ##[4000:6000] $fell(b)
// another possibility
  property p;
  int ct_now; 
(@(posedge clk) ($rose(a), ct_now=count) |-> 
   @(negedge b) count - ct_now <=(6000-4000);
endproperty

Here, in the consequent, you fire a task that is waiting for a negedge b. If the simulator puts that event in the queue for something to do, I see less calculations.
I’ll do some inquiry about this and let you know.
ON

property p_period; 
realtime sampled_time;
(@( posedge clk) (1, sampled_time=$realtime) |-> ##1 ($realtime - sampled_time <= period_min && $realtime - sampled_time >= period_max)

Is there a reason to do this test at all cycles? Mybe you can do it periodically based on the value of “count”, or just once with an initial statement (e.g.,

initial begin #100 assert property (p_period);

Comment: You don’t need the first_match in the consequent because upon a match in the consequent the assertion passes.
first_match(##[80:1000] $rose(clk2) ) // no first_match needed here

a ##0 $rose(b) ##0 first_match(##[0:20000] $rose(clk1)) |-> first_match(##[80:1000] $rose(clk2) )

On Is there a way to find which assertion takes more time to process ?
Ask your vendor.

1 Like