tests/various/muxpack.ys

   1 read_verilog muxpack.v
   2 design -save read
   3
   4 hierarchy -top mux_if_unbal_4_1
   5 prep
   6 design -save gold
   7 muxpack
   8 opt
   9 #stat
  10 select -assert-count 0 t:$mux
  11 select -assert-count 1 t:$pmux
  12 design -stash gate
  13 design -import gold -as gold
  14 design -import gate -as gate
  15 miter -equiv -flatten -make_assert -make_outputs gold gate miter
  16 sat -verify -prove-asserts -show-ports miter
  17
  18 design -load read
  19 hierarchy -top mux_if_unbal_5_3
  20 prep
  21 design -save gold
  22 muxpack
  23 opt
  24 #stat
  25 select -assert-count 0 t:$mux
  26 select -assert-count 1 t:$pmux
  27 design -stash gate
  28 design -import gold -as gold
  29 design -import gate -as gate
  30 miter -equiv -flatten -make_assert -make_outputs gold gate miter
  31 sat -verify -prove-asserts -show-ports miter
  32
  33 # TODO: Currently ExclusiveDatabase only analyses $eq cells
  34 #design -load read
  35 #hierarchy -top mux_if_unbal_5_3_invert
  36 #prep
  37 #design -save gold
  38 #muxpack
  39 #opt
  40 #stat
  41 #select -assert-count 0 t:$mux
  42 #select -assert-count 1 t:$pmux
  43 #design -stash gate
  44 #design -import gold -as gold
  45 #design -import gate -as gate
  46 #miter -equiv -flatten -make_assert -make_outputs gold gate miter
  47 #sat -verify -prove-asserts -show-ports miter
  48
  49 design -load read
  50 hierarchy -top mux_if_unbal_5_3_width_mismatch
  51 prep
  52 design -save gold
  53 muxpack
  54 opt
  55 #stat
  56 select -assert-count 0 t:$mux
  57 select -assert-count 2 t:$pmux
  58 design -stash gate
  59 design -import gold -as gold
  60 design -import gate -as gate
  61 miter -equiv -flatten -make_assert -make_outputs gold gate miter
  62 sat -verify -prove-asserts -show-ports miter
  63
  64 design -load read
  65 hierarchy -top mux_if_unbal_4_1_missing
  66 prep
  67 design -save gold
  68 muxpack
  69 opt
  70 #stat
  71 select -assert-count 0 t:$mux
  72 select -assert-count 1 t:$pmux
  73 design -stash gate
  74 design -import gold -as gold
  75 design -import gate -as gate
  76 miter -equiv -flatten -make_assert -make_outputs gold gate miter
  77 sat -verify -prove-asserts -show-ports miter
  78
  79 design -load read
  80 hierarchy -top mux_if_unbal_5_3_order
  81 prep
  82 design -save gold
  83 muxpack
  84 opt
  85 #stat
  86 select -assert-count 0 t:$mux
  87 select -assert-count 1 t:$pmux
  88 design -stash gate
  89 design -import gold -as gold
  90 design -import gate -as gate
  91 miter -equiv -flatten -make_assert -make_outputs gold gate miter
  92 sat -verify -prove-asserts -show-ports miter
  93
  94 design -load read
  95 hierarchy -top mux_if_unbal_4_1_nonexcl
  96 prep
  97 design -save gold
  98 muxpack
  99 opt
 100 #stat
 101 select -assert-count 0 t:$mux
 102 select -assert-count 1 t:$pmux
 103 design -stash gate
 104 design -import gold -as gold
 105 design -import gate -as gate
 106 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 107 sat -verify -prove-asserts -show-ports miter
 108
 109 design -load read
 110 hierarchy -top mux_if_unbal_5_3_nonexcl
 111 prep
 112 design -save gold
 113 muxpack
 114 opt
 115 #stat
 116 select -assert-count 0 t:$mux
 117 select -assert-count 1 t:$pmux
 118 design -stash gate
 119 design -import gold -as gold
 120 design -import gate -as gate
 121 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 122 sat -verify -prove-asserts -show-ports miter
 123
 124 design -load read
 125 hierarchy -top mux_case_unbal_8_7
 126 prep
 127 design -save gold
 128 muxpack
 129 opt
 130 #stat
 131 select -assert-count 0 t:$mux
 132 select -assert-count 1 t:$pmux
 133 design -stash gate
 134 design -import gold -as gold
 135 design -import gate -as gate
 136 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 137 sat -verify -prove-asserts -show-ports miter
 138
 139 design -load read
 140 hierarchy -top mux_if_bal_8_2
 141 prep
 142 design -save gold
 143 muxpack
 144 opt
 145 #stat
 146 select -assert-count 7 t:$mux
 147 select -assert-count 0 t:$pmux
 148 design -stash gate
 149 design -import gold -as gold
 150 design -import gate -as gate
 151 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 152 sat -verify -prove-asserts -show-ports miter
 153
 154 design -load read
 155 hierarchy -top mux_if_bal_5_1
 156 prep
 157 design -save gold
 158 muxpack
 159 opt
 160 #stat
 161 select -assert-count 4 t:$mux
 162 select -assert-count 0 t:$pmux
 163 design -stash gate
 164 design -import gold -as gold
 165 design -import gate -as gate
 166 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 167 sat -verify -prove-asserts -show-ports miter
 168
 169 design -load read
 170 hierarchy -top cliffordwolf_nonexclusive_select
 171 prep
 172 design -save gold
 173 muxpack
 174 opt
 175 #stat
 176 select -assert-count 3 t:$mux
 177 select -assert-count 0 t:$pmux
 178 design -stash gate
 179 design -import gold -as gold
 180 design -import gate -as gate
 181 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 182 sat -verify -prove-asserts -show-ports miter
 183
 184 #design -load read
 185 #hierarchy -top cliffordwolf_freduce
 186 #prep
 187 #design -save gold
 188 #proc; opt; freduce; opt
 189 #show
 190 #muxpack
 191 #opt
 192 #stat
 193 #select -assert-count 0 t:$mux
 194 #select -assert-count 1 t:$pmux
 195 #design -stash gate
 196 #design -import gold -as gold
 197 #design -import gate -as gate
 198 #miter -equiv -flatten -make_assert -make_outputs gold gate miter
 199 #sat -verify -prove-asserts -show-ports miter
 200
 201 design -load read
 202 hierarchy -top case_nonexclusive_select
 203 prep
 204 design -save gold
 205 muxpack
 206 opt
 207 #stat
 208 select -assert-count 0 t:$mux
 209 select -assert-count 2 t:$pmux
 210 design -stash gate
 211 design -import gold -as gold
 212 design -import gate -as gate
 213 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 214 sat -verify -prove-asserts -show-ports miter
 215
 216 design -load read
 217 hierarchy -top case_nonoverlap
 218 #prep # Do not prep otherwise $pmux's overlapping entry will get removed
 219 proc
 220 design -save gold
 221 opt -fast -mux_undef
 222 select -assert-count 2 t:$pmux
 223 muxpack
 224 opt
 225 #stat
 226 select -assert-count 0 t:$mux
 227 select -assert-count 1 t:$pmux
 228 design -stash gate
 229 design -import gold -as gold
 230 design -import gate -as gate
 231 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 232 sat -verify -prove-asserts -show-ports miter
 233
 234 design -load read
 235 hierarchy -top case_overlap
 236 #prep # Do not prep otherwise $pmux's overlapping entry will get removed
 237 proc
 238 design -save gold
 239 opt -fast -mux_undef
 240 select -assert-count 2 t:$pmux
 241 muxpack
 242 opt
 243 #stat
 244 select -assert-count 0 t:$mux
 245 select -assert-count 2 t:$pmux
 246 design -stash gate
 247 design -import gold -as gold
 248 design -import gate -as gate
 249 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 250 sat -verify -prove-asserts -show-ports miter
 251
 252 design -load read
 253 hierarchy -top case_overlap2
 254 #prep # Do not prep otherwise $pmux's overlapping entry will get removed
 255 proc
 256 design -save gold
 257 opt -fast -mux_undef
 258 select -assert-count 2 t:$pmux
 259 muxpack
 260 opt
 261 #stat
 262 select -assert-count 0 t:$mux
 263 select -assert-count 2 t:$pmux
 264 design -stash gate
 265 design -import gold -as gold
 266 design -import gate -as gate
 267 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 268 sat -verify -prove-asserts -show-ports miter