tests/various/peepopt.ys

   1 read_verilog <<EOT
   2 module peepopt_shiftmul_0 #(parameter N=3, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output [W-1:0] o);
   3 assign o = i[s*W+:W];
   4 endmodule
   5 EOT
   6
   7 prep -nokeepdc
   8 equiv_opt -assert peepopt
   9 design -load postopt
  10 clean
  11 select -assert-count 1 t:$shiftx
  12 select -assert-count 0 t:$shiftx t:* %D
  13
  14 ####################
  15
  16 design -reset
  17 read_verilog <<EOT
  18 module peepopt_shiftmul_1 (output [7:0] y, input [2:0] w);
  19 assign y = 1'b1 >> (w * (3'b110));
  20 endmodule
  21 EOT
  22
  23 prep -nokeepdc
  24 equiv_opt -assert peepopt
  25 design -load postopt
  26 clean
  27 select -assert-count 1 t:$shr
  28 select -assert-count 1 t:$mul
  29 select -assert-count 0 t:$shr t:$mul %% t:* %D
  30
  31 ####################
  32
  33 design -reset
  34 read_verilog <<EOT
  35 module peepopt_shiftmul_2 (input [11:0] D, input [1:0] S, output [11:0] Y);
  36         assign Y = D >> (S*3);
  37 endmodule
  38 EOT
  39
  40 prep
  41 design -save gold
  42 peepopt
  43 design -stash gate
  44
  45 design -import gold -as gold peepopt_shiftmul_2
  46 design -import gate -as gate peepopt_shiftmul_2
  47
  48 miter -equiv -make_assert -make_outputs -ignore_gold_x -flatten gold gate miter
  49 sat -show-public -enable_undef -prove-asserts miter
  50 cd gate
  51 select -assert-count 1 t:$shr
  52 select -assert-count 1 t:$mul
  53 select -assert-count 0 t:$shr t:$mul %% t:* %D
  54
  55 ####################
  56
  57 design -reset
  58 read_verilog <<EOT
  59 module peepopt_muldiv_0(input [1:0] i, output [1:0] o);
  60 wire [3:0] t;
  61 assign t = i * 3;
  62 assign o = t / 3;
  63 endmodule
  64 EOT
  65
  66 prep -nokeepdc
  67 equiv_opt -assert peepopt
  68 design -load postopt
  69 clean
  70 select -assert-count 0 t:*