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

// ========== Copyright Header Begin ==========================================
//
// OpenSPARC T2 Processor File: mcusat_rd_que_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_RD_REQ_DEASSRT             (RD_REQ_DEASSRT         );
    wildcard state s_RD_REQ_ASSRT               (RD_REQ_ASSRT           );
    wildcard state s_RD_Q_WR_PTR_DEASSRT        (RD_Q_WR_PTR_DEASSRT    );
    wildcard state s_RD_Q_WR_PTR_ASSRT0         (RD_Q_WR_PTR_ASSRT0     );
    wildcard state s_RD_Q_WR_PTR_ASSRT1         (RD_Q_WR_PTR_ASSRT1     );
    wildcard state s_RD_Q_WR_PTR_ASSRT2         (RD_Q_WR_PTR_ASSRT2     );
    wildcard state s_RD_Q_WR_PTR_ASSRT3         (RD_Q_WR_PTR_ASSRT3     );
    wildcard state s_RD_Q_WR_PTR_ASSRT4         (RD_Q_WR_PTR_ASSRT4     );
    wildcard state s_RD_Q_WR_PTR_ASSRT5         (RD_Q_WR_PTR_ASSRT5     );
    wildcard state s_RD_Q_WR_PTR_ASSRT6         (RD_Q_WR_PTR_ASSRT6     );
    wildcard state s_RD_Q_WR_PTR_ASSRT7         (RD_Q_WR_PTR_ASSRT7     );
    wildcard state s_RD_Q_RD_PTR_DEASSRT        (RD_Q_RD_PTR_DEASSRT    );
    wildcard state s_RD_Q_RD_PTR_ASSRT0         (RD_Q_RD_PTR_ASSRT0     );
    wildcard state s_RD_Q_RD_PTR_ASSRT1         (RD_Q_RD_PTR_ASSRT1     );
    wildcard state s_RD_Q_RD_PTR_ASSRT2         (RD_Q_RD_PTR_ASSRT2     );
    wildcard state s_RD_Q_RD_PTR_ASSRT3         (RD_Q_RD_PTR_ASSRT3     );
    wildcard state s_RD_Q_RD_PTR_ASSRT4         (RD_Q_RD_PTR_ASSRT4     );
    wildcard state s_RD_Q_RD_PTR_ASSRT5         (RD_Q_RD_PTR_ASSRT5     );
    wildcard state s_RD_Q_RD_PTR_ASSRT6         (RD_Q_RD_PTR_ASSRT6     );
    wildcard state s_RD_Q_RD_PTR_ASSRT7         (RD_Q_RD_PTR_ASSRT7     );
    wildcard state s_RD_Q_CNT0                  (RD_Q_CNT0              );
    wildcard state s_RD_Q_CNT1                  (RD_Q_CNT1              );
    wildcard state s_RD_Q_CNT2                  (RD_Q_CNT2              );
    wildcard state s_RD_Q_CNT3                  (RD_Q_CNT3              );
    wildcard state s_RD_Q_CNT4                  (RD_Q_CNT4              );
    wildcard state s_RD_Q_CNT5                  (RD_Q_CNT5              );
    wildcard state s_RD_Q_CNT6                  (RD_Q_CNT6              );
    wildcard state s_RD_Q_CNT7                  (RD_Q_CNT7              );
    wildcard state s_RD_Q_CNT8                  (RD_Q_CNT8              );
    wildcard state s_RD_Q_NOT_FULL              (RD_Q_NOT_FULL          );
    wildcard state s_RD_Q_FULL                  (RD_Q_FULL              );
    wildcard state s_RD_COLPS_FIFO_CNT0         (RD_COLPS_FIFO_CNT0     );
    wildcard state s_RD_COLPS_FIFO_CNT1         (RD_COLPS_FIFO_CNT1     );
    wildcard state s_RD_COLPS_FIFO_CNT2         (RD_COLPS_FIFO_CNT2     );
    wildcard state s_RD_COLPS_FIFO_CNT3         (RD_COLPS_FIFO_CNT3     );
    wildcard state s_RD_COLPS_FIFO_CNT4         (RD_COLPS_FIFO_CNT4     );
    wildcard state s_RD_COLPS_FIFO_CNT5         (RD_COLPS_FIFO_CNT5     );
    wildcard state s_RD_COLPS_FIFO_CNT6         (RD_COLPS_FIFO_CNT6     );
    wildcard state s_RD_COLPS_FIFO_CNT7         (RD_COLPS_FIFO_CNT7     );
    wildcard state s_RD_COLPS_FIFO_CNT8         (RD_COLPS_FIFO_CNT8     );
    wildcard state s_RD_COLPS_FIFO_NOT_FULL     (RD_COLPS_FIFO_NOT_FULL );
    wildcard state s_RD_COLPS_FIFO_FULL         (RD_COLPS_FIFO_FULL     );
    wildcard state s_RD_Q_NOT_EMPTY             (RD_Q_NOT_EMPTY         );
    wildcard state s_RD_Q_EMPTY                 (RD_Q_EMPTY             );
    wildcard state s_RD_COLPS_FIFO_NOT_EMPTY    (RD_COLPS_FIFO_NOT_EMPTY);
    wildcard state s_RD_COLPS_FIFO_EMPTY        (RD_COLPS_FIFO_EMPTY    );


  // transitions(to same)
  wildcard trans t_s_RD_Q_s_RD_Q       ( [RD_REQ_DEASSRT, RD_REQ_ASSRT, RD_Q_WR_PTR_DEASSRT, RD_Q_WR_PTR_ASSRT0, RD_Q_WR_PTR_ASSRT1, RD_Q_WR_PTR_ASSRT2, RD_Q_WR_PTR_ASSRT3, RD_Q_WR_PTR_ASSRT4, RD_Q_WR_PTR_ASSRT5, RD_Q_WR_PTR_ASSRT6, RD_Q_WR_PTR_ASSRT7, RD_Q_RD_PTR_DEASSRT, RD_Q_RD_PTR_ASSRT0, RD_Q_RD_PTR_ASSRT1, RD_Q_RD_PTR_ASSRT2, RD_Q_RD_PTR_ASSRT3, RD_Q_RD_PTR_ASSRT4, RD_Q_RD_PTR_ASSRT5, RD_Q_RD_PTR_ASSRT6, RD_Q_RD_PTR_ASSRT7, RD_Q_CNT0, RD_Q_CNT1, RD_Q_CNT2, RD_Q_CNT3, RD_Q_CNT4, RD_Q_CNT5, RD_Q_CNT6, RD_Q_CNT7, RD_Q_CNT8, RD_Q_NOT_FULL, RD_Q_FULL, RD_COLPS_FIFO_CNT0, RD_COLPS_FIFO_CNT1, RD_COLPS_FIFO_CNT2, RD_COLPS_FIFO_CNT3, RD_COLPS_FIFO_CNT4, RD_COLPS_FIFO_CNT5, RD_COLPS_FIFO_CNT6, RD_COLPS_FIFO_CNT7, RD_COLPS_FIFO_CNT8, RD_COLPS_FIFO_NOT_FULL, RD_COLPS_FIFO_FULL, RD_Q_NOT_EMPTY, RD_Q_EMPTY, RD_COLPS_FIFO_NOT_EMPTY, RD_COLPS_FIFO_EMPTY] -> [RD_REQ_DEASSRT, RD_REQ_ASSRT, RD_Q_WR_PTR_DEASSRT, RD_Q_WR_PTR_ASSRT0, RD_Q_WR_PTR_ASSRT1, RD_Q_WR_PTR_ASSRT2, RD_Q_WR_PTR_ASSRT3, RD_Q_WR_PTR_ASSRT4, RD_Q_WR_PTR_ASSRT5, RD_Q_WR_PTR_ASSRT6, RD_Q_WR_PTR_ASSRT7, RD_Q_RD_PTR_DEASSRT, RD_Q_RD_PTR_ASSRT0, RD_Q_RD_PTR_ASSRT1, RD_Q_RD_PTR_ASSRT2, RD_Q_RD_PTR_ASSRT3, RD_Q_RD_PTR_ASSRT4, RD_Q_RD_PTR_ASSRT5, RD_Q_RD_PTR_ASSRT6, RD_Q_RD_PTR_ASSRT7, RD_Q_CNT0, RD_Q_CNT1, RD_Q_CNT2, RD_Q_CNT3, RD_Q_CNT4, RD_Q_CNT5, RD_Q_CNT6, RD_Q_CNT7, RD_Q_CNT8, RD_Q_NOT_FULL, RD_Q_FULL, RD_COLPS_FIFO_CNT0, RD_COLPS_FIFO_CNT1, RD_COLPS_FIFO_CNT2, RD_COLPS_FIFO_CNT3, RD_COLPS_FIFO_CNT4, RD_COLPS_FIFO_CNT5, RD_COLPS_FIFO_CNT6, RD_COLPS_FIFO_CNT7, RD_COLPS_FIFO_CNT8, RD_COLPS_FIFO_NOT_FULL, RD_COLPS_FIFO_FULL, RD_Q_NOT_EMPTY, RD_Q_EMPTY, RD_COLPS_FIFO_NOT_EMPTY, RD_COLPS_FIFO_EMPTY]);

  // transitions(to different)
  wildcard trans t_s_RD_REQ_DEASSRT_s_RD_REQ_ASSRT         (RD_REQ_DEASSRT -> RD_REQ_ASSRT);
  wildcard trans t_s_RD_REQ_ASSRT_s_RD_REQ_DEASSRT         (RD_REQ_ASSRT   -> RD_REQ_DEASSRT);

. for ( $i = 0; $i < 8; $i++ ) {
.   print "  wildcard trans t_s_RD_Q_WR_PTR_DEASSRT_s_RD_Q_WR_PTR_ASSRT$i\t\t(RD_Q_WR_PTR_DEASSRT -> RD_Q_WR_PTR_ASSRT$i\);\n";
.   print "  wildcard trans t_s_RD_Q_WR_PTR_ASSRT$i\_s_RD_Q_WR_PTR_DEASSRT\t\t(RD_Q_WR_PTR_ASSRT$i\ -> RD_Q_WR_PTR_DEASSRT);\n";
.  for ( $j = $i+1; $j < 8; $j++ ) {
.   print "  wildcard trans t_s_RD_Q_WR_PTR_ASSRT$i\_s_RD_Q_WR_PTR_ASSRT$j\t\t(RD_Q_WR_PTR_ASSRT$i\ -> RD_Q_WR_PTR_ASSRT$j\);\n";
. if ( $j eq "7" ) {
// This can never be achieved since, rd q full <=> no more requests.
.   print "  wildcard bad_trans t_s_RD_Q_WR_PTR_ASSRT$j\_s_RD_Q_WR_PTR_ASSRT$i\t\t(RD_Q_WR_PTR_ASSRT$j\ -> RD_Q_WR_PTR_ASSRT$i\);\n";
.   } else {
.   print "  wildcard trans t_s_RD_Q_WR_PTR_ASSRT$j\_s_RD_Q_WR_PTR_ASSRT$i\t\t(RD_Q_WR_PTR_ASSRT$j\ -> RD_Q_WR_PTR_ASSRT$i\);\n";
.   }
.  }
.}

// $i = 7 would not allow this transition coz queue is full
. for ( $i = 0; $i < 8; $i++ ) {
.   print "  wildcard trans t_s_RD_Q_RD_PTR_DEASSRT_s_RD_Q_RD_PTR_ASSRT$i\t\t(RD_Q_RD_PTR_DEASSRT -> RD_Q_RD_PTR_ASSRT$i\);\n";
.   print "  wildcard trans t_s_RD_Q_RD_PTR_ASSRT$i\_s_RD_Q_RD_PTR_DEASSRT\t\t(RD_Q_RD_PTR_ASSRT$i\ -> RD_Q_RD_PTR_DEASSRT);\n";
.  for ( $j = $i+1; $j < 8; $j++ ) {
.   print "  wildcard bad_trans t_s_RD_Q_RD_PTR_ASSRT$i\_s_RD_Q_RD_PTR_ASSRT$j\t\t(RD_Q_RD_PTR_ASSRT$i\ -> RD_Q_RD_PTR_ASSRT$j\);\n";
.   print "  wildcard bad_trans t_s_RD_Q_RD_PTR_ASSRT$j\_s_RD_Q_RD_PTR_ASSRT$i\t\t(RD_Q_RD_PTR_ASSRT$j\ -> RD_Q_RD_PTR_ASSRT$i\);\n";
.  }
.}

. for ( $i = 0; $i < 8; $i++ ) {
.  $j = $i+1;
.   print "  wildcard trans t_s_RD_Q_CNT$i\_s_RD_Q_CNT$j\t\t(RD_Q_CNT$i\ -> RD_Q_CNT$j\);\n";
.   print "  wildcard trans t_s_RD_Q_CNT$j\_s_RD_Q_CNT$i\t\t(RD_Q_CNT$j\ -> RD_Q_CNT$i\);\n";
.}

  wildcard trans t_s_RD_Q_NOT_FULL_s_RD_Q_FULL         (RD_Q_NOT_FULL -> RD_Q_FULL);
  wildcard trans t_s_RD_Q_FULL_s_RD_Q_NOT_FULL         (RD_Q_FULL     -> RD_Q_NOT_FULL);

. for ( $i = 0; $i < 8; $i++ ) {
.  $j = $i+1;
.   print "  wildcard trans t_s_RD_COLPS_FIFO_CNT$i\_s_RD_COLPS_FIFO_CNT$j\t\t(RD_COLPS_FIFO_CNT$i\ -> RD_COLPS_FIFO_CNT$j\);\n";
.   print "  wildcard trans t_s_RD_COLPS_FIFO_CNT$j\_s_RD_COLPS_FIFO_CNT$i\t\t(RD_COLPS_FIFO_CNT$j\ -> RD_COLPS_FIFO_CNT$i\);\n";
.}

  wildcard trans t_s_RD_COLPS_FIFO_NOT_FULL_s_RD_COLPS_FIFO_FULL         (RD_COLPS_FIFO_NOT_FULL -> RD_COLPS_FIFO_FULL);
  wildcard trans t_s_RD_COLPS_FIFO_FULL_s_RD_COLPS_FIFO_NOT_FULL         (RD_COLPS_FIFO_FULL     -> RD_COLPS_FIFO_NOT_FULL);

  wildcard trans t_s_RD_Q_NOT_EMPTY_s_RD_Q_EMPTY         (RD_Q_NOT_EMPTY -> RD_Q_EMPTY);
  wildcard trans t_s_RD_Q_EMPTY_s_RD_Q_NOT_EMPTY         (RD_Q_EMPTY     -> RD_Q_NOT_EMPTY);
  wildcard trans t_s_RD_COLPS_FIFO_NOT_EMPTY_s_RD_COLPS_FIFO_EMPTY         (RD_COLPS_FIFO_NOT_EMPTY -> RD_COLPS_FIFO_EMPTY);
  wildcard trans t_s_RD_COLPS_FIFO_EMPTY_s_RD_COLPS_FIFO_NOT_EMPTY         (RD_COLPS_FIFO_EMPTY     -> RD_COLPS_FIFO_NOT_EMPTY);

  // transitions(combinations)
  wildcard trans t_s_0_to_8_b2b_rd          (RD_REQ_DEASSRT   -> RD_REQ_ASSRT[.1:8.] -> RD_REQ_DEASSRT);


  // bad states
  //bad_state s_not_RD_Q_STATE (not state);

  // bad transitions
  //bad_trans t_not_RD_Q_TRANS (not trans);

// }