//---------------------------------------------------------------------------
//
//       ASSERT_CYCLE_SEQUENCE
//
//---------------------------------------------------------------------------
// NAME
//          ASSERT_CYCLE_SEQUENCE - if "necessary_condition" is 0, this 
//	      assertion checks that if all num_cks-1 first events of 
//	      "event_sequence" are true, then the last one 
//            ("event_sequence[0]") must occur.
//
//            If "necessary_condition" is 1, this assertion checks that
//	      once the first event ("event_sequence[num_cks-1]") occurs,
//	      all the remaining ones must occur.
//
// SYNOPSIS
//          assert_cycle_sequence [#(severity_level, num_cks, necessary_condition,
//                    options, msg)] inst_name (clk, reset_n, event_sequence);
//
//---------------------------------------------------------------------------

module assert_cycle_sequence (clk, reset_n, event_sequence);
// synopsys template
  parameter severity_level = 0;
  parameter num_cks=1;	// number of clocks for the sequence
  parameter necessary_condition = 0;
  parameter options = 0;
  parameter msg="VIOLATION";
  input clk, reset_n;
  input [num_cks-1:0] event_sequence;

//synopsys translate_off
`ifdef ASSERT_ON

  parameter assert_name = "ASSERT_CYCLE_SEQUENCE";

  integer error_count;
  initial error_count = 0;

  `include "ovl_task.h"

  `ifdef ASSERT_INIT_MSG
    initial
      ovl_init_msg; // Call the User Defined Init Message Routine
  `endif

  // internal parameters
  parameter width     = (num_cks>0)?num_cks:1;
  parameter num_cks_1 = width - 1;
  parameter num_buf_1 = (num_cks_1+1)*num_cks_1/2;
  parameter nec_cond  = necessary_condition & 1'b1;
  parameter non_pipe  = necessary_condition & 2'b10;

  reg [num_buf_1:1] pipe_regs;
  initial pipe_regs = 0;

  integer e_idx;
  initial e_idx = num_cks_1;

  initial begin
    if (num_cks <= 0) begin // assert invalid num_cks
      $display("WARNING: %s : parameter num_cks (%d <= 0) is invalid : time %0t : %m",
                     assert_name, num_cks, $time);
      $display("          Use default value 1 for parameter num_cks.");
    end
  end

  `ifdef ASSERT_GLOBAL_RESET
    buf (rst_n, `ASSERT_GLOBAL_RESET);
  `else
    buf (rst_n, reset_n);
  `endif

  integer ii, jj, nn, pp, lim, start;

  reg and_res;
  always @(posedge clk) begin
    if (rst_n == 0) begin // active low reset
      pipe_regs = 0;                // fill ZEROs to pipes
      e_idx <= num_cks_1;
    end
    else begin
      if (width == 1) begin
        if (!event_sequence[0]) begin // check error
	  ovl_error("");
        end
      end
      else if (nec_cond != 0) begin
        if (non_pipe) begin // non-pipelined
          if (pipe_regs[1] == 1'b0) begin // INIT
            if (event_sequence[num_cks_1]) begin
              pipe_regs[1] <= 1'b1;       // start CHECK
              e_idx <= num_cks_1 - 1'b1;
            end
          end
          else begin                      // CHECK
            if (event_sequence[e_idx] != 1'b1) begin
              pipe_regs[1] <= 1'b0;
              ovl_error("");
            end
            if (e_idx > 0) begin
              e_idx <= e_idx - 1'b1;
            end
            else begin
              pipe_regs[1] <= 1'b0;          // done CHECK, go to INIT
            end
          end
        end
        else begin          // pipelined
          if (pipe_regs[num_cks_1:1] & ~event_sequence[num_cks_1-1:0]) begin
            ovl_error("");
          end
          pipe_regs[num_cks_1:1] <= {1'b1,pipe_regs[num_cks_1-1:1]} &
                                    event_sequence[num_cks_1:1];
        end
      end
      else begin         // (necessary_condition==0), pipelined
        lim = num_cks_1;
        nn = 0; jj = 0; start = 0;
        for (pp = num_cks_1; pp >= lim; pp = pp-1) begin
          nn = nn + 1;
          start = start + nn;
          jj = start;
          and_res = 1'b1;               // get preconditon with and_res
          for (ii = nn; ii < (pp+nn); ii = ii+1) begin
            and_res = and_res && pipe_regs[jj];
            jj = jj + ii;
          end
          if (and_res && !event_sequence[num_cks_1 - pp]) begin // check error
            ovl_error("");
          end
        end
        for (ii = 1; ii < num_buf_1; ii = ii+1) begin // update pipes
          pipe_regs[ii] <= pipe_regs[ii+1];
        end
        jj = 1;
        for (ii = 1; ii <= num_cks_1; ii = ii+1) begin
          pipe_regs[jj] <= event_sequence[ii];
          jj = jj + ii + 1;
        end
      end
    end
  end // always
`endif
//synopsys translate_on

endmodule