tests/various/muxcover.ys

   1
   2 read_verilog -formal <<EOT
   3     module gate (input [2:0] A, B, C, D, X, output reg [2:0] Y);
   4         always @*
   5             (* parallel_case *)
   6             casez (X)
   7                 3'b??1: Y = A;
   8                 3'b?1?: Y = B;
   9                 3'b1??: Y = C;
  10                 3'b000: Y = D;
  11             endcase
  12     endmodule
  13 EOT
  14
  15
  16 ## Example usage for "pmuxtree" and "muxcover"
  17
  18 proc
  19 pmuxtree
  20 techmap
  21 muxcover -mux4
  22
  23 splitnets -ports
  24 clean
  25 # show
  26
  27
  28 ## Equivalence checking
  29
  30 read_verilog -formal <<EOT
  31     module gold (input [2:0] A, B, C, D, X, output reg [2:0] Y);
  32         always @*
  33             casez (X)
  34                 3'b001: Y = A;
  35                 3'b010: Y = B;
  36                 3'b100: Y = C;
  37                 3'b000: Y = D;
  38                 default: Y = 'bx;
  39             endcase
  40     endmodule
  41 EOT
  42
  43 proc
  44 splitnets -ports
  45 techmap -map +/simcells.v t:$_MUX4_
  46
  47 equiv_make gold gate equiv
  48 hierarchy -top equiv
  49 equiv_simple -undef
  50 equiv_status -assert
  51
  52 ## Partial matching MUX4
  53
  54 design -reset
  55 read_verilog -formal <<EOT
  56 module mux_if_bal_3_1 #(parameter N=3, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
  57 always @* begin
  58     o <= {{W{{1'bx}}}};
  59     if (s[0] == 1'b0)
  60      if (s[1] == 1'b0)
  61       o <= i[0*W+:W];
  62      else
  63       o <= i[1*W+:W];
  64     else
  65      if (s[1] == 1'b0)
  66       o <= i[2*W+:W];
  67 end
  68 endmodule
  69 EOT
  70 prep
  71 design -save gold
  72
  73 techmap
  74 muxcover -mux4=150
  75 select -assert-count 0 t:$_MUX_
  76 select -assert-count 1 t:$_MUX4_
  77 select -assert-count 0 t:$_MUX8_
  78 select -assert-count 0 t:$_MUX16_
  79 techmap -map +/simcells.v t:$_MUX4_
  80 design -stash gate
  81
  82 design -import gold -as gold
  83 design -import gate -as gate
  84
  85 miter -equiv -flatten -make_assert -make_outputs gold gate miter
  86 sat -verify -prove-asserts -show-ports miter
  87
  88 ## Partial matching MUX8
  89
  90 design -reset
  91 read_verilog -formal <<EOT
  92 module mux_if_bal_5_1 #(parameter N=5, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
  93 always @* begin
  94     o <= {{W{{1'bx}}}};
  95     if (s[0] == 1'b0)
  96      if (s[1] == 1'b0)
  97       if (s[2] == 1'b0)
  98        o <= i[0*W+:W];
  99       else
 100        o <= i[1*W+:W];
 101      else
 102       if (s[2] == 1'b0)
 103        o <= i[2*W+:W];
 104       else
 105        o <= i[3*W+:W];
 106     else
 107      if (s[1] == 1'b0)
 108       if (s[2] == 1'b0)
 109        o <= i[4*W+:W];
 110 end
 111 endmodule
 112 EOT
 113 prep
 114 design -save gold
 115
 116 techmap
 117 muxcover -mux4=150 -mux8=200
 118 clean
 119 opt_expr -mux_bool
 120 select -assert-count 0 t:$_MUX_
 121 select -assert-count 0 t:$_MUX4_
 122 select -assert-count 1 t:$_MUX8_
 123 select -assert-count 0 t:$_MUX16_
 124 techmap -map +/simcells.v t:$_MUX8_
 125 design -stash gate
 126
 127 design -import gold -as gold
 128 design -import gate -as gate
 129
 130 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 131 sat -verify -prove-asserts -show-ports miter
 132
 133 ## Partial matching MUX16
 134
 135 design -reset
 136 read_verilog -formal <<EOT
 137 module mux_if_bal_9_1 #(parameter N=9, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
 138 always @* begin
 139     o <= {{W{{1'bx}}}};
 140     if (s[0] == 1'b0)
 141      if (s[1] == 1'b0)
 142       if (s[2] == 1'b0)
 143        if (s[3] == 1'b0)
 144         o <= i[0*W+:W];
 145        else
 146         o <= i[1*W+:W];
 147       else
 148        if (s[3] == 1'b0)
 149         o <= i[2*W+:W];
 150        else
 151         o <= i[3*W+:W];
 152      else
 153       if (s[2] == 1'b0)
 154        if (s[3] == 1'b0)
 155         o <= i[4*W+:W];
 156        else
 157         o <= i[5*W+:W];
 158       else
 159        if (s[3] == 1'b0)
 160         o <= i[6*W+:W];
 161        else
 162         o <= i[7*W+:W];
 163     else
 164      if (s[1] == 1'b0)
 165       if (s[2] == 1'b0)
 166        if (s[3] == 1'b0)
 167         o <= i[8*W+:W];
 168 end
 169 endmodule
 170 EOT
 171 prep
 172 design -save gold
 173
 174 techmap
 175 muxcover -mux4=150 -mux8=200 -mux16=250
 176 clean
 177 opt_expr -mux_bool
 178 select -assert-count 0 t:$_MUX_
 179 select -assert-count 0 t:$_MUX4_
 180 select -assert-count 0 t:$_MUX8_
 181 select -assert-count 1 t:$_MUX16_
 182 techmap -map +/simcells.v t:$_MUX16_
 183 design -stash gate
 184
 185 design -import gold -as gold
 186 design -import gate -as gate
 187
 188 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 189 sat -verify -prove-asserts -show-ports miter
 190
 191 ## MUX2 in MUX4 :: https://github.com/YosysHQ/yosys/issues/1132
 192
 193 design -reset
 194 read_verilog -formal <<EOT
 195 module mux2in4(input [1:0] i, input s, output o);
 196     assign o = s ? i[1] : i[0];
 197 endmodule
 198 EOT
 199 prep
 200 design -save gold
 201
 202 techmap
 203 muxcover -mux4=99 -nodecode
 204 clean
 205 opt_expr -mux_bool
 206 select -assert-count 0 t:$_MUX_
 207 select -assert-count 1 t:$_MUX4_
 208 select -assert-count 0 t:$_MUX8_
 209 select -assert-count 0 t:$_MUX16_
 210 techmap -map +/simcells.v t:$_MUX4_
 211 design -stash gate
 212
 213 design -import gold -as gold
 214 design -import gate -as gate
 215
 216 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 217 sat -verify -prove-asserts -show-ports miter
 218
 219 ## MUX2 in MUX8 :: https://github.com/YosysHQ/yosys/issues/1132
 220
 221 design -reset
 222 read_verilog -formal <<EOT
 223 module mux2in8(input [1:0] i, input s, output o);
 224     assign o = s ? i[1] : i[0];
 225 endmodule
 226 EOT
 227 prep
 228 design -save gold
 229
 230 techmap
 231 muxcover -mux8=99 -nodecode
 232 clean
 233 opt_expr -mux_bool
 234 select -assert-count 0 t:$_MUX_
 235 select -assert-count 0 t:$_MUX4_
 236 select -assert-count 1 t:$_MUX8_
 237 select -assert-count 0 t:$_MUX16_
 238 techmap -map +/simcells.v t:$_MUX8_
 239 design -stash gate
 240
 241 design -import gold -as gold
 242 design -import gate -as gate
 243
 244 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 245 sat -verify -prove-asserts -show-ports miter
 246
 247 ## MUX4 in MUX8 :: https://github.com/YosysHQ/yosys/issues/1132
 248
 249 design -reset
 250 read_verilog -formal <<EOT
 251 module mux4in8(input [3:0] i, input [1:0] s, output o);
 252     assign o = s[1] ? (s[0] ? i[3] : i[2]) : (s[0] ? i[1] : i[0]);
 253 endmodule
 254 EOT
 255 prep
 256 design -save gold
 257
 258 techmap
 259 muxcover -mux8=299 -nodecode
 260 clean
 261 opt_expr -mux_bool
 262 select -assert-count 0 t:$_MUX_
 263 select -assert-count 0 t:$_MUX4_
 264 select -assert-count 1 t:$_MUX8_
 265 select -assert-count 0 t:$_MUX16_
 266 techmap -map +/simcells.v t:$_MUX8_
 267 design -stash gate
 268
 269 design -import gold -as gold
 270 design -import gate -as gate
 271
 272 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 273 sat -verify -prove-asserts -show-ports miter
 274
 275 ## MUX2 in MUX16 :: https://github.com/YosysHQ/yosys/issues/1132
 276
 277 design -reset
 278 read_verilog -formal <<EOT
 279 module mux2in16(input [1:0] i, input s, output o);
 280     assign o = s ? i[1] : i[0];
 281 endmodule
 282 EOT
 283 prep
 284 design -save gold
 285
 286 techmap
 287 muxcover -mux16=99 -nodecode
 288 clean
 289 opt_expr -mux_bool
 290 select -assert-count 0 t:$_MUX_
 291 select -assert-count 0 t:$_MUX4_
 292 select -assert-count 0 t:$_MUX8_
 293 select -assert-count 1 t:$_MUX16_
 294 techmap -map +/simcells.v t:$_MUX16_
 295 design -stash gate
 296
 297 design -import gold -as gold
 298 design -import gate -as gate
 299
 300 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 301 sat -verify -prove-asserts -show-ports miter
 302
 303 ## MUX4 in MUX16 :: https://github.com/YosysHQ/yosys/issues/1132
 304
 305 design -reset
 306 read_verilog -formal <<EOT
 307 module mux4in16(input [3:0] i, input [1:0] s, output o);
 308     assign o = s[1] ? (s[0] ? i[3] : i[2]) : (s[0] ? i[1] : i[0]);
 309 endmodule
 310 EOT
 311 prep
 312 design -save gold
 313
 314 techmap
 315 muxcover -mux16=299 -nodecode
 316 clean
 317 opt_expr -mux_bool
 318 select -assert-count 0 t:$_MUX_
 319 select -assert-count 0 t:$_MUX4_
 320 select -assert-count 0 t:$_MUX8_
 321 select -assert-count 1 t:$_MUX16_
 322 techmap -map +/simcells.v t:$_MUX16_
 323 design -stash gate
 324
 325 design -import gold -as gold
 326 design -import gate -as gate
 327
 328 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 329 sat -verify -prove-asserts -show-ports miter
 330
 331 ## MUX8 in MUX16 :: https://github.com/YosysHQ/yosys/issues/1132
 332
 333 design -reset
 334 read_verilog -formal <<EOT
 335 module mux4in16(input [7:0] i, input [2:0] s, output o);
 336     assign o = s[2] ? s[1] ? (s[0] ? i[3] : i[2]) : (s[0] ? i[1] : i[0])
 337                     : s[1] ? (s[0] ? i[7] : i[6]) : (s[0] ? i[5] : i[4]);
 338 endmodule
 339 EOT
 340 prep
 341 design -save gold
 342
 343 techmap
 344 muxcover -mux16=699 -nodecode
 345 clean
 346 opt_expr -mux_bool
 347 select -assert-count 0 t:$_MUX_
 348 select -assert-count 0 t:$_MUX4_
 349 select -assert-count 0 t:$_MUX8_
 350 select -assert-count 1 t:$_MUX16_
 351 techmap -map +/simcells.v t:$_MUX16_
 352 design -stash gate
 353
 354 design -import gold -as gold
 355 design -import gate -as gate
 356
 357 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 358 sat -verify -prove-asserts -show-ports miter
 359
 360 ## mux_if_bal_5_1 :: https://github.com/YosysHQ/yosys/issues/1132
 361
 362 design -reset
 363 read_verilog -formal <<EOT
 364 module mux_if_bal_5_1 #(parameter N=5, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
 365 always @* begin
 366     o <= {{W{{1'bx}}}};
 367     if (s[0] == 1'b0)
 368      if (s[1] == 1'b0)
 369       if (s[2] == 1'b0)
 370        o <= i[0*W+:W];
 371       else
 372        o <= i[1*W+:W];
 373      else
 374       if (s[2] == 1'b0)
 375        o <= i[2*W+:W];
 376       else
 377        o <= i[3*W+:W];
 378     else
 379      if (s[1] == 1'b0)
 380       if (s[2] == 1'b0)
 381        o <= i[4*W+:W];
 382 end
 383 endmodule
 384 EOT
 385 prep
 386 design -save gold
 387
 388 wreduce
 389 opt -full
 390 techmap
 391 muxcover -mux8=350
 392 clean
 393 opt_expr -mux_bool
 394 select -assert-count 0 t:$_MUX_
 395 select -assert-count 0 t:$_MUX4_
 396 select -assert-count 1 t:$_MUX8_
 397 select -assert-count 0 t:$_MUX16_
 398 techmap -map +/simcells.v t:$_MUX8_
 399 design -stash gate
 400
 401 design -import gold -as gold
 402 design -import gate -as gate
 403
 404 miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold gate miter
 405 sat -verify -prove-asserts -show-ports miter
 406
 407 ## mux_if_bal_5_1 (nodecode) :: https://github.com/YosysHQ/yosys/issues/1132
 408 design -load gold
 409
 410 wreduce
 411 opt -full
 412 techmap
 413 muxcover -mux8=350 -nodecode
 414 clean
 415 opt_expr -mux_bool
 416 select -assert-count 0 t:$_MUX_
 417 select -assert-count 0 t:$_MUX4_
 418 select -assert-count 1 t:$_MUX8_
 419 select -assert-count 0 t:$_MUX16_
 420 techmap -map +/simcells.v t:$_MUX8_
 421 design -stash gate
 422
 423 design -import gold -as gold
 424 design -import gate -as gate
 425
 426 miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold gate miter
 427 sat -verify -prove-asserts -show-ports miter
 428
 429 ## mux_if_bal_9_1 :: https://github.com/YosysHQ/yosys/issues/1132
 430
 431 design -reset
 432 read_verilog -formal <<EOT
 433 module mux_if_bal_9_1 #(parameter N=9, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
 434 always @* begin
 435     o <= {{W{{1'bx}}}};
 436     if (s[3] == 1'b0)
 437      if (s[2] == 1'b0)
 438       if (s[1] == 1'b0)
 439        if (s[0] == 1'b0)
 440         o <= i[0*W+:W];
 441        else
 442         o <= i[1*W+:W];
 443       else
 444        if (s[0] == 1'b0)
 445         o <= i[2*W+:W];
 446        else
 447         o <= i[3*W+:W];
 448      else
 449       if (s[1] == 1'b0)
 450        if (s[0] == 1'b0)
 451         o <= i[4*W+:W];
 452        else
 453         o <= i[5*W+:W];
 454       else
 455        if (s[0] == 1'b0)
 456         o <= i[6*W+:W];
 457        else
 458         o <= i[7*W+:W];
 459     else
 460      if (s[2] == 1'b0)
 461       if (s[1] == 1'b0)
 462        if (s[0] == 1'b0)
 463         o <= i[8*W+:W];
 464 end
 465 endmodule
 466 EOT
 467 prep
 468 design -save gold
 469
 470 wreduce
 471 opt -full
 472 techmap
 473 muxcover -mux16=750
 474 clean
 475 opt_expr -mux_bool
 476 select -assert-count 0 t:$_MUX_
 477 select -assert-count 0 t:$_MUX4_
 478 select -assert-count 0 t:$_MUX8_
 479 select -assert-count 1 t:$_MUX16_
 480 techmap -map +/simcells.v t:$_MUX16_
 481 design -stash gate
 482
 483 design -import gold -as gold
 484 design -import gate -as gate
 485
 486 miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold gate miter
 487 sat -verify -prove-asserts -show-ports miter
 488
 489 ## mux_if_bal_9_1 (nodecode) :: https://github.com/YosysHQ/yosys/issues/1132
 490
 491 design -load gold
 492
 493 wreduce
 494 opt -full
 495 techmap
 496 muxcover -mux16=750 -nodecode
 497 clean
 498 opt_expr -mux_bool
 499 select -assert-count 0 t:$_MUX_
 500 select -assert-count 0 t:$_MUX4_
 501 select -assert-count 0 t:$_MUX8_
 502 select -assert-count 1 t:$_MUX16_
 503 techmap -map +/simcells.v t:$_MUX16_
 504 design -stash gate
 505
 506 design -import gold -as gold
 507 design -import gate -as gate
 508
 509 miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold gate miter
 510 sat -verify -prove-asserts -show-ports miter