assert_width_logic.v

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

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

  parameter WIDTH_START = 2'b00;
  parameter WIDTH_CKMIN = 2'b01;
  parameter WIDTH_CKMAX = 2'b10;
  parameter WIDTH_IDLE  = 2'b11;

  reg r_test_expr;
  reg [1:0] r_state;
  integer num_cks;

  initial begin
    r_state=WIDTH_START;
    r_test_expr = 1'b0;
    num_cks = 0;
  end

  parameter assert_name = "ASSERT_WIDTH";

  `include "std_ovl_task.h"

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

  initial begin
    if ((min_cks > 0) && (max_cks > 0))
      if (min_cks > max_cks) ovl_error_t("min_cks > max_cks");
  end

`ifdef OVL_ASSERT_ON

  always @(posedge clk) begin
    r_test_expr <= test_expr;
      if (`OVL_RESET_SIGNAL != 1'b0) begin
        case (r_state)
          WIDTH_START: 
            if ((r_test_expr == 1'b0) && (test_expr == 1'b1)) begin
              num_cks <= 1;
              if      (min_cks > 0) r_state <= WIDTH_CKMIN;
              else if (max_cks > 0) r_state <= WIDTH_CKMAX;
            end
          WIDTH_CKMIN: 
            if (test_expr == 1'b1) begin
              num_cks <= num_cks + 1;
              if (num_cks >= min_cks) begin
                if (max_cks > 0) r_state <= WIDTH_CKMAX;
                else             r_state <= WIDTH_IDLE;
              end
            end
            else begin
              if (num_cks < min_cks) begin
                ovl_error_t("MIN_CHECK");
              end
              r_state <= WIDTH_START;
            end
          WIDTH_CKMAX:
            if (test_expr == 1'b1) begin
              num_cks <= num_cks + 1;
              if (num_cks >= max_cks) begin
                ovl_error_t("MAX_CHECK");
                r_state <= WIDTH_IDLE;
              end
            end
            else begin
              if (num_cks > max_cks) begin
                ovl_error_t("MAX_CHECK");
              end
              r_state <= WIDTH_START;
            end
          WIDTH_IDLE:
            if (test_expr == 1'b0) begin
              r_state <= WIDTH_START;
            end
        endcase
      end
      else begin
         r_state <= WIDTH_START;
         r_test_expr <= 1'b0;
      end
  end // always            

`endif // OVL_ASSERT_ON

`ifdef OVL_COVER_ON

  reg r_test_expr_cover;
  reg timer_started;
  integer num_cks_cover;

  initial begin
    r_test_expr_cover = 1'b0;
    num_cks_cover = 0;
  end

  always @(posedge clk) begin
    r_test_expr_cover <= test_expr;
    if (`OVL_RESET_SIGNAL != 1'b0 && coverage_level != `OVL_COVER_NONE) begin
      if ((r_test_expr_cover == 1'b0) && (test_expr == 1'b1)) begin
        num_cks_cover <= 1;
        timer_started <= 1;
        ovl_cover_t("test_expr_asserts covered");
      end
      else if (timer_started && test_expr == 1'b1)
        num_cks_cover <= num_cks_cover + 1;
      else if (timer_started && (r_test_expr_cover == 1'b1) && (test_expr == 1'b0)) begin
        num_cks_cover <= 0;
        timer_started <= 0;
        if (min_cks > 0 && num_cks_cover == min_cks)
          ovl_cover_t("test_expr_asserted_for_min_cks covered");
        if (max_cks > 0 && num_cks_cover == max_cks)
          ovl_cover_t("test_expr_asserted_for_max_cks covered");
      end
    end
    else begin
      num_cks_cover <= 0;
      timer_started <= 0;
    end
  end // always

`endif // OVL_COVER_ON