tests/opt/opt_expr_xor.ys

   1 read_verilog <<EOT
   2 module top(input a, output [3:0] y);
   3 assign y[0] = a^1'b0;
   4 assign y[1] = 1'b1^a;
   5 assign y[2] = a~^1'b0;
   6 assign y[3] = 1'b1^~a;
   7 endmodule
   8 EOT
   9 design -save read
  10 select -assert-count 2 t:$xor
  11 select -assert-count 2 t:$xnor
  12
  13 equiv_opt opt_expr
  14 design -load postopt
  15 select -assert-none t:$xor
  16 select -assert-none t:$xnor
  17 select -assert-count 2 t:$not
  18
  19
  20 design -load read
  21 simplemap
  22 equiv_opt opt_expr
  23 design -load postopt
  24 select -assert-none t:$_XOR_
  25 select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_
  26 select -assert-count 3 t:$_NOT_
  27
  28
  29 design -reset
  30 read_verilog -icells <<EOT
  31 module top(input a, output [1:0] y);
  32 $_XNOR_ u0(.A(a), .B(1'b0), .Y(y[0]));
  33 $_XNOR_ u1(.A(1'b1), .B(a), .Y(y[1]));
  34 endmodule
  35 EOT
  36 select -assert-count 2 t:$_XNOR_
  37 equiv_opt opt_expr
  38 design -load postopt
  39 select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_
  40 select -assert-count 1 t:$_NOT_
  41
  42
  43 design -reset
  44 read_verilog <<EOT
  45 module top(input a, output [1:0] w, x, y, z);
  46 assign w = a^1'b0;
  47 assign x = a^1'b1;
  48 assign y = a~^1'b0;
  49 assign z = a~^1'b1;
  50 endmodule
  51 EOT
  52 equiv_opt opt_expr
  53
  54
  55 # Single-bit $xor
  56 design -reset
  57 read_verilog -noopt <<EOT
  58 module gold(input i, output o);
  59 assign o = 1'bx ^ i;
  60 endmodule
  61 EOT
  62 select -assert-count 1 t:$xor
  63 copy gold coarse
  64 copy gold fine
  65 copy gold coarse_keepdc
  66 copy gold fine_keepdc
  67
  68 cd coarse
  69 opt_expr
  70 select -assert-none c:*
  71
  72 cd fine
  73 simplemap
  74 opt_expr
  75 select -assert-none c:*
  76
  77 cd
  78 miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
  79 sat -verify -prove-asserts -show-ports -enable_undef miter
  80 miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
  81 sat -verify -prove-asserts -show-ports -enable_undef miter2
  82
  83 cd coarse_keepdc
  84 opt_expr -keepdc
  85 select -assert-count 1 c:*
  86
  87 cd fine_keepdc
  88 simplemap
  89 opt_expr -keepdc
  90 select -assert-count 1 c:*
  91
  92 cd
  93 miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
  94 sat -verify -prove-asserts -show-ports -enable_undef miter3
  95 miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
  96 sat -verify -prove-asserts -show-ports -enable_undef miter4
  97
  98
  99 # Multi-bit $xor
 100 design -reset
 101 read_verilog -noopt <<EOT
 102 module gold(input i, output [6:0] o);
 103 assign o = {1'bx, 1'b0, 1'b0, 1'b1, 1'bx, 1'b1, i} ^ {7{i}};
 104 endmodule
 105 EOT
 106 select -assert-count 1 t:$xor
 107 copy gold coarse
 108 copy gold fine
 109 copy gold coarse_keepdc
 110 copy gold fine_keepdc
 111
 112 cd coarse
 113 opt_expr -fine
 114 select -assert-count 0 t:$xor
 115
 116 cd fine
 117 simplemap
 118 opt_expr
 119 select -assert-none t:$_XOR_
 120
 121 cd
 122 miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
 123 sat -verify -prove-asserts -show-ports -enable_undef miter
 124 miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
 125 sat -verify -prove-asserts -show-ports -enable_undef miter2
 126
 127 cd coarse_keepdc
 128 opt_expr -keepdc -fine
 129 select -assert-count 1 t:$xor
 130
 131 cd fine_keepdc
 132 simplemap
 133 opt_expr -keepdc
 134 select -assert-count 3 t:$_XOR_
 135
 136 cd
 137 miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
 138 sat -verify -prove-asserts -show-ports -enable_undef miter3
 139 miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
 140 sat -verify -prove-asserts -show-ports -enable_undef miter4