verif/env/common/coverage/mcusat/mcusat_rd_wr_l2if_sample.vrhpal

// ========== Copyright Header Begin ==========================================
//
// OpenSPARC T2 Processor File: mcusat_rd_wr_l2if_sample.vrhpal
// Copyright (C) 1995-2007 Sun Microsystems, Inc. All Rights Reserved
// 4150 Network Circle, Santa Clara, California 95054, U.S.A.
//
// * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
//
// This program is free software; you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation; version 2 of the License.
//
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program; if not, write to the Free Software
// Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
//
// For the avoidance of doubt, and except that if any non-GPL license
// choice is available it will apply instead, Sun elects to use only
// the General Public License version 2 (GPLv2) at this time for any
// software where a choice of GPL license versions is made
// available with the language indicating that GPLv2 or any later version
// may be used, or where a choice of which version of the GPL is applied is
// otherwise unspecified.
//
// Please contact Sun Microsystems, Inc., 4150 Network Circle, Santa Clara,
// CA 95054 USA or visit www.sun.com if you need additional information or
// have any questions.
//
// ========== Copyright Header End ============================================
    wildcard state s_L2_RD_ASSRT                (L2_RD_ASSRT);
    wildcard state s_L2_RD_DEASSRT              (L2_RD_DEASSRT);
    wildcard state s_L2_RD_DUMMY_ASSRT          (L2_RD_DUMMY_ASSRT);
    wildcard state s_L2_RD_DUMMY_DEASSRT        (L2_RD_DUMMY_DEASSRT);
    wildcard state s_L2_Q_FULL_RD_DUMMY_DEASSRT (L2_Q_FULL_RD_DUMMY_DEASSRT);
    wildcard state s_L2_Q_FULL_RD_DUMMY_ACK_DEASSRT (L2_Q_FULL_RD_DUMMY_ACK_DEASSRT);
    wildcard state s_L2_Q_FULL_RD_DEASSRT       (L2_Q_FULL_RD_DEASSRT);
    wildcard state s_L2_WR_ASSRT                (L2_WR_ASSRT);
    wildcard state s_L2_WR_DEASSRT              (L2_WR_DEASSRT);
    wildcard state s_DRAM_WR_ACK_ASSRT          (DRAM_WR_ACK_ASSRT);
    wildcard state s_DRAM_WR_ACK_DEASSRT        (DRAM_WR_ACK_DEASSRT);
    wildcard state s_DRAM_WR_VLD_ASSRT          (DRAM_WR_VLD_ASSRT);
    wildcard state s_DRAM_WR_VLD_DEASSRT        (DRAM_WR_VLD_DEASSRT);
    wildcard state s_L2_Q_FULL_WR_ASSRT         (L2_Q_FULL_WR_ASSRT);
    wildcard state s_L2_Q_FULL_WR_DEASSRT       (L2_Q_FULL_WR_DEASSRT);

  // transitions(to same)
    wildcard trans t_s_L2if_s_L2if       ([L2_RD_DEASSRT, L2_RD_DUMMY_DEASSRT, L2_Q_FULL_RD_DUMMY_DEASSRT, L2_Q_FULL_RD_DUMMY_ACK_DEASSRT, L2_Q_FULL_RD_DEASSRT, L2_WR_DEASSRT, DRAM_WR_ACK_DEASSRT, DRAM_WR_VLD_ASSRT, DRAM_WR_VLD_DEASSRT, L2_Q_FULL_WR_DEASSRT] ->[L2_RD_DEASSRT, L2_RD_DUMMY_DEASSRT, L2_Q_FULL_RD_DUMMY_DEASSRT, L2_Q_FULL_RD_DUMMY_ACK_DEASSRT, L2_Q_FULL_RD_DEASSRT, L2_WR_DEASSRT, DRAM_WR_ACK_DEASSRT, DRAM_WR_VLD_ASSRT, DRAM_WR_VLD_DEASSRT, L2_Q_FULL_WR_DEASSRT]);

  // transitions(to different)
    wildcard trans t_s_L2_RD_ASSRT_s_L2_RD_DEASSRT              (L2_RD_ASSRT -> L2_RD_DEASSRT);
    wildcard trans t_s_L2_RD_DEASSRT_s_L2_RD_ASSRT              (L2_RD_DEASSRT -> L2_RD_ASSRT);
    wildcard trans t_s_L2_RD_DUMMY_ASSRT_s_L2_RD_DUMMY_DEASSRT  (L2_RD_DUMMY_ASSRT -> L2_RD_DUMMY_DEASSRT);
    wildcard trans t_s_L2_RD_DUMMY_DEASSRT_s_L2_RD_DUMMY_ASSRT  (L2_RD_DUMMY_DEASSRT -> L2_RD_DUMMY_ASSRT);

    wildcard trans t_s_L2_WR_ASSRT_s_L2_WR_DEASSRT                (L2_WR_ASSRT -> L2_WR_DEASSRT);
    wildcard trans t_s_L2_WR_DEASSRT_s_L2_WR_ASSRT                (L2_WR_DEASSRT -> L2_WR_ASSRT);
    wildcard trans t_s_DRAM_WR_ACK_ASSRT_s_DRAM_WR_ACK_DEASSRT    (DRAM_WR_ACK_ASSRT -> DRAM_WR_ACK_DEASSRT);
    wildcard trans t_s_DRAM_WR_ACK_DEASSRT_s_DRAM_WR_ACK_ASSRT    (DRAM_WR_ACK_DEASSRT -> DRAM_WR_ACK_ASSRT);
    wildcard trans t_s_L2_Q_FULL_WR_ASSRT_s_L2_Q_FULL_WR_DEASSRT  (L2_Q_FULL_WR_ASSRT -> L2_Q_FULL_WR_DEASSRT);
    wildcard trans t_s_DRAM_WR_VLD_ASSRT_s_DRAM_WR_VLD_DEASSRT    (DRAM_WR_VLD_ASSRT -> DRAM_WR_VLD_DEASSRT);
    wildcard trans t_s_DRAM_WR_VLD_DEASSRT_s_DRAM_WR_VLD_ASSRT    (DRAM_WR_VLD_DEASSRT -> DRAM_WR_VLD_ASSRT);
    wildcard trans t_s_L2_Q_FULL_WR_DEASSRT_s_L2_Q_FULL_WR_ASSRT  (L2_Q_FULL_WR_DEASSRT -> L2_Q_FULL_WR_ASSRT);

 // transitions(combinations) see if achievable
    // with the rclk=#10gclk the wr ack deassrt for 6 clocks
    // running at ciop and changing from 5 to 4, yet again
    wildcard trans t_s_wr_req_ack_n_vld                           (L2_WR_ASSRT -> L2_WR_DEASSRT[.1:50.] -> DRAM_WR_ACK_ASSRT -> DRAM_WR_ACK_DEASSRT[.5:7.] -> DRAM_WR_VLD_ASSRT[.8.] -> DRAM_WR_VLD_DEASSRT );


  // bad states
  //bad_state s_not_WR_Q_STATE (not state);
  bad_state s_bad_rd_wr_assrt (L2_RD_WR_ASSRT);
  bad_state s_bad_q_full_n_dummy_rd (L2_Q_FULL_RD_DUMMY_ASSRT);
  wildcard bad_state s_L2_Q_FULL_RD_DUMMY_ASSRT   (L2_Q_FULL_RD_DUMMY_ASSRT);
  wildcard bad_state s_L2_Q_FULL_RD_DUMMY_ACK     (L2_Q_FULL_RD_DUMMY_ACK);
  wildcard bad_state s_L2_Q_FULL_RD_ASSRT         (L2_Q_FULL_RD_ASSRT);

  // bad transitions
  //bad_trans t_not_WR_Q_TRANS (not trans);
  bad_trans t_wr_full_n_ack  (DRAM_Q_FULL_WR_ACK_DEASSRT -> DRAM_Q_FULL_WR_ACK_ASSRT -> DRAM_Q_FULL_WR_ACK_DEASSRT);
  bad_trans t_wr_full_n_vld  (DRAM_Q_FULL_WR_VLD_DEASSRT -> DRAM_Q_FULL_WR_VLD_ASSRT -> DRAM_Q_FULL_WR_VLD_DEASSRT);
  bad_trans t_rd_full_n_ack  (DRAM_Q_FULL_RD_ACK_DEASSRT -> DRAM_Q_FULL_RD_ACK_ASSRT -> DRAM_Q_FULL_RD_ACK_DEASSRT);
  // with the rclk=#10gclk the wr ack deassrt for 6 clocks (changing from 6 to 5)
  // running at ciop and changing from 5 to 4, yet again
  wildcard bad_trans t_s_wr_req_ack_n_vld_bad0                 (DRAM_WR_ACK_ASSRT -> DRAM_WR_ACK_VLD_DEASSRT[.1:4.] -> DRAM_WR_VLD_ASSRT);
  wildcard bad_trans t_s_wr_req_ack_n_vld_bad1                 (DRAM_WR_ACK_ASSRT -> DRAM_WR_ACK_VLD_DEASSRT[.10:50.] -> DRAM_WR_VLD_ASSRT);
  wildcard bad_trans t_s_dummy_rd_n_full_bad                            (L2_Q_FULL_RD_DUMMY_ASSRT -> L2_Q_FULL_RD_DUMMY_DEASSRT[.1:15.] -> L2_Q_FULL_RD_DUMMY_ACK -> L2_Q_FULL_RD_DUMMY_ACK_DEASSRT);
  wildcard bad_trans t_s_L2_Q_FULL_RD_DUMMY_ASSRT_s_L2_Q_FULL_RD_DUMMY_DEASSRT    (L2_Q_FULL_RD_DUMMY_ASSRT -> L2_Q_FULL_RD_DUMMY_DEASSRT);
  wildcard bad_trans t_s_L2_Q_FULL_RD_DUMMY_DEASSRT_s_L2_Q_FULL_RD_DUMMY_ASSRT    (L2_Q_FULL_RD_DUMMY_DEASSRT -> L2_Q_FULL_RD_DUMMY_ASSRT);
  wildcard bad_trans t_s_L2_Q_FULL_RD_DUMMY_ACK_s_L2_Q_FULL_RD_DUMMY_ACK_DEASSRT  (L2_Q_FULL_RD_DUMMY_ACK -> L2_Q_FULL_RD_DUMMY_ACK_DEASSRT);
  wildcard bad_trans t_s_L2_Q_FULL_RD_DUMMY_ACK_DEASSRT_s_L2_Q_FULL_RD_DUMMY_ACK  (L2_Q_FULL_RD_DUMMY_ACK_DEASSRT -> L2_Q_FULL_RD_DUMMY_ACK);
  wildcard bad_trans t_s_L2_Q_FULL_RD_ASSRT_s_L2_Q_FULL_RD_DEASSRT                (L2_Q_FULL_RD_ASSRT -> L2_Q_FULL_RD_DEASSRT);
  wildcard bad_trans t_s_L2_Q_FULL_RD_DEASSRT_s_L2_Q_FULL_RD_ASSRT                (L2_Q_FULL_RD_DEASSRT -> L2_Q_FULL_RD_ASSRT);

// }