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 select -assert-count 0 t:$_MUX_
 119 select -assert-count 0 t:$_MUX4_
 120 select -assert-count 1 t:$_MUX8_
 121 select -assert-count 0 t:$_MUX16_
 122 techmap -map +/simcells.v t:$_MUX8_
 123 design -stash gate
 124
 125 design -import gold -as gold
 126 design -import gate -as gate
 127
 128 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 129 sat -verify -prove-asserts -show-ports miter
 130
 131 ## Partial matching MUX16
 132
 133 design -reset
 134 read_verilog -formal <<EOT
 135 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);
 136 always @* begin
 137     o <= {{W{{1'bx}}}};
 138     if (s[0] == 1'b0)
 139      if (s[1] == 1'b0)
 140       if (s[2] == 1'b0)
 141        if (s[3] == 1'b0)
 142         o <= i[0*W+:W];
 143        else
 144         o <= i[1*W+:W];
 145       else
 146        if (s[3] == 1'b0)
 147         o <= i[2*W+:W];
 148        else
 149         o <= i[3*W+:W];
 150      else
 151       if (s[2] == 1'b0)
 152        if (s[3] == 1'b0)
 153         o <= i[4*W+:W];
 154        else
 155         o <= i[5*W+:W];
 156       else
 157        if (s[3] == 1'b0)
 158         o <= i[6*W+:W];
 159        else
 160         o <= i[7*W+:W];
 161     else
 162      if (s[1] == 1'b0)
 163       if (s[2] == 1'b0)
 164        if (s[3] == 1'b0)
 165         o <= i[8*W+:W];
 166 end
 167 endmodule
 168 EOT
 169 prep
 170 design -save gold
 171
 172 techmap
 173 muxcover -mux4=150 -mux8=200 -mux16=250
 174 select -assert-count 0 t:$_MUX_
 175 select -assert-count 0 t:$_MUX4_
 176 select -assert-count 0 t:$_MUX8_
 177 select -assert-count 1 t:$_MUX16_
 178 techmap -map +/simcells.v t:$_MUX16_
 179 design -stash gate
 180
 181 design -import gold -as gold
 182 design -import gate -as gate
 183
 184 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 185 sat -verify -prove-asserts -show-ports miter
 186