assert_frame_logic.sv

OVL——基于断言的verilog验证 Verilog数字系统设计:RTL综合、测试平台与验证

// Accellera Standard V1.0 Open Verification Library (OVL).
// Accellera Copyright (c) 2005. All rights reserved.

  `include "std_ovl_task.h"

  parameter assert_name = "ASSERT_FRAME";

  integer ii;
  reg win;
  reg r_start_event;

  `ifdef OVL_INIT_MSG
    initial
      ovl_init_msg_t; // Call the User Defined Init Message Routine
  `endif

  initial begin
    // *** NEW STATIC CHECK FOR MIN/MAX and action_on_new_start ***
    if (~((action_on_new_start == `OVL_IGNORE_NEW_START) ||
          (action_on_new_start == `OVL_RESET_ON_NEW_START) ||
          (action_on_new_start == `OVL_ERROR_ON_NEW_START))) begin
       ovl_error_t("illegal action_on_new_start parameter");
    end
    if (max_cks && (max_cks < min_cks)) begin
       ovl_error_t("min_cks > max_cks");
    end
    ii = 0;
    win = 0;
    r_start_event = 1'b0;
  end

  always @(posedge clk) begin
      r_start_event <= start_event;
  end
  always @(posedge clk) begin
    if (`OVL_RESET_SIGNAL != 1'b1) begin
      ii <= 0;
      win <= 0;
    end
    else begin
      if (max_cks > 0) begin
        case (win) 
          0: 
            if (r_start_event == 1'b0 && start_event == 1'b1 && (test_expr != 1'b1)) begin
              win <= 1'b1;
              ii <= max_cks;
            end
          1: 
            if (r_start_event == 1'b0 && start_event == 1'b1 && 
              action_on_new_start == `OVL_RESET_ON_NEW_START) begin
              ii <= max_cks;
            end
            else if (ii <= 1 || test_expr == 1'b1) begin
              win <= 1'b0;
            end
            else begin
              ii <= ii -1;
            end
        endcase
      end
      else if (min_cks > 0) begin
        case (win) 
          0: 
            if (r_start_event == 1'b0 && start_event == 1'b1) begin
              win <= 1'b1;
              ii <= min_cks;
            end
          1: 
            if (r_start_event == 1'b0 && start_event == 1'b1 && 
              action_on_new_start == `OVL_RESET_ON_NEW_START) begin
              ii <= min_cks;
            end
            else if (ii <= 1 || test_expr == 1'b1) begin
              win <= 1'b0;
            end
            else begin
              ii <= ii -1;
            end
        endcase
      end
    end
  end

  property ASSERT_FRAME_MIN0_MAX0_P;
  @(posedge clk) 
  disable iff (`OVL_RESET_SIGNAL != 1'b1)
  $rose(start_event) |-> test_expr;
  endproperty

  property ASSERT_FRAME_ERR_ON_START_P;
  @(posedge clk) 
  disable iff (`OVL_RESET_SIGNAL != 1'b1)
  !($rose(start_event) && win);
  endproperty

  property ASSERT_FRAME_MIN_CHECK_P;
  @(posedge clk) 
  disable iff (`OVL_RESET_SIGNAL != 1'b1)
  ($rose(start_event) && !win) |-> ((!test_expr[*(min_cks)]));
  endproperty

  property ASSERT_FRAME_MAX_CHECK_P;
  @(posedge clk) 
  disable iff (`OVL_RESET_SIGNAL != 1'b1)
  ($rose(start_event) && !win) |-> (!test_expr[*0:max_cks] ##1 test_expr);
  endproperty

  property ASSERT_FRAME_RESET_ON_START_MIN_CHECK_P;
  @(posedge clk) 
  disable iff (`OVL_RESET_SIGNAL != 1'b1)
  $rose(start_event) |=> ((!test_expr[*(min_cks-1)]) or ($rose(start_event)));
  endproperty

  property ASSERT_FRAME_RESET_ON_START_MAX_CHECK_P;
  @(posedge clk) 
  disable iff (`OVL_RESET_SIGNAL != 1'b1)
  $rose(start_event) |=> (!test_expr[*0:(max_cks-1)] ##1 (test_expr || ($rose(start_event))));
  endproperty


`ifdef OVL_ASSERT_ON

  generate

    case (property_type)
      `OVL_ASSERT : begin
        if (min_cks == 0 && max_cks == 0) begin
          A_ASSERT_FRAME_MIN0_MAX0_P:
          assert property (ASSERT_FRAME_MIN0_MAX0_P) else ovl_error_t("");
        end
        if (action_on_new_start == `OVL_IGNORE_NEW_START ||
            action_on_new_start == `OVL_ERROR_ON_NEW_START) begin
          if (min_cks > 0) begin
            A_ASSERT_FRAME_MIN_CHECK_P:
            assert property (ASSERT_FRAME_MIN_CHECK_P) else ovl_error_t("");
          end
          if (max_cks > 0) begin
            A_ASSERT_FRAME_MAX_CHECK_P:
            assert property (ASSERT_FRAME_MAX_CHECK_P) else ovl_error_t("");
          end
        end
        if (action_on_new_start == `OVL_RESET_ON_NEW_START) begin
          if (min_cks > 0) begin
            A_ASSERT_FRAME_RESET_ON_START_MIN_CHECK_P:
            assert property (ASSERT_FRAME_RESET_ON_START_MIN_CHECK_P)
            else ovl_error_t("");
          end
          if (max_cks > 0) begin
            A_ASSERT_FRAME_RESET_ON_START_MAX_CHECK_P:
            assert property (ASSERT_FRAME_RESET_ON_START_MAX_CHECK_P)
            else ovl_error_t("");
          end
        end
        if (action_on_new_start == `OVL_ERROR_ON_NEW_START) begin
          A_ASSERT_FRAME_ERR_ON_START_P:
          assert property (ASSERT_FRAME_ERR_ON_START_P)
          else ovl_error_t("illegal start event");
        end
      end
      `OVL_ASSUME : begin
        if (min_cks == 0 && max_cks == 0) begin
          M_ASSERT_FRAME_MIN0_MAX0_P:
          assume property (ASSERT_FRAME_MIN0_MAX0_P);
        end
        if (action_on_new_start == `OVL_IGNORE_NEW_START ||
            action_on_new_start == `OVL_ERROR_ON_NEW_START) begin
          if (min_cks > 0) begin
            M_ASSERT_FRAME_MIN_CHECK_P:
            assume property (ASSERT_FRAME_MIN_CHECK_P);
          end
          if (max_cks > 0) begin
            M_ASSERT_FRAME_MAX_CHECK_P:
            assume property (ASSERT_FRAME_MAX_CHECK_P);
          end
        end
        if (action_on_new_start == `OVL_RESET_ON_NEW_START) begin
          if (min_cks > 0) begin
            M_ASSERT_FRAME_RESET_ON_START_MIN_CHECK_P:
            assume property (ASSERT_FRAME_RESET_ON_START_MIN_CHECK_P);
          end
          if (max_cks > 0) begin
            M_ASSERT_FRAME_RESET_ON_START_MAX_CHECK_P:
            assume property (ASSERT_FRAME_RESET_ON_START_MAX_CHECK_P);
          end
        end
        if (action_on_new_start == `OVL_ERROR_ON_NEW_START) begin
          M_ASSERT_FRAME_ERR_ON_START_P:
          assume property (ASSERT_FRAME_ERR_ON_START_P);
        end
      end
      default     : ovl_error_t("");
    endcase

  endgenerate

`endif // OVL_ASSERT_ON

`ifdef OVL_COVER_ON

  generate

    if (coverage_level != `OVL_COVER_NONE) begin

      cover_frame_start:
      cover property (@(posedge clk) (`OVL_RESET_SIGNAL != 1'b0 &&
                                      ($rose(start_event))))
                     ovl_cover_t("start_event covered");
    end

  endgenerate

`endif // OVL_COVER_ON