Leading clock mismatch error in a multi-clock property

SystemVerilog
, , ,
1

I’m trying to analyze what these errors are. Can you tell me what they mean? I have 2 scenarios:

First scenario:


property my_prop(logic clkA, clkB, sigA, sigB);
    @(posedge clkA) sigA |-> @(posedge clkB) sigB;
endproperty : p_prop

Error says "Leading clock mismatch: clkB of the consequent of the |-> operator does not agree with clkA of the antecedent.

Second scenario:


sequence my_seqA(logic clkA, sigA);
  @(posedge clkA) sigA;
endsequence : my_seqA

sequence my_seqB(logic clkB, sigB);
  @(posedge clkB) sigB;
endsequence : my_seqB

property my_prop(logic clkA, clkB, sigA, sigB);
    @(posedge clkA) sigA |-> 
    my_seqA(clkA, sigA) ##5
    my_seqB(clkB, sigB);
endproperty : p_prop

Error is "Clocks do not agree in ‘cycle delay’ sequence operator.

I tried to put ##0 after ##5, but the error is the same. Then I tried to put ##1 after ##5 and the compile error is gone. What does it mean?
In the LRM it says that I can use either ##0 and ##1 for multi-clock sequence.

2

In reply to Reuben:

  • @(posedge clkA) sigA |-> @(posedge clkB) sigB; // IS LEGAL
  • my_seqA(clkA, sigA) ##5 my_seqB(clkB, sigB);
    Violates 1800’2012 16.13.1 Multiclocked sequences, see below

module top; 
    bit clk1, clk2, a, b, c, d;  
    initial forever #10 clk1=!clk1;  
    initial forever #13 clk2=!clk2;  
    sequence s1; 
        a ##1 b; 
    endsequence 
    sequence s2; 
        c ##1 d; 
    endsequence 

    ap_illegal1_qq: assert property(@(posedge clk1)  a ##1 b ##2 @(posedge clk2) s2);
    // 1800'2012 16.13.1 Multiclocked sequences
    //  Differently clocked or multiclocked sequence operands cannot be combined 
    // with any sequence operators other than ##1 and ##0. 
    // For example, if clk1 and clk2 are not identical, then the following are illegal:
    ap_illegal1: assert property(@(posedge clk1) s1 ##2 @(posedge clk2) s2);
    ap_illegal2: assert property(@(posedge clk1) s1 intersect @(posedge clk2) s2);  // line 19
    //     Directive 'ap_illegal2' has multiple leading clocks for its maximal property.
endmodule  
// A compiler at eda playground
ERROR ACOMP3007 "Invalid delay operator. Only ##0 and ##1 are supported in multiclock context." "testbench.sv" 12  62
ERROR ACOMP3007 "Invalid delay operator. Only ##0 and ##1 are supported in multiclock context." "testbench.sv" 17  53
ERROR ACOMP3008 "Intersect is not valid multiclocked sequence operator." "testbench.sv" 18  53

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

See Paper: VF Horizons:PAPER: SVA Alternative for Complex Assertions - SystemVerilog - Verification Academy

3

In reply to ben@SystemVerilog.us:

Hi Ben. Even though I used ##0, it is still having the same error.
But when I use ##1, the compilation is good.


  logic clk_A, clk_B, clk_C, sig_Aa, sig_Ab, sig_Ba, sig_Bb, sig_Ca, sig_Cb;
  
  sequence s_seqA(logic clk, a, b);
    @(posedge clk)
    a ##1 b;
  endsequence : s_seqA
  
  sequence s_seqB(logic clk, a, b);
    @(posedge clk)
    a ##1 b;
  endsequence : s_seqB
  
  sequence s_seqC(logic clk, a, b);
    @(posedge clk)
    a ##1 b;
  endsequence : s_seqC
  
  property p_prop(logic clkA, clkB, clkC, sigAa, sigAb, sigBa, sigBb, sigCa, sigCb);
    @(posedge clkA)
    sigAa |-> ##1
    s_seqA(clkA, sigAa, sigAb) ##1 // Replace this with ##0 and it will have an error
    s_seqB(clkB, sigBa, sigBb); 
  endproperty : p_prop
  
  ap_try : assert property(p_prop(clk_A, clk_B, clk_C, sig_Aa, sig_Ab, sig_Ba, sig_Bb, sig_Ca, sig_Cb));
4

In reply to Reuben:
I believe that the versions prior to 1800’2012 had the limitation *“Differently clocked or multiclocked sequence operands cannot be combined with any sequence operators other than 1.”

See Paper: VF Horizons:PAPER: SVA Alternative for Complex Assertions - SystemVerilog - Verification Academy