SVA : signal inside signal

SystemVerilog
,
1

Hello,
I would like to write a single property that will require a certain signal to set entirely within another signal, i.e. the following waveforms are legal :
ext_sig --------_/----------
int_sig --------------_________/---------------
OR :
ext_sig --------_/----------
int_sig --------_/---------------------
OR :
ext_sig --------____________________/----------
int_sig -------------------_/----------
OR :
ext_sig --------_/----------
int_sig --------_/----------

The following scenarios are illegal and should be detected :

  1. int_sig is not set :
    ext_sig --------____________________/----------
    int_sig ---------------------------------------------

  2. int_sig is set before ext_sig
    ext_sig --------_____________/----------
    int_sig -----_    /-------------------------

  3. int_sig is active after ext_sig was cleared
    ext_sig --------_____________/----------
    int_sig -----------------------------_    /---------

  4. int_sig is active without ext_sig
    ext_sig ----------------------------------------
    int_sig --------------________/----------------

Also, it is preferable that the signals polarity will be parametric(i.e. in the above examples the polarities are 0,0)
Can the above be described using a single property ?__
Thanks

2

In reply to shaygueta:

You want the within sequence operator. I think this will do it, or at least get you very close.

module top;
  
  bit a=1,b=1,clk=1;

  sequence pulse(sig, polarity=1);
    $fell(sig^polarity) ##0 sig^polarity[->1];
  endsequence
   
  assert property (@(posedge clk) $fell(a) || $fell(b) && a |-> pulse(b,0) within pulse(a,0))  $info("pass"); else $error("fail"); 
    initial repeat (100) #5 clk = !clk;
  
  initial begin
    @(posedge clk)
    @(posedge clk) a<=0; b<=1;
    @(posedge clk) a<=0; b<=0;
    @(posedge clk) a<=0; b<=0;
    @(posedge clk) a<=0; b<=1;
    @(posedge clk) a<=1; b<=1; $display("pass");
    @(posedge clk) a<=0; b<=0;
    @(posedge clk) a<=1; b<=1; $display("pass");
    @(posedge clk) a<=1; b<=1;
    @(posedge clk) a<=0; b<=1;
    @(posedge clk) a<=1; b<=1; $display("fail");
    @(posedge clk) a<=1; b<=1;
    @(posedge clk) a<=1; b<=0; $display("fail");
    @(posedge clk) a<=0; b<=0;
    @(posedge clk) a<=1; b<=1;
    @(posedge clk) a<=1; b<=0; $display("fail");
    @(posedge clk) a<=1; b<=1;
  end
endmodule