abstract: test -slice for all modes, -rtlilslice for -init

tests/various/abstract_init.ys

@@ -37,3 +37,79 @@ select -assert-count 1 w:Q a:init=2'b01 %i
 abstract -init w:QQQ
 check -assert
 select -assert-count 1 w:Q a:init=2'b0x %i
+
+design -reset
+read_verilog <<EOT
+module foo (CLK, Q);
+	input CLK;
+	//         downto
+	output reg [1:0] Q = 1'b1;
+	always @(posedge CLK)
+		Q <= ~Q;
+endmodule
+EOT
+
+proc
+opt_expr
+opt_dff
+select -assert-count 1 w:Q a:init=2'b01 %i
+abstract -init -slice 0 w:Q
+check -assert
+select -assert-count 1 w:Q a:init=2'b0x %i
+
+design -reset
+read_verilog <<EOT
+module foo (CLK, Q);
+	input CLK;
+	//         downto
+	output reg [1:0] Q = 1'b1;
+	always @(posedge CLK)
+		Q <= ~Q;
+endmodule
+EOT
+
+proc
+opt_expr
+opt_dff
+select -assert-count 1 w:Q a:init=2'b01 %i
+abstract -init -rtlilslice 0 w:Q
+check -assert
+select -assert-count 1 w:Q a:init=2'b0x %i
+
+design -reset
+read_verilog <<EOT
+module foo (CLK, Q);
+	input CLK;
+	//         upto
+	output reg [0:1] Q = 1'b1;
+	always @(posedge CLK)
+		Q <= ~Q;
+endmodule
+EOT
+
+proc
+opt_expr
+opt_dff
+select -assert-count 1 w:Q a:init=2'b01 %i
+abstract -init -slice 0 w:Q
+check -assert
+select -assert-count 1 w:Q a:init=2'bx1 %i
+
+design -reset
+read_verilog <<EOT
+module foo (CLK, Q);
+	input CLK;
+	//         upto
+	output reg [0:1] Q = 1'b1;
+	always @(posedge CLK)
+		Q <= ~Q;
+endmodule
+EOT
+
+proc
+opt_expr
+opt_dff
+select -assert-count 1 w:Q a:init=2'b01 %i
+abstract -init -rtlilslice 0 w:Q
+check -assert
+select -assert-count 1 w:Q a:init=2'b0x %i

tests/various/abstract_state.ys

@@ -62,6 +62,39 @@ select -assert-count 1 @not %x:+[A] o:Q %i
 # -----------------------------------------------------------------------------
 design -reset
 read_verilog <<EOT
+module wide_flop_no_q (CLK, DDD, QQQ, magic);
+	input CLK;
+	input [2:0] DDD;
+	output reg [2:0] QQQ;
+	input magic;
+	always @(posedge CLK)
+		QQQ <= DDD;
+endmodule
+EOT
+proc
+opt_expr
+opt_dff
+dump
+abstract -state -enablen magic -slice 0 w:QQQ
+check -assert
+# Connections to dff D input port
+select -set conn_to_d t:$dff %x:+[D] t:$dff %d
+# The D input port is partially fed with a mux
+select -set mux @conn_to_d %ci t:$mux %i
+select -assert-count 1 @mux
+# and also the DDD input
+select -assert-count 1 @conn_to_d w:DDD %i
+# The S input port is fed with the magic wire
+select -assert-count 1 @mux %x:+[S] w:magic %i
+# The A input port is fed with an anyseq
+select -assert-count 1 @mux %x:+[A] %ci t:$anyseq %i
+# The B input port is fed with DDD
+select -assert-count 1 @mux %x:+[B] %ci w:DDD %i
+# -----------------------------------------------------------------------------
+# Selecting wire Q connected to bit 0 of QQQ is the same as specifying
+# QQQ with the -slice 0 argument
+design -reset
+read_verilog <<EOT
 module wide_flop (CLK, DDD, QQQ, Q, magic);
 	input CLK;
 	input [2:0] DDD;
@@ -78,18 +111,13 @@ design -save wide_flop
 # Test that abstracting an output slice muxes an input slice
 abstract -state -enablen magic w:Q
 check -assert
-# Connections to dff D input port
+# Same testing as previous case
 select -set conn_to_d t:$dff %x:+[D] t:$dff %d
-# The D input port is partially fed with a mux
 select -set mux @conn_to_d %ci t:$mux %i
 select -assert-count 1 @mux
-# and also the DDD input
 select -assert-count 1 @conn_to_d w:DDD %i
-# The S input port is fed with the magic wire
 select -assert-count 1 @mux %x:+[S] w:magic %i
-# The A input port is fed with an anyseq
 select -assert-count 1 @mux %x:+[A] %ci t:$anyseq %i
-# The B input port is fed with DDD
 select -assert-count 1 @mux %x:+[B] %ci w:DDD %i
 # -----------------------------------------------------------------------------
 design -reset

tests/various/abstract_value.ys

@@ -13,7 +13,6 @@ proc
 design -save split_output
 # Basic -value test
 abstract -value -enable magic w:W
-# show
 check -assert
 # Connections to $add Y output port
 select -set conn_to_y t:$add %x:+[Y] t:$add %d
@@ -29,6 +28,29 @@ select -assert-count 1 @mux %x:+[B] %ci t:$anyseq %i
 # The Y output port feeds into the Y module output
 select -assert-count 1 @mux %x:+[Y] %co o:Y %i
 # -----------------------------------------------------------------------------
+# Same thing, but we use -slice instead of wire W
+design -reset
+read_verilog <<EOT
+module split_output_no_w (A, B, Y, magic);
+	input [1:0] A;
+	input [1:0] B;
+	output [1:0] Y;
+	input magic;
+    assign Y = A + B;
+endmodule
+EOT
+proc
+# Same test as the previous case
+abstract -value -enable magic -slice 0 w:Y
+check -assert
+select -set conn_to_y t:$add %x:+[Y] t:$add %d
+select -set mux @conn_to_y %ci t:$mux %i
+select -assert-count 1 @mux
+select -assert-count 1 @conn_to_y %a o:Y %i
+select -assert-count 1 @mux %x:+[S] w:magic %i
+select -assert-count 1 @mux %x:+[B] %ci t:$anyseq %i
+select -assert-count 1 @mux %x:+[Y] %co o:Y %i
+# -----------------------------------------------------------------------------
 design -reset
 read_verilog <<EOT
 module split_input (A, B, Y, magic);
@@ -45,7 +67,6 @@ proc
 design -save split_input
 # The mux goes on an input this time
 abstract -value -enable magic w:W
-# show
 check -assert
 # Connections to add A input port
 select -set conn_to_a t:$add %x:+[A] t:$add %d