Assertion Check

In reply to rkg_:
I am having trouble deciphering your question.
I modeled your code using the variables a, b, c
http://systemverilog.us/vf/may7b.sv



Below is the insertion of the code and images.
Your code looks ok

What is the issue?


// DO you want this? 
( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b01 )   |-> 
            ##1 (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8])
            ##0 o_fll_lock; 

// OR this "intersect 1'b1[*1:8] , will it start matching just after sar_eoc==1"
( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b01 )   |-> 
             (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8])
            ##0 o_fll_lock; 

I suggest that you play with my code, and add debugging features.
You may also want to rephrase your requirements in English.


module top;
    timeunit 1ns;  timeprecision 100ps;    
    `include "uvm_macros.svh"
    import uvm_pkg::*;
    bit clk, a, b, c, frame; 
    event start, one, two, isct0, endc; 
    initial forever #10 clk = !clk;

    /* ( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b01 )   |-> 
            ##1 (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8])
            ##0 o_fll_lock; */ 
    function automatic void gen_e(int i);
        if(i==0) -> start;
        if(i==0)  frame = 1'b0;
        if(i==1) -> one;
        if(i==2) ->  two;
        if(i==3) ->  isct0;
        if(i==3) frame = 1'b1;
        if(i==4) begin frame = 1'b0; ->  endc; end   
    endfunction

    always @(posedge clk) begin 
       ap_test: assert property(@ (posedge clk)  ($rose(a),gen_e(0)) |-> 
        ##1 (1, gen_e(1)) ##0 ( ($rose(b)[=2], gen_e(2)) intersect 
            (1,  gen_e(3))  ##0 1 [*1:8]  )
        ##0 (c, gen_e(4))) else  frame <= 1'b0;   
       repeat(15) @(posedge clk) ; // separate threads for analysis 
    end 

    initial begin
      repeat (200) begin        
        @(posedge clk);  #2; 
        if (!randomize(a, b, c) with {
          a dist {1'b1 := 1, 1'b0 := 4};
          b dist {1'b1 := 1, 1'b0 := 1};
          c dist {1'b1 := 1, 1'b0 := 1};
        })
          `uvm_error("MYERR", "This is a randomize error");
      end
      $finish;
    end
  endmodule

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers: