Need help to create assertion for the below requirement

In reply to Verif_Learner_SG:
The best way to approach the definition of a property is to specify the desired “good/expected behavior”. This is my take on your requirements.



module top;
  bit clk,reset;
  bit sig1,sig2,sig3;
  int data_load;
  always #5 clk=!clk; 
 
  // If new sig1 then data_load will be stable starting from the next clock 
  // until sig2. At sig2 data_load is changed in value and in the next cycle sig3==1
  property p_with_sig2;
    int v; 
    @(posedge clk) disable iff(reset)
    ($rose(sig1), v=data_load) |-> ##1 first_match(data_load==v[*1:$] ##1 sig2) 
                                  ##0 data_load !=v ##1 sig3;
  endproperty
  ap_with_sig2: assert property (p_with_sig2);

  //  if data_load changes between Sig1 and Sig2 posedges,
  // then Sig3 must get asserted within let's say 1 to 10 clocks
  property p_with_no_sig2;
    int v; 
    @(posedge clk) disable iff(reset)
    ($rose(sig1), v=data_load) ##1 (data_load!=v && !sig2)[->1] |-> ##[1:10] sig3;
  endproperty
  ap_with_no_sig2: assert property (p_with_no_sig2);

  initial begin
    $dumpfile("dump.vcd");
    $dumpvars(0,tb);
    #200 $finish;
  end

endmodule

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.