sequence s_state_transition(state, state1, state2);

  (state == state1 || state == state2) throughout (state == state2)[->1];

endsequence

property p_chk_transition2(clk, rst, trig, num, state, state1, state2);

  @(posedge clk)

  disable iff (rst)

  $rose(trig) && (state == state1) |-> ##1 ($stable(num) throughout (s_state_transition(state, state1, state2)

                                                               ##1 s_state_transition(state, state2, state1)));

endproperty

property p_chk_transition3(clk, rst, trig, num, state, state1, state2, state3);

  @(posedge clk)

  disable iff (rst)

  $rose(trig) && (state == state1) |-> ##1 ($stable(num) throughout (s_state_transition(state, state1, state2)

                                                                 ##1 s_state_transition(state, state2, state3)

                                                                 ##1 s_state_transition(state, state3, state1)));

endproperty

property p_chk_transition5(clk, rst, trig, num, state, state1, state2, state3, state4, state5);

  @(posedge clk)

  disable iff (rst)

  $rose(trig) && (state == state1) |-> ##1 ($stable(num) throughout (s_state_transition(state, state1, state2)

                                                                 ##1 s_state_transition(state, state2, state3)

                                                                 ##1 s_state_transition(state, state3, state4)

                                                                 ##1 s_state_transition(state, state4, state5)

                                                                 ##1 s_state_transition(state, state5, state1)));

endproperty

property p_chk_transition6(clk, rst, trig, num, state, state1, state2, state3, state4, state5, state6);

  @(posedge clk)

  disable iff (rst)

  $rose(trig) && (state == state1) |-> ##1 ($stable(num) throughout (s_state_transition(state, state1, state2)

                                                                 ##1 s_state_transition(state, state2, state3)

                                                                 ##1 s_state_transition(state, state3, state4)

                                                                 ##1 s_state_transition(state, state4, state5)

                                                                 ##1 s_state_transition(state, state5, state6)

                                                                 ##1 s_state_transition(state, state6, state1)));

endproperty

property p_chk_transition7(clk, rst, trig, num, state, state1, state2, state3, state4, state5, state6, state7);

  @(posedge clk)

  disable iff (rst)

  $rose(trig) && (state == state1) |-> ##1 ($stable(num) throughout (s_state_transition(state, state1, state2)

                                                                 ##1 s_state_transition(state, state2, state3)

                                                                 ##1 s_state_transition(state, state3, state4)

                                                                 ##1 s_state_transition(state, state4, state5)

                                                                 ##1 s_state_transition(state, state5, state6)

                                                                 ##1 s_state_transition(state, state6, state7)

                                                                 ##1 s_state_transition(state, state7, state1)));

endproperty

property p_chk_transition9(clk, rst, trig, num, state, state1, state2, state3, state4, state5, state6, state7, state8, state9);

  @(posedge clk)

  disable iff (rst)

  $rose(trig) && (state == state1) |-> ##1 ($stable(num) throughout (s_state_transition(state, state1, state2)

                                                                 ##1 s_state_transition(state, state2, state3)

                                                                 ##1 s_state_transition(state, state3, state4)

                                                                 ##1 s_state_transition(state, state4, state5)

                                                                 ##1 s_state_transition(state, state5, state6)

                                                                 ##1 s_state_transition(state, state6, state7)

                                                                 ##1 s_state_transition(state, state7, state8)

                                                                 ##1 s_state_transition(state, state8, state9)

                                                                 ##1 s_state_transition(state, state9, state1)));

endproperty

property p_chk_state(clk, rst, en, trig, cyc, state, state1, state2);

  @(posedge clk)

  disable iff (rst)

  en && $rose(trig) && state == state1 |-> ##cyc state == state2;

endproperty

property p_state_transition(clk, rst, trig, state, state1, state2, state3);

  @(posedge clk)

  disable iff (rst)

  state == state1 ##1 state == state2 |-> ((state == state2) throughout $rose(trig)[->1]) ##1 state == state3;

endproperty

property p_trig_transition4(clk, rst, en, trig, cyc, state, state1, state2, state3, state4);

  @(posedge clk)

  disable iff (rst)

  en && $rose(trig) |-> ##cyc s_state_transition(state, state1, state2)

                        ##0   s_state_transition(state, state2, state3)

                        ##0   s_state_transition(state, state3, state4);

endproperty

property p_trig_transition6(clk, rst, en, trig, cyc, state, state1, state2, state3, state4, state5, state6);

  @(posedge clk)

  disable iff (rst)

  en && $rose(trig) |-> ##cyc s_state_transition(state, state1, state2)

                        ##0   s_state_transition(state, state2, state3)

                        ##0   s_state_transition(state, state3, state4)

                        ##0   s_state_transition(state, state4, state5)

                        ##0   s_state_transition(state, state5, state6);

endproperty

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

  @(posedge clk)

  disable iff (rst)

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

endproperty

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

  @(posedge clk)

  disable iff (rst)

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

endproperty

property p_test2(clk, rst, trig, cyc, sig);

  @(posedge clk)

  disable iff (rst)

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

endproperty

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

  @(posedge clk)

  disable iff (rst)

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

endproperty

property p_test4(clk, rst, trig1, trig2, trig3, fire, cyc1, cyc2, sig);

  @(posedge clk)

  disable iff (rst)

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

endproperty

property p_test5(clk, rst, trig1, trig2, fire, cyc1, cyc2, sig, exp);

  @(posedge clk)

  disable iff (rst)

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

endproperty

property p_test6(clk, rst, trig1, trig2, fire, cyc1, cyc2, sig);

  @(posedge clk)

  disable iff (rst)

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

endproperty

property p_trig1_trig2_thr_stable(clk, rst, en, trig1, trig2, cyc, sig);

  @(posedge clk)

  disable iff (rst)

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

endproperty

property p_trig1_trig2_thr_val(clk, rst, en, trig1, trig2, cyc, sig, val);

  @(posedge clk)

  disable iff (rst)

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

endproperty

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

  @(posedge clk)

  disable iff (rst)

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

endproperty

property p_sig_toggle(clk, rst, en, trig1, trig2, cyc1, cyc2, cyc3, cyc4, sig);

  @(posedge clk)

  disable iff (rst)

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

endproperty

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

  @(posedge clk)

  disable iff (rst)

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

endproperty

property p_trig1_trig2_with_rose(clk, rst, en, trig1, trig2, cyc, sig);

  @(posedge clk)

  disable iff (rst)

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

endproperty

property p_trig1_sig1r1_sig2r(clk, rst, en, trig1, cyc1, cyc2, cyc3, sig1, sig2);

  @(posedge clk)

  disable iff (rst)

  en && $rose(trig1) |-> ##cyc1 $rose(sig1)[->1] ##[cyc2:cyc3] $rose(sig2);

endproperty

property p_trig1_sig1r1_sig2r1(clk, rst, en, trig1, cyc1, cyc2, sig1, sig2);

  @(posedge clk)

  disable iff (rst)

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

endproperty

property p_chk_st123(clk, rst, en, st1, cyc21, cyc22, st2, cyc31, cyc32, st3);

  @(posedge clk)

  disable iff (rst)

  en && st1  |-> ##[cyc21:cyc22] st2 |-> ##[cyc31:cyc32] st3;

endproperty