Multiclock assertion

Hi,
I am working on a assertion where signal “a” and “b” are completely independent signals and when posedge of signal “a” is there then wait for signal “b” to go low irrespective of clock and any other signal once it goes low wait for 5 cycles to check if it stays low for that cycles if not then try again when signal “b” goes low eventually when signal b stays low more then 5 cycles then after the posedge of signal “b” check that signal “c” stays low for 2 clock cycles. I am not sure that below code will work.

sequence wait_5_cycles;
  @(negedge clk) (b == 0)[*5];
endsequence

sequence wait_for_valid_b_low;
  (
    ##[0:$] $fell(b) and b_low_5_cycles
  )[->1];  
endsequence

property full_check;
  @(posedge a)
    wait_for_valid_b_low ##[1:$] $rose(b) ##1 @(negedge clk) (c == 0);
endproperty

assert property (full_check)
  else $error("Assertion Failed.");

Your requirements are difficult to understand because it is too verbal and everything was put into one very long sentence. Perplexity.ai did a good job at rephrasing the requirements to:

Requirements Breakdown

  1. Signal “a” and “b” are independent.
  2. On the posedge of signal “a”, wait for signal “b” to go low.
  3. Once signal “b” goes low, check if it stays low for 5 cycles.
  4. If signal “b” does not stay low for 5 cycles, retry when signal “b” goes low again.
  5. When signal “b” stays low for more than 5 cycles, after the posedge of signal “b”, check that signal “c” stays low for 2 clock cycles
@(posedge clk) $rose(a)|->  
         first_match(##1 !b[->1]  ##0 !b[*5][*1:$]) 
            ##1 b[->1] ##1 !c[*2]; 

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
https://systemverilog.us/vf/Cohen_Links_to_papers_books.pdf

Hi Ben,
You almost got the requirements but here are few correction.

  1. Signal “a” and “b” are independent. means no clock requited async signals
  2. On the posedge of signal “a” then wait for negedge of signal “b” .
  3. Once signal “b” goes low, check if it stays low for 5 cycles if not then check for subsequent negedge for signal b for this requirement.
  4. When signal “b” stays low for more than 5 cycles, after the at posedge of signal “b”, check that signal “c” stays low for 2 clock cycles

Thanks.

Sorry to tell you this, but your new requirements are very peculiar in that you sometimes use the variable forthe event, then switch to a clocking to test its duration.
The foillowing is close to what you want, but is illegal:
p: assert property( @(posedge a) 1|-> // ILEGAL
first_match( (@(negedge b) ##0 @(posedge clk) !b[*5]) [*1:$]) ##0 @(posedge b) ##1 @(posedge clk) !c[*2]);
** Error: (vsim-3937) Asserting on an illegal multiply clocked temporal expression. The clock flow cannot change in the operand of ‘first_match’ operator.

I suggest that you use an automatic task called by @(posedge a) and then use fork-join_none statements to get what you need. Immediate assertions can then be used from within the task.

Hi Ben,
i have written a immediate assertion for this but i am not sure when signal “a[0]”,“a[1]” and “a[2]” are triggered same time as they are different signals how the count variables will be taken care in this can you suggest any improvements.

  always @(posedge a[0] or posedge a[1] or posedge a[2]) begin 
    fork 
      begin
        if(o)begin
           count =0;             
          repeat(20)begin
            @(negedge b);
              count =0;
            repeat(5) begin 
              @(negedge clk);
                if(!b)begin
                 count++;
                end
            end
            if(count == 5) begin 
              @(posedge b);
              repeat(2) begin 
                 @(negedge clk);
                 assert (!c)
                   $info("assertion_debug  PASSED");
                 else 
                   $error("assertion_debug FAILED");
              end
              break;
            end
          end
        end
      end
    join_none
  end

Thanks.

I don’t quite understand your question, but here is my take:

module mx; 
 bit a, b, c, clk; 
 /* Signal “a” and “b” are independent. means no clock requited async signals
On the posedge of signal “a” then wait for negedge of signal “b” .
Once signal “b” goes low, check if it stays low for 5 cycles if not then check for subsequent negedge for signal b for this requirement.
When signal “b” stays low for more than 5 cycles, after the at posedge of signal “b”, check that signal “c” stays low for 2 clock cycles
*/
// Task triggering 
ap: assert property( @(posedge a) 1|->  (1, t_abcd())); 
  //  first_match( (@(negedge b) ##0 @(posedge clk) !b[*5]) [*1:$]) ##0 @(posedge b)  ##1 @(posedge clk) !c[*2]); 
 
    task automatic t_abcd(); //
       int count; 
       bit is_matched, go; 
       @(negedge b) 
        fork 
          begin  : p1  // (@(negedge b) ##0 @(posedge clk) !b[*5]) [*1:20]
            // count =0;             
            repeat(20)begin 
               count =0;
                repeat(5) @(negedge clk) if(!b)  count++;  
                if(count == 5) go=1; 
                disable p1; 
            end 
            am_no5b0: assert(0) else $display("assertion_debug NO count==5"); 
            disable p2; 
           end

           begin : p2
              wait(go);  // ##0 @(posedge b)  ##1 @(posedge clk) !c[*2]); 
                  @(posedge b);
                  repeat(2) begin 
                     @(negedge clk);
                     assert (!c)
                       $info("assertion_debug  PASSED");
                     else 
                       $error("assertion_debug FAILED");
                  end 
            end 
        join
    endtask

endmodule 

The following assertion might do the trick. I have no way to test it other than that it compiles w/o error.
ap: assert property(
@(posedge a) 1 ##0 @(negedge b) ##0
@(posedge clk) (!b[->1] ##0 !b[*1:5] ##1 b)[*0:$] ##0
!b[->1] ##0 !b[*6] |->
@(posedge b) 1 ##1 @(posedge clk) !c[*2]);

I think that triggering on negedge b and on posedge b is not necessary, posedge clk is fine.

Hi ben,
Ran this immediate assertion found one issue that “Delays or wait statements in match item task calls are not supported”.

Thanks.

Show code

Hi Ben,
code is same as you provided but my compiler is different. what can be the work around?

module mx; 
     bit a, b, c, clk; 
     /* Signal “a” and “b” are independent. means no clock requited async signals
          On the posedge of signal “a” then wait for negedge of signal “b” .
          Once signal “b” goes low, check if it stays low for 5 cycles if not then check for 
           subsequent negedge for signal b for this requirement.
          When signal “b” stays low for more than 5 cycles, after the at posedge of signal “b”, 
          check that signal “c” stays low for 2 clock cycles
      */
       // Task triggering 
      ap: assert property( @(posedge a) 1|->  (1, t_abcd())); 
       //  first_match( (@(negedge b) ##0 @(posedge clk) !b[*5]) [*1:$]) ##0 @(posedge b)  
        ##1 @(posedge clk) !c[*2]); 
 
    task automatic t_abcd(); //
       int count; 
       bit is_matched, go; 
       @(negedge b) 
        fork 
          begin  : p1  // (@(negedge b) ##0 @(posedge clk) !b[*5]) [*1:20]
            // count =0;             
            repeat(20)begin 
               count =0;
                repeat(5) @(negedge clk) if(!b)  count++;  
                if(count == 5) go=1; 
                disable p1; 
            end 
            am_no5b0: assert(0) else $display("assertion_debug NO count==5"); 
            disable p2; 
           end

           begin : p2
              wait(go);  // ##0 @(posedge b)  ##1 @(posedge clk) !c[*2]); 
                  @(posedge b);
                  repeat(2) begin 
                     @(negedge clk);
                     assert (!c)
                       $info("assertion_debug  PASSED");
                     else 
                       $error("assertion_debug FAILED");
                  end 
            end 
        join
    endtask
endmodule

Thanks.