tests/opt/opt_expr_xnor.ys

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