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