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:*
  71
  72 ####################
  73
  74 design -reset
  75 read_verilog <<EOT
  76 module peepopt_dffmuxext_unsigned(input clk, ce, input [1:0] i, output reg [3:0] o);
  77     always @(posedge clk) if (ce) o <= i;
  78 endmodule
  79 EOT
  80
  81 proc
  82 equiv_opt -assert peepopt
  83 design -load postopt
  84 clean
  85 select -assert-count 1 t:$dff r:WIDTH=2 %i
  86 select -assert-count 1 t:$mux r:WIDTH=2 %i
  87 select -assert-count 0 t:$dff t:$mux %% t:* %D
  88
  89 ####################
  90
  91 design -reset
  92 read_verilog <<EOT
  93 module peepopt_dffmuxext_signed(input clk, ce, input signed [1:0] i, output reg signed [3:0] o);
  94     always @(posedge clk) if (ce) o <= i;
  95 endmodule
  96 EOT
  97
  98 proc
  99 equiv_opt -assert peepopt
 100 design -load postopt
 101 clean
 102 select -assert-count 1 t:$dff r:WIDTH=2 %i
 103 select -assert-count 1 t:$mux r:WIDTH=2 %i
 104 select -assert-count 0 t:$dff t:$mux %% t:* %D
 105
 106 ###################
 107
 108 design -reset
 109 read_verilog <<EOT
 110 module peepopt_dffmuxext_const(input clk, ce, input [1:0] i, output reg [5:0] o);
 111     always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz};
 112 endmodule
 113 EOT
 114
 115 proc
 116 equiv_opt -assert peepopt
 117 design -load postopt
 118 select -assert-count 1 t:$dff r:WIDTH=2 %i
 119 select -assert-count 1 t:$mux r:WIDTH=2 %i
 120 select -assert-count 0 t:$dff t:$mux %% t:* %D
 121
 122 ###################
 123
 124 design -reset
 125 read_verilog <<EOT
 126 module peepopt_dffmuxext_const_init(input clk, ce, input [1:0] i, (* init=6'b0x00x1 *) output reg [5:0] o);
 127     always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz};
 128 endmodule
 129 EOT
 130
 131 proc
 132 equiv_opt -assert peepopt
 133 design -load postopt
 134 select -assert-count 1 t:$dff r:WIDTH=4 %i
 135 select -assert-count 1 t:$mux r:WIDTH=4 %i
 136 select -assert-count 0 t:$dff t:$mux %% t:* %D
 137
 138 ####################
 139
 140 design -reset
 141 read_verilog <<EOT
 142 module peepopt_dffmuxext_unsigned_rst(input clk, ce, rst, input [1:0] i, output reg [3:0] o);
 143     always @(posedge clk) if (rst) o <= 0; else if (ce) o <= i;
 144 endmodule
 145 EOT
 146
 147 proc
 148 equiv_opt -assert peepopt
 149 design -load postopt
 150 wreduce
 151 select -assert-count 1 t:$dff r:WIDTH=2 %i
 152 select -assert-count 2 t:$mux
 153 select -assert-count 2 t:$mux r:WIDTH=2 %i
 154 select -assert-count 0 t:$dff t:$mux %% t:* %D
 155
 156 ####################
 157
 158 design -reset
 159 read_verilog <<EOT
 160 module peepopt_dffmuxext_signed_rst(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o);
 161     always @(posedge clk) begin
 162         if (ce) o <= i;
 163         if (!rstn) o <= 4'b1111;
 164     end
 165 endmodule
 166 EOT
 167
 168 proc
 169 equiv_opt -assert peepopt
 170 design -load postopt
 171 wreduce
 172 select -assert-count 1 t:$dff r:WIDTH=2 %i
 173 select -assert-count 2 t:$mux
 174 select -assert-count 2 t:$mux r:WIDTH=2 %i
 175 select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D
 176
 177 ####################
 178
 179 design -reset
 180 read_verilog <<EOT
 181 module peepopt_dffmuxext_signed_rst_init(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o);
 182     initial o <= 4'b0010;
 183     always @(posedge clk) begin
 184         if (ce) o <= i;
 185         if (!rstn) o <= 4'b1111;
 186     end
 187 endmodule
 188 EOT
 189
 190 proc
 191 # NB: equiv_opt uses equiv_induct which covers
 192 #     only the induction half of temporal induction
 193 #     --- missing the base-case half
 194 #     This makes it akin to `sat -tempinduct-inductonly`
 195 #     instead of `sat -tempinduct-baseonly` or
 196 #     `sat -tempinduct` which is necessary for this
 197 #     testcase
 198 #equiv_opt -assert peepopt
 199
 200 design -save gold
 201 peepopt
 202 wreduce
 203 design -stash gate
 204 design -import gold -as gold
 205 design -import gate -as gate
 206 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 207 sat -tempinduct -verify -prove-asserts -show-ports miter
 208
 209 design -load gate
 210 select -assert-count 1 t:$dff r:WIDTH=4 %i
 211 select -assert-count 2 t:$mux
 212 select -assert-count 2 t:$mux r:WIDTH=4 %i
 213 select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D