assert_handshake_logic.sv

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

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

  parameter assert_name = "ASSERT_HANDSHAKE";

  `include "std_ovl_task.h"

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

  property ASSERT_HANDSHAKE_ACK_MIN_CYCLE_P;
  @(posedge clk)
  disable iff (`OVL_RESET_SIGNAL != 1'b1)
  $rose(req) |-> (!($rose(ack))) [*min_ack_cycle];
  endproperty

  property ASSERT_HANDSHAKE_ACK_MAX_CYCLE_P;
  @(posedge clk)
  disable iff (`OVL_RESET_SIGNAL != 1'b1)
  $rose(req) |-> (##[1:max_ack_cycle] ($rose(ack) || ($rose(req) && (req_drop == 1'b1))));
  endproperty
  
  property ASSERT_HANDSHAKE_ACK_MAX_LENGTH_P;
  @(posedge clk)
  disable iff (`OVL_RESET_SIGNAL != 1'b1)
  $rose(ack) |-> (ack)[*deassert_count:max_ack_length] ##1 (!ack);
  endproperty 

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

  property ASSERT_HANDSHAKE_MULTIPLE_REQ_P;
  @(posedge clk)
  disable iff (`OVL_RESET_SIGNAL != 1'b1)
  not ((req && !ack) [*1:$] ##1 (!req && !ack) [*1:$] ##1 (req && !ack));
  endproperty

  property ASSERT_HANDSHAKE_REQ_DEASSERT_P;
  @(posedge clk)
  disable iff (`OVL_RESET_SIGNAL != 1'b1)
  ($rose(ack) && (req)) |=> (##[0:deassert_count](!req));
  endproperty

`ifdef OVL_ASSERT_ON

  generate

    case (property_type)
      `OVL_ASSERT : begin
        if (min_ack_cycle > 0) begin
          A_ASSERT_HANDSHAKE_ACK_MIN_CYCLE_P:
          assert property (ASSERT_HANDSHAKE_ACK_MIN_CYCLE_P)
          else ovl_error_t("ack min cycle violation");
        end
        if (max_ack_cycle > 0) begin
          A_ASSERT_HANDSHAKE_ACK_MAX_CYCLE_P:
          assert property (ASSERT_HANDSHAKE_ACK_MAX_CYCLE_P)
          else ovl_error_t("ack max cycle violation");
        end
        if ((max_ack_length > 0) && (max_ack_length >= deassert_count)) begin
          A_ASSERT_HANDSHAKE_ACK_MAX_LENGTH_P:
          assert property (ASSERT_HANDSHAKE_ACK_MAX_LENGTH_P)
          else ovl_error_t("ack max length violation");
        end
        if (deassert_count > 0) begin
          A_ASSERT_HANDSHAKE_REQ_DEASSERT_P:
          assert property (ASSERT_HANDSHAKE_REQ_DEASSERT_P)
          else ovl_error_t("req deassert violation");
        end
        if (req_drop > 0) begin
          A_ASSERT_HANDSHAKE_REQ_DROP_P:
          assert property (ASSERT_HANDSHAKE_REQ_DROP_P)
          else ovl_error_t("req drop violation");
        end
        A_ASSERT_HANDSHAKE_MULTIPLE_REQ_P:
        assert property (ASSERT_HANDSHAKE_MULTIPLE_REQ_P)
          else ovl_error_t("multiple req violation");
      end
      `OVL_ASSUME : begin
        if (min_ack_cycle > 0) begin
          M_ASSERT_HANDSHAKE_ACK_MIN_CYCLE_P:
          assume property (ASSERT_HANDSHAKE_ACK_MIN_CYCLE_P);
        end
        if (max_ack_cycle > 0) begin
          M_ASSERT_HANDSHAKE_ACK_MAX_CYCLE_P:
          assume property (ASSERT_HANDSHAKE_ACK_MAX_CYCLE_P);
        end
        if ((max_ack_length > 0) && (max_ack_length >= deassert_count)) begin
          M_ASSERT_HANDSHAKE_ACK_MAX_LENGTH_P:
          assume property (ASSERT_HANDSHAKE_ACK_MAX_LENGTH_P);
        end
        if (deassert_count > 0) begin
          M_ASSERT_HANDSHAKE_REQ_DEASSERT_P:
          assume property (ASSERT_HANDSHAKE_REQ_DEASSERT_P);
        end
        if (req_drop > 0) begin
          M_ASSERT_HANDSHAKE_REQ_DROP_P:
          assume property (ASSERT_HANDSHAKE_REQ_DROP_P);
        end
        M_ASSERT_HANDSHAKE_MULTIPLE_REQ_P:
        assume property (ASSERT_HANDSHAKE_MULTIPLE_REQ_P);
      end
      default     : ovl_error_t("");
    endcase

  endgenerate

`endif // OVL_ASSERT_ON

`ifdef OVL_COVER_ON

  generate 

    if (coverage_level != `OVL_COVER_NONE) begin

     cover_req_asserted:
     cover property (@(posedge clk) ((`OVL_RESET_SIGNAL != 1'b0) && $rose(req)))
                     ovl_cover_t("req_asserted covered");

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

  endgenerate

`endif // OVL_COVER_ON