design -reset
read_verilog <<EOT
module opt_dffmuxext_unsigned(input clk, ce, input [1:0] i, output reg [3:0] o);
    always @(posedge clk) if (ce) o <= i;
endmodule
EOT

proc
equiv_opt -assert opt
design -load postopt
select -assert-count 1 t:$dffe r:WIDTH=2 %i
select -assert-count 0 t:$dffe %% t:* %D

####################

design -reset
read_verilog <<EOT
module opt_dffmuxext_signed(input clk, ce, input signed [1:0] i, output reg signed [3:0] o);
    always @(posedge clk) if (ce) o <= i;
endmodule
EOT

proc
equiv_opt -assert opt
design -load postopt
wreduce
select -assert-count 1 t:$dffe r:WIDTH=2 %i
select -assert-count 0 t:$dffe %% t:* %D

###################

design -reset
read_verilog <<EOT
module opt_dffmuxext_const(input clk, ce, input [1:0] i, output reg [5:0] o);
    always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz};
endmodule
EOT

proc
equiv_opt -assert opt
design -load postopt
select -assert-count 1 t:$dffe r:WIDTH=2 %i
select -assert-count 0 t:$dffe %% t:* %D

###################

design -reset
read_verilog <<EOT
module opt_dffmuxext_const_init(input clk, ce, input [1:0] i, (* init=6'b0x00x1 *) output reg [5:0] o);
    always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz};
endmodule
EOT

proc
equiv_opt -assert opt
design -load postopt
select -assert-count 1 t:$dffe r:WIDTH=4 %i
select -assert-count 0 t:$dffe %% t:* %D

####################

design -reset
read_verilog <<EOT
module opt_dffmuxext_unsigned_rst(input clk, ce, rst, input [1:0] i, output reg [3:0] o);
    always @(posedge clk) if (rst) o <= 0; else if (ce) o <= i;
endmodule
EOT

proc
equiv_opt -assert opt
design -load postopt
wreduce
select -assert-count 1 t:$sdffe r:WIDTH=2 %i
select -assert-count 0 t:$sdffe %% t:* %D

####################

design -reset
read_verilog <<EOT
module opt_dffmuxext_signed_rst(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o);
    always @(posedge clk) begin
        if (ce) o <= i;
        if (!rstn) o <= 4'b1111;
    end
endmodule
EOT

proc
equiv_opt -assert opt
design -load postopt
wreduce
select -assert-count 1 t:$sdffe r:WIDTH=2 %i
select -assert-count 0 t:$sdffe %% t:* %D

####################

design -reset
read_verilog <<EOT
module opt_dffmuxext_signed_rst_init(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o);
    initial o <= 4'b0010;
    always @(posedge clk) begin
        if (ce) o <= i;
        if (!rstn) o <= 4'b1111;
    end
endmodule
EOT

proc
# NB: equiv_opt uses equiv_induct which covers
#     only the induction half of temporal induction
#     --- missing the base-case half
#     This makes it akin to `sat -tempinduct-inductonly`
#     instead of `sat -tempinduct-baseonly` or
#     `sat -tempinduct` which is necessary for this
#     testcase
#equiv_opt -assert opt

design -save gold
opt
wreduce
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -tempinduct -verify -prove-asserts -show-ports miter

design -load gate
select -assert-count 1 t:$sdffe r:WIDTH=3 %i
select -assert-count 0 t:$sdffe %% t:* %D