tests/opt/opt_dff_dffmux.ys

   1 design -reset
   2 read_verilog <<EOT
   3 module opt_dffmuxext_unsigned(input clk, ce, input [1:0] i, output reg [3:0] o);
   4     always @(posedge clk) if (ce) o <= i;
   5 endmodule
   6 EOT
   7
   8 proc
   9 equiv_opt -assert opt
  10 design -load postopt
  11 select -assert-count 1 t:$dffe r:WIDTH=2 %i
  12 select -assert-count 0 t:$dffe %% t:* %D
  13
  14 ####################
  15
  16 design -reset
  17 read_verilog <<EOT
  18 module opt_dffmuxext_signed(input clk, ce, input signed [1:0] i, output reg signed [3:0] o);
  19     always @(posedge clk) if (ce) o <= i;
  20 endmodule
  21 EOT
  22
  23 proc
  24 equiv_opt -assert opt
  25 design -load postopt
  26 wreduce
  27 select -assert-count 1 t:$dffe r:WIDTH=2 %i
  28 select -assert-count 0 t:$dffe %% t:* %D
  29
  30 ###################
  31
  32 design -reset
  33 read_verilog <<EOT
  34 module opt_dffmuxext_const(input clk, ce, input [1:0] i, output reg [5:0] o);
  35     always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz};
  36 endmodule
  37 EOT
  38
  39 proc
  40 equiv_opt -assert opt
  41 design -load postopt
  42 select -assert-count 1 t:$dffe r:WIDTH=2 %i
  43 select -assert-count 0 t:$dffe %% t:* %D
  44
  45 ###################
  46
  47 design -reset
  48 read_verilog <<EOT
  49 module opt_dffmuxext_const_init(input clk, ce, input [1:0] i, (* init=6'b0x00x1 *) output reg [5:0] o);
  50     always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz};
  51 endmodule
  52 EOT
  53
  54 proc
  55 equiv_opt -assert opt
  56 design -load postopt
  57 select -assert-count 1 t:$dffe r:WIDTH=4 %i
  58 select -assert-count 0 t:$dffe %% t:* %D
  59
  60 ####################
  61
  62 design -reset
  63 read_verilog <<EOT
  64 module opt_dffmuxext_unsigned_rst(input clk, ce, rst, input [1:0] i, output reg [3:0] o);
  65     always @(posedge clk) if (rst) o <= 0; else if (ce) o <= i;
  66 endmodule
  67 EOT
  68
  69 proc
  70 equiv_opt -assert opt
  71 design -load postopt
  72 wreduce
  73 select -assert-count 1 t:$sdffe r:WIDTH=2 %i
  74 select -assert-count 0 t:$sdffe %% t:* %D
  75
  76 ####################
  77
  78 design -reset
  79 read_verilog <<EOT
  80 module opt_dffmuxext_signed_rst(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o);
  81     always @(posedge clk) begin
  82         if (ce) o <= i;
  83         if (!rstn) o <= 4'b1111;
  84     end
  85 endmodule
  86 EOT
  87
  88 proc
  89 equiv_opt -assert opt
  90 design -load postopt
  91 wreduce
  92 select -assert-count 1 t:$sdffe r:WIDTH=2 %i
  93 select -assert-count 0 t:$sdffe %% t:* %D
  94
  95 ####################
  96
  97 design -reset
  98 read_verilog <<EOT
  99 module opt_dffmuxext_signed_rst_init(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o);
 100     initial o <= 4'b0010;
 101     always @(posedge clk) begin
 102         if (ce) o <= i;
 103         if (!rstn) o <= 4'b1111;
 104     end
 105 endmodule
 106 EOT
 107
 108 proc
 109 # NB: equiv_opt uses equiv_induct which covers
 110 #     only the induction half of temporal induction
 111 #     --- missing the base-case half
 112 #     This makes it akin to `sat -tempinduct-inductonly`
 113 #     instead of `sat -tempinduct-baseonly` or
 114 #     `sat -tempinduct` which is necessary for this
 115 #     testcase
 116 #equiv_opt -assert opt
 117
 118 design -save gold
 119 opt
 120 wreduce
 121 design -stash gate
 122 design -import gold -as gold
 123 design -import gate -as gate
 124 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 125 sat -tempinduct -verify -prove-asserts -show-ports miter
 126
 127 design -load gate
 128 select -assert-count 1 t:$sdffe r:WIDTH=3 %i
 129 select -assert-count 0 t:$sdffe %% t:* %D