[OpenSPARC-T2-DV] / 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);

// }
Commit	Line	Data
86530b38 AT	1	// ========== Copyright Header Begin ==========================================
	2	//
	3	// OpenSPARC T2 Processor File: mcusat_rd_wr_l2if_sample.vrhpal
	4	// Copyright (C) 1995-2007 Sun Microsystems, Inc. All Rights Reserved
	5	// 4150 Network Circle, Santa Clara, California 95054, U.S.A.
	6	//
	7	// * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
	8	//
	9	// This program is free software; you can redistribute it and/or modify
	10	// it under the terms of the GNU General Public License as published by
	11	// the Free Software Foundation; version 2 of the License.
	12	//
	13	// This program is distributed in the hope that it will be useful,
	14	// but WITHOUT ANY WARRANTY; without even the implied warranty of
	15	// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
	16	// GNU General Public License for more details.
	17	//
	18	// You should have received a copy of the GNU General Public License
	19	// along with this program; if not, write to the Free Software
	20	// Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
	21	//
	22	// For the avoidance of doubt, and except that if any non-GPL license
	23	// choice is available it will apply instead, Sun elects to use only
	24	// the General Public License version 2 (GPLv2) at this time for any
	25	// software where a choice of GPL license versions is made
	26	// available with the language indicating that GPLv2 or any later version
	27	// may be used, or where a choice of which version of the GPL is applied is
	28	// otherwise unspecified.
	29	//
	30	// Please contact Sun Microsystems, Inc., 4150 Network Circle, Santa Clara,
	31	// CA 95054 USA or visit www.sun.com if you need additional information or
	32	// have any questions.
	33	//
	34	// ========== Copyright Header End ============================================
	35	wildcard state s_L2_RD_ASSRT (L2_RD_ASSRT);
	36	wildcard state s_L2_RD_DEASSRT (L2_RD_DEASSRT);
	37	wildcard state s_L2_RD_DUMMY_ASSRT (L2_RD_DUMMY_ASSRT);
	38	wildcard state s_L2_RD_DUMMY_DEASSRT (L2_RD_DUMMY_DEASSRT);
	39	wildcard state s_L2_Q_FULL_RD_DUMMY_DEASSRT (L2_Q_FULL_RD_DUMMY_DEASSRT);
	40	wildcard state s_L2_Q_FULL_RD_DUMMY_ACK_DEASSRT (L2_Q_FULL_RD_DUMMY_ACK_DEASSRT);
	41	wildcard state s_L2_Q_FULL_RD_DEASSRT (L2_Q_FULL_RD_DEASSRT);
	42	wildcard state s_L2_WR_ASSRT (L2_WR_ASSRT);
	43	wildcard state s_L2_WR_DEASSRT (L2_WR_DEASSRT);
	44	wildcard state s_DRAM_WR_ACK_ASSRT (DRAM_WR_ACK_ASSRT);
	45	wildcard state s_DRAM_WR_ACK_DEASSRT (DRAM_WR_ACK_DEASSRT);
	46	wildcard state s_DRAM_WR_VLD_ASSRT (DRAM_WR_VLD_ASSRT);
	47	wildcard state s_DRAM_WR_VLD_DEASSRT (DRAM_WR_VLD_DEASSRT);
	48	wildcard state s_L2_Q_FULL_WR_ASSRT (L2_Q_FULL_WR_ASSRT);
	49	wildcard state s_L2_Q_FULL_WR_DEASSRT (L2_Q_FULL_WR_DEASSRT);
	50
	51	// transitions(to same)
	52	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]);
	53
	54	// transitions(to different)
	55	wildcard trans t_s_L2_RD_ASSRT_s_L2_RD_DEASSRT (L2_RD_ASSRT -> L2_RD_DEASSRT);
	56	wildcard trans t_s_L2_RD_DEASSRT_s_L2_RD_ASSRT (L2_RD_DEASSRT -> L2_RD_ASSRT);
	57	wildcard trans t_s_L2_RD_DUMMY_ASSRT_s_L2_RD_DUMMY_DEASSRT (L2_RD_DUMMY_ASSRT -> L2_RD_DUMMY_DEASSRT);
	58	wildcard trans t_s_L2_RD_DUMMY_DEASSRT_s_L2_RD_DUMMY_ASSRT (L2_RD_DUMMY_DEASSRT -> L2_RD_DUMMY_ASSRT);
	59
	60	wildcard trans t_s_L2_WR_ASSRT_s_L2_WR_DEASSRT (L2_WR_ASSRT -> L2_WR_DEASSRT);
	61	wildcard trans t_s_L2_WR_DEASSRT_s_L2_WR_ASSRT (L2_WR_DEASSRT -> L2_WR_ASSRT);
	62	wildcard trans t_s_DRAM_WR_ACK_ASSRT_s_DRAM_WR_ACK_DEASSRT (DRAM_WR_ACK_ASSRT -> DRAM_WR_ACK_DEASSRT);
	63	wildcard trans t_s_DRAM_WR_ACK_DEASSRT_s_DRAM_WR_ACK_ASSRT (DRAM_WR_ACK_DEASSRT -> DRAM_WR_ACK_ASSRT);
	64	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);
65	wildcard trans t_s_DRAM_WR_VLD_ASSRT_s_DRAM_WR_VLD_DEASSRT (DRAM_WR_VLD_ASSRT -> DRAM_WR_VLD_DEASSRT);
66	wildcard trans t_s_DRAM_WR_VLD_DEASSRT_s_DRAM_WR_VLD_ASSRT (DRAM_WR_VLD_DEASSRT -> DRAM_WR_VLD_ASSRT);
67	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);
68
69	// transitions(combinations) see if achievable
70	// with the rclk=#10gclk the wr ack deassrt for 6 clocks
71	// running at ciop and changing from 5 to 4, yet again
72	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 );
73
74
75	// bad states
76	//bad_state s_not_WR_Q_STATE (not state);
77	bad_state s_bad_rd_wr_assrt (L2_RD_WR_ASSRT);
78	bad_state s_bad_q_full_n_dummy_rd (L2_Q_FULL_RD_DUMMY_ASSRT);
79	wildcard bad_state s_L2_Q_FULL_RD_DUMMY_ASSRT (L2_Q_FULL_RD_DUMMY_ASSRT);
80	wildcard bad_state s_L2_Q_FULL_RD_DUMMY_ACK (L2_Q_FULL_RD_DUMMY_ACK);
81	wildcard bad_state s_L2_Q_FULL_RD_ASSRT (L2_Q_FULL_RD_ASSRT);
82
83	// bad transitions
84	//bad_trans t_not_WR_Q_TRANS (not trans);
85	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);
86	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);
87	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);
88	// with the rclk=#10gclk the wr ack deassrt for 6 clocks (changing from 6 to 5)
89	// running at ciop and changing from 5 to 4, yet again
90	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);
91	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);
92	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);
93	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);
94	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);
95	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);
96	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);
97	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);
98	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);
99
100	// }
101