property p_chk_val(clk, rst, en, cyc, sig, val);

  @(posedge clk)

  disable iff (rst)

  en |-> ##cyc sig === val;

endproperty

property p_chk2_val(clk, rst, en1, cyc1, en2, cyc2, sig, val);

  @(posedge clk)

  disable iff (rst)

  en1 ##cyc1 en2 |-> ##cyc2 sig === val;

endproperty

property p_chk_val_repeat(clk, rst, en, num1, cyc, sig, val, num2);

  @(posedge clk)

  disable iff (rst)

  en[*num1] |-> ##cyc (sig === val)[*num2];

endproperty

property p_chk_stable(clk, rst, en, cyc, sig);

  @(posedge clk)

  disable iff (rst)

  en |-> ##cyc $stable(sig);

endproperty

property p_trig_rose(clk, rst, en, trig, cyc, sig);

  @(posedge clk)

  disable iff (rst)

  en && $rose(trig) |-> ##cyc $rose(sig);

endproperty

property p_trig2_rose(clk, rst, en, trig1, cyc1, trig2, cyc2, sig);

  @(posedge clk)

  disable iff (rst)

  en && $rose(trig1) ##cyc1 $rose(trig2) |-> ##cyc2 $rose(sig);

endproperty

property p_trig2_val(clk, rst, en, trig1, cyc1, trig2, cyc2, sig, val);

  @(posedge clk)

  disable iff (rst)

  en && $rose(trig1) ##cyc1 $rose(trig2) |-> ##cyc2 sig === val;

endproperty

property p_trig2_trig3_thr_val(clk, rst, en, trig1, cyc1, trig2, cyc2, trig3, sig, val);

  @(posedge clk)

  disable iff (rst)

  en && $rose(trig1) ##cyc1 $rose(trig2) |-> ##cyc2 ((sig === val) throughout $rose(trig3)[->1]);

endproperty

property p_trig_rose2(clk, rst, en, trig, cyc1, cyc2, sig);

  @(posedge clk)

  disable iff (rst)

  en && $rose(trig) |-> ##[cyc1:cyc2] $rose(sig);

endproperty

property p_chk_trig2_rose(clk, rst, en, trig1, trig2, cyc1, cyc2, sig);

  @(posedge clk)

  disable iff (rst)

  en && $rose(trig1) ##cyc1 $rose(trig2)[->1] |-> ##cyc2 $rose(sig);

endproperty

property p_chk_trig2_stable(clk, rst, en, trig1, trig2, cyc1, cyc2, sig);

  @(posedge clk)

  disable iff (rst)

  en && $rose(trig1) ##cyc1 $rose(trig2)[->1] |-> ##cyc2 $stable(sig);

endproperty

property p_trig_sync_rose(clk, rst, en, sync, trig, cyc, sig);

  @(posedge clk)

  disable iff (rst)

  en && $rose(trig) ##0 sync[->1] |-> ##cyc $rose(sig);

endproperty

property p_trig_val(clk, rst, en, trig, cyc, sig, val);

  @(posedge clk)

  disable iff (rst)

  en && $rose(trig) |-> ##cyc sig === val;

endproperty

property p_trig_stable(clk, rst, en, trig, cyc, sig);

  @(posedge clk)

  disable iff (rst)

  en && $rose(trig) |-> ##cyc $stable(sig);

endproperty

property p_trig1_trig2_val(clk, rst, trig1, trig2, act, cyc, sig, val);

  @(posedge clk)

  disable iff (rst)

  $rose(trig1) ##0 $rose(trig2)[->1] ##0 act[->1] |-> ##cyc sig == val;

endproperty

property p_trig1_trig2_through(clk, rst, trig1, trig2, act, cyc, sig, val1, val2);

  @(posedge clk)

  disable iff (rst)

  $rose(trig1) |-> ((sig == val1) throughout ($rose(trig2)[->1] ##0 act[->1])) ##cyc sig == val2;

endproperty

property p_trig_past_val(clk, rst, en, trig, cyc, sig, val);

  @(posedge clk)

  disable iff (rst)

  en && $rose(trig) |-> $past(sig, cyc) === val;

endproperty

property p_cnt_up(clk, rst, en, cyc, cnt, val, delta);

  @(posedge clk)

  disable iff (rst)

  en && (cnt != val) |-> ##cyc cnt == ($past(cnt, cyc) + delta);

endproperty

property p_cnt_down(clk, rst, en, cyc, cnt, val, delta);

  @(posedge clk)

  disable iff (rst)

  en && (cnt != val) |-> ##cyc cnt == ($past(cnt, cyc) - delta);

endproperty

property p_cnt_val(clk, rst, en, cyc, cnt, val1, val2);

  @(posedge clk)

  disable iff (rst)

  en && (cnt == val1) |-> ##cyc cnt == val2;

endproperty

property p_cnt_stable(clk, rst, en, cyc, cnt, num);

  @(posedge clk)

  disable iff (rst)

  en & (cnt != $past(cnt)) |-> ##cyc $stable(cnt)[*num];

endproperty

property p_chk_pulse(clk, rst, en, trig, cyc1, cyc2, sig);

  @(posedge clk)

  disable iff (rst)

  en && $rose(trig) |-> ##cyc1 $rose(sig) ##cyc2 $fell(sig);

endproperty

property p_chk_pulse_width(clk, rst, en, trig, cyc1, cyc2, sig);

  @(posedge clk)

  disable iff (rst)

  en && $rose(trig) |-> ##cyc1 $rose(sig) ##0 sig[*cyc2] ##1 $fell(sig);

endproperty

property p_chk_trig_val2(clk, rst, en, trig, cyc1, cyc2, sig, val1, val2);

  @(posedge clk)

  disable iff (rst)

  en && $rose(trig) |-> ##cyc1 sig == val1 ##cyc2 sig == val2;

endproperty

property p_chk_rose_a(clk, rst, en, trig, cyc, sig);

  @(posedge clk)

  disable iff (rst)

  en && $rose(trig) ##cyc $rose(trig)[->1] |-> $rose(sig);

endproperty

property p_state_trans_next(clk, rst, en, state, state1, state2);

  @(posedge clk)

  disable iff (rst)

  en && (state === state1) ##1 (state !== state1) |-> (state  === state2);

endproperty

property p_state_trans_past_trg(clk, rst, en, state, state1, cyc, sig, val);

  @(posedge clk)

  disable iff (rst)

  en && (state === state1) ##1 (state !== state1) |-> $past(sig, cyc) === val;

endproperty

property p_chk_pulse_state_trans(clk, rst, state, state1, state2, trig, cyc1, cyc2, sig);

  @(posedge clk)

  disable iff (rst)

  (state == state1 ##1 state == state2) ##0 trig[->1] |-> ##cyc1 $rose(sig) ##0 trig[->1] ##cyc2 $fell(sig);

endproperty

property p_chk_transition1(clk, rst, trig, num, state, state1);

  @(posedge clk)

  disable iff (rst)

  $rose(trig) |-> ##1 ($stable(state) throughout !$stable(num)[->1]);

endproperty