Review 'misc' test group (help - select)

misc_reviewed/help/help.ys

+tee -q -o result.log help

misc_reviewed/help/help_all.ys

+tee -q -o result.log help -all

misc_reviewed/help/help_cells.ys

+tee -q -o result.log help -cells

misc_reviewed/help/help_celltype.pat

+    $dff (CLK, D, Q)
+
+No help message for this cell type found.
+
+Run 'help $dff+' to display the Verilog model for this cell type.

misc_reviewed/help/help_celltype.ys

+tee -q -o result.out help $dff

misc_reviewed/help/help_celltype_plus.pat

+module \\$dff (CLK, D, Q);
+
+    parameter WIDTH = 0;
+    parameter CLK_POLARITY = 1'b1;
+
+    input CLK;
+    input \[WIDTH-1:0\] D;
+    output reg \[WIDTH-1:0\] Q;
+    wire pos_clk = CLK == CLK_POLARITY;
+
+    always @(posedge pos_clk) begin
+        Q <= D;
+    end
+
+endmodule

misc_reviewed/help/help_celltype_plus.ys

+tee -q -o result.out help $dff+

misc_reviewed/help/help_command.pat

+read_verilog \[options\] \[filename\]

misc_reviewed/help/help_command.ys

+tee -q -o result.out help read_verilog

misc_reviewed/help/help_no_such_command.pat

+No such command or cell type: u

misc_reviewed/help/help_no_such_command.ys

+tee -q -o result.out help u

misc_reviewed/hilomap/hilomap.ys

+read_verilog ../top.v
+proc
+hilomap
+select -assert-count 1 t:$dffsr
+select -assert-count 4 t:$mux
+select -assert-count 2 t:$not
+select -assert-count 2 t:dffsr
+select -assert-none t:$dffsr t:$mux t:$not t:dffsr %% t:* %D

misc_reviewed/hilomap/hilomap_hicell.ys

+read_verilog ../top.v
+proc
+hilomap -hicell VCC V
+select -assert-count 4 t:VCC
+select -assert-count 0 t:GND

misc_reviewed/hilomap/hilomap_hicell_locell_singleton.ys

+read_verilog ../top.v
+proc
+hilomap -locell GND G -hicell VCC V -singleton
+
+select assert-count 1 t:VCC
+select assert-count 1 t:GND

misc_reviewed/hilomap/hilomap_hicell_singleton.ys

+read_verilog ../top.v
+proc
+hilomap -hicell VCC V -singleton
+
+select -assert-count 2 t:VCC
+select -assert-count 0 t:GND

misc_reviewed/hilomap/hilomap_locell.ys

+read_verilog ../top.v
+proc
+hilomap -locell GND G
+select -assert-count 0 t:VCC
+select -assert-count 6 t:GND

misc_reviewed/hilomap/hilomap_locell_singleton.ys

+read_verilog ../top.v
+proc
+hilomap -locell GND G -singleton
+select -assert-count 0 t:VCC
+select -assert-count 2 t:GND

misc_reviewed/hilomap/hilomap_singleton.ys

+read_verilog ../top.v
+proc
+hilomap -singleton

misc_reviewed/hilomap/top.v

+module dffsr
+    ( input d, clk, pre, clr, output reg q );
+	always @( posedge clk, posedge pre, posedge clr )
+		if ( pre )
+			q <= 1'b1;
+		else if ( clr )
+			q <= 1'b0;
+		else
+            q <= d;
+endmodule
+
+module top (
+input clk,
+input a,
+output b,b2
+);
+
+dffsr u_dffsr (
+        .clk (clk ),
+        .clr (1'b0),
+        .pre (1'b1),
+        .d (a ),
+        .q (b )
+    );
+
+dffsr u2_dffsr (
+        .clk (clk ),
+        .clr (1'b0),
+        .pre (1'b1),
+        .d (a ),
+        .q (b2 )
+    );
+
+endmodule

misc_reviewed/history/history.ys

+read_verilog ../top.v
+proc
+synth
+synth_xilinx
+tee -o result.out  history

misc_reviewed/history/top.v

+(* black_box *) module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output A,
+ output cout
+ );
+
+assign {cout,A} =  cin + y + x;
+
+endmodule

misc_reviewed/insbuf/insbuf.ys

+read_verilog ../top.v
+synth
+insbuf
+select -assert-count 1 t:$_BUF_

misc_reviewed/insbuf/insbuf_cell.ys

+read_verilog ../top.v
+synth
+insbuf -buf $_NOT_ A Y
+select -assert-count 1 t:$_NOT_

misc_reviewed/insbuf/insbuf_unknown_arg.ys

+read_verilog ../top.v
+synth
+insbuf buf

misc_reviewed/insbuf/insbuf_wide.ys

+read_verilog ../top_wide.v
+synth
+insbuf
+select -assert-count 16 t:$_BUF_

misc_reviewed/insbuf/top.v

+module top    (
+out,
+i,
+clk,
+o,
+in
+);
+    output [7:0] out;
+    input clk, in;
+    reg [7:0] out;
+    input i;
+    output o;
+
+    always @(posedge clk)
+	begin
+		out    <= out << 1;
+		out[0] <= in;
+	end
+
+endmodule

misc_reviewed/insbuf/top_wide.v

+module top    (
+out,
+in
+);
+    output [7:0] out;
+    input [7:0] in;
+
+    wire [7:0] o;
+
+	assign o  = in;
+
+	assign out = o;
+
+endmodule

misc_reviewed/log/log.ys

+tee -o result.log log "OK"

misc_reviewed/log/log_n.ys

+tee -o result.log log -n "OK"

misc_reviewed/log/log_nolog.ys

+tee -o result.log log -nolog "OK"

misc_reviewed/log/log_stderr.ys

+tee -o result.log log -stderr "OK"

misc_reviewed/log/log_stdout.ys

+tee -o result.log log -stdout "OK"

misc_reviewed/ltp/ltp.pat

+Longest topological path in top (length=3):
+    0: \\x
+    1: $add$../top.v:13$2_Y (via $add$../top.v:13$2)
+    2: \\A (via $procdff$4)
+    3: $add$../top.v:15$3_Y (via $add$../top.v:15$3)

misc_reviewed/ltp/ltp.ys

+read_verilog ../top.v
+proc
+tee -o result.out ltp

misc_reviewed/ltp/ltp_loop.pat

+Warning: Detected loop at $and$../top_logic_loop.v:13$1_Y in top
+
+Longest topological path in top (length=3):
+    0: \\x
+    1: $and$../top_logic_loop.v:13$1_Y (via $and$../top_logic_loop.v:13$1)
+    2: $and$../top_logic_loop.v:14$2_Y (via $and$../top_logic_loop.v:14$2)
+    3: $not$../top_logic_loop.v:15$3_Y (via $not$../top_logic_loop.v:15$3)

misc_reviewed/ltp/ltp_loop.ys

+read_verilog ../top_logic_loop.v
+proc
+tee -o result.out ltp

misc_reviewed/ltp/ltp_noff.pat

+Longest topological path in top (length=1):
+    0: \\x
+    1: $add$../top.v:13$2_Y (via $add$../top.v:13$2)
+   ff: \\A (via $procdff$4)

misc_reviewed/ltp/ltp_noff.ys

+read_verilog ../top.v
+proc
+tee -o result.out ltp -noff

misc_reviewed/ltp/ltp_noproc.pat

+Warning: Ignoring module top because it contains processes (run 'proc' command first).

misc_reviewed/ltp/ltp_noproc.ys

+read_verilog ../top.v
+tee -o result.out ltp

misc_reviewed/ltp/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output cout
+ );
+ wire o;
+
+always @(posedge cin)
+	A <= y + x;
+
+assign cout =  cin + A;
+
+endmodule

misc_reviewed/ltp/top_logic_loop.v

+module top
+(
+ input x,
+ input y,
+ input z,
+
+ output A,
+ output B
+ );
+
+ wire A1,B1,A2,B2;
+
+ assign A1 = x & A2;
+ assign A2 = A1 & y;
+ assign A = ~A2;
+
+endmodule

misc_reviewed/miter/miter_assert.ys

+read_verilog -sv ../top.v
+proc
+tee -o result.log miter -assert -make_outputs top
+tee -o result.log miter -assert -make_outputs middle

misc_reviewed/miter/miter_assert_assert.ys

+read_verilog -sv ../top_assert.v
+proc
+tee -o result.log miter -assert -make_outputs top miter
+tee -o result.log miter -assert -make_outputs middle

misc_reviewed/miter/miter_assert_flatten.ys

+read_verilog -sv ../top.v
+proc
+tee -o result.log miter -assert -flatten top
+tee -o result.log miter -assert -flatten middle

misc_reviewed/miter/miter_cant_find_gate_module_fail.pat

+ERROR: Can't find gate module \\gate!

misc_reviewed/miter/miter_cant_find_gate_module_fail.ys

+read_verilog -sv ../top.v
+proc
+tee -o result.log miter -equiv top gate top

misc_reviewed/miter/miter_cant_find_gold_module_fail.pat

+ERROR: Can't find gold module \\gold!

misc_reviewed/miter/miter_cant_find_gold_module_fail.ys

+read_verilog -sv ../top.v
+proc
+tee -o result.log miter -equiv gold gate top

misc_reviewed/miter/miter_cant_find_module_fail.pat

+ERROR: Can't find module \\t!

misc_reviewed/miter/miter_cant_find_module_fail.ys

+read_verilog -sv ../top.v
+proc
+tee -o result.log miter -assert t

misc_reviewed/miter/miter_equiv.ys

+read_verilog ../top_equiv.v
+hierarchy -top dut
+proc
+memory -nomap
+equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5
+memory
+opt -full
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter

misc_reviewed/miter/miter_equiv_ignore_gold_x.ys

+read_verilog ../top_equiv.v
+hierarchy -top dut
+proc
+memory -nomap
+equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5
+memory
+opt -full
+
+miter -equiv -flatten -ignore_gold_x -make_assert -make_outputs gold gate miter

misc_reviewed/miter/miter_equiv_outcmp.ys

+read_verilog ../top_equiv.v
+hierarchy -top dut
+proc
+memory -nomap
+equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5
+memory
+opt -full
+
+miter -equiv -flatten -make_outcmp -make_assert -make_outputs gold gate miter

misc_reviewed/miter/miter_missing_mode_param_fail.pat

+ERROR: Missing mode parameter!

misc_reviewed/miter/miter_missing_mode_param_fail.ys

+read_verilog -sv ../top.v
+proc
+tee -o result.log miter

misc_reviewed/miter/miter_no_match_in_gate_fail.pat

+ERROR: No matching port in gate module was found for \\y!

misc_reviewed/miter/miter_no_match_in_gate_fail.ys

+read_verilog -sv ../top_err_1.v
+proc
+tee -o result.log miter -equiv middle u_rtl top1

misc_reviewed/miter/miter_no_match_in_gold_fail.pat

+ERROR: No matching port in gold module was found for \\y!

misc_reviewed/miter/miter_no_match_in_gold_fail.ys

+read_verilog -sv ../top_err_1.v
+proc
+tee -o result.log miter -equiv u_rtl middle top1

misc_reviewed/miter/miter_there_is_already_a_module_fail.pat

+ERROR: There is already a module \\top!

misc_reviewed/miter/miter_there_is_already_a_module_fail.ys

+read_verilog -sv ../top.v
+proc
+tee -o result.log miter -equiv top middle top

misc_reviewed/miter/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output cout
+ );
+ parameter X = 1;
+ wire o;
+
+`ifndef BUG
+always @(posedge cin)
+	A <= o;
+
+//assign cout =  cin? y : x;
+
+middle u_mid (.x(x),.o(o));
+u_rtl inst_u_rtl (.x(x),.o(o));
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule
+
+module middle
+(
+	input x,
+	input y,
+	output o
+);
+
+assign o = x + y;
+endmodule
+
+module u_rtl
+(
+	input x,
+	input y,
+	output o
+);
+
+assign o = x + y;
+endmodule

misc_reviewed/miter/top_assert.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout
+ );
+
+ reg ASSERT = 1;
+ (* anyconst *) reg foo;
+ (* anyseq *) reg too;
+
+
+
+ initial begin
+    begin
+        A = 0;
+        cout = 0;
+    end
+ end
+
+`ifndef BUG
+always @(posedge x) begin
+    if ($initstate)
+        A <= 0;
+    A <=  y + cin + too;
+    assume(too);
+    assume(s_eventually too);
+end
+always @(negedge x) begin
+    if ($initstate)
+        cout <= 0;
+        cout <=  y + A + foo;
+    assert(ASSERT);
+    assert(s_eventually ASSERT);
+end
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule
+
+module middle
+(
+	input x,
+	input y,
+	output o
+);
+
+assign o = x + y;
+endmodule

misc_reviewed/miter/top_equiv.v

+module dut(
+	input fast_clk, slow_clk,
+	input [3:0] waddr, raddr,
+	input [3:0] wdata,
+	input wen,
+	output [3:0] rdata
+);
+
+	reg [3:0] mem[0:15];
+	reg [3:0] raddr_reg;
+
+	always @(posedge fast_clk) begin
+		if (wen)
+			mem[waddr] <= wdata;
+	end
+
+	always @(posedge slow_clk)
+		raddr_reg <= raddr;
+
+	assign rdata = mem[raddr_reg];
+endmodule

misc_reviewed/miter/top_err_1.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output cout
+ );
+ parameter X = 1;
+ wire o;
+
+`ifndef BUG
+always @(posedge cin)
+	A <= o;
+
+//assign cout =  cin? y : x;
+
+middle u_mid (.x(x),.o(o));
+u_rtl inst_u_rtl (.x(x),.o(o));
+`else
+assign {cout,A} =  cin - y * x;
+`endif
+
+endmodule
+
+module middle
+(
+	input x,
+	input y,
+	output o
+);
+
+assign o = x + y;
+endmodule
+
+module u_rtl
+(
+	input x,
+//	input y,
+	output o
+);
+
+assign o = x;
+endmodule

misc_reviewed/mutate/mutate_all.ys

+read_verilog ../top.v
+mutate -list 512 -o mutate.yss
+script mutate.yss
+select -assert-count 2 t:$add
+select -assert-count 9 t:$not
+select -assert-count 3 t:$xnor
+select -assert-count 1 t:$xor

misc_reviewed/mutate/mutate_cnot0.ys

+read_verilog ../top.v
+tee -o result.log mutate -mode cnot0 -module top -cell $add$../top.v:12$2 -port Y -portbit 0 -ctrlbit 1 -wire A -wirebit 0 -src ../top.v:7 -src ../top.v:12
+
+select -assert-count 1 t:$xnor
+
+
+

misc_reviewed/mutate/mutate_cnot1.ys

+read_verilog ../top.v
+tee -o result.log mutate -mode cnot1 -module top -cell $add$../top.v:12$2 -port A -portbit 0 -ctrlbit 1 -src top.v:12
+
+select -assert-count 1 t:$xor
+
+
+

misc_reviewed/mutate/mutate_const0.ys

+read_verilog ../top.v
+tee -o result.log mutate -mode const0 -module top -cell $add$../top.v:12$2 -port Y -portbit 0 -wire A -wirebit 0 -src ../top.v:7 -src ../top.v:12
+stat
+
+

misc_reviewed/mutate/mutate_const1.ys

+read_verilog ../top.v
+tee -o result.log mutate -mode const1 -module top -cell $add$../top.v:12$2 -port Y -portbit 0 -wire A -wirebit 0 -src ../top.v:7 -src ../top.v:12
+stat
+

misc_reviewed/mutate/mutate_error_fail.pat

+ERROR: Invalid mode:

misc_reviewed/mutate/mutate_error_fail.ys

+read_verilog ../top.v
+tee -o result.log mutate -cell $add$../top.v:12$1 -port \Y -portbit 0 -ctrlbit 0 -module top
+

misc_reviewed/mutate/mutate_inv.ys

+read_verilog ../top.v
+tee -o result.log mutate -mode inv -module top -cell $add$../top.v:12$2 -port Y -portbit 0 -wire A -wirebit 0 -src ../top.v:7 -src ../top.v:12
+
+select -assert-count 1 t:$not

misc_reviewed/mutate/mutate_list.ys

+read_verilog ../top.v
+tee -o result.log mutate -list 32
+

misc_reviewed/mutate/mutate_list_cfg.ys

+read_verilog ../top.v
+tee -o result.log mutate -list 32 -cfg weight_cover 1
+
+

misc_reviewed/mutate/mutate_list_ctrl.ys

+read_verilog ../top.v
+tee -o result.log mutate -list 32 -ctrl A 1 1
+

misc_reviewed/mutate/mutate_list_none.ys

+read_verilog ../top.v
+tee -o result.log mutate -list 32 -none
+

misc_reviewed/mutate/mutate_list_o.ys

+read_verilog ../top.v
+tee -o result.log mutate -list 32 -o o.txt
+

misc_reviewed/mutate/mutate_list_s.ys

+read_verilog ../top.v
+tee -o result.log mutate -list 32 -s s.txt
+help mutate
+

misc_reviewed/mutate/mutate_list_seed.ys

+read_verilog ../top.v
+tee -o result.log mutate -list 32 -seed 5
+

misc_reviewed/mutate/mutate_mem.ys

+read_verilog ../top_mem.v
+mutate -list 512 -o mutate.yss
+script mutate.yss
+
+

misc_reviewed/mutate/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output A,
+ output cout
+ );
+
+
+assign {cout,A} =  cin + y + x;
+
+endmodule
+

misc_reviewed/mutate/top_mem.v

+module top
+(
+	input [7:0] data_a, data_b,
+	input [6:1] addr_a, addr_b,
+	input we_a, we_b, re_a, re_b, clka, clkb,
+	output reg [7:0] q_a, q_b
+);
+	// Declare the RAM variable
+	reg [7:0] ram[63:0];
+
+	initial begin
+        q_a <= 8'h00;
+        q_b <= 8'd0;
+	end
+
+	// Port A
+	always @ (posedge clka)
+	begin
+		if (we_a)
+		begin
+			ram[addr_a] <= data_a;
+			q_a <= data_a;
+		end
+		if (re_b)
+		begin
+			q_a <= ram[addr_a];
+		end
+	end
+
+	// Port B
+	always @ (posedge clkb)
+	begin
+		if (we_b)
+		begin
+			ram[addr_b] <= data_b;
+			q_b <= data_b;
+		end
+		if (re_b)
+		begin
+			q_b <= ram[addr_b];
+		end
+	end
+
+endmodule

misc_reviewed/muxpack/muxpack.ys

+read_verilog ../top.v
+proc
+select -assert-count 13 t:$mux
+select -assert-count 1 t:$pmux
+select -assert-count 28 t:$eq
+muxpack
+select -assert-count 1 t:$mux
+select -assert-count 3 t:$pmux
+select -assert-count 28 t:$eq

misc_reviewed/muxpack/muxpack_reduce.ys

+read_verilog ../top_reduce.v
+proc
+muxpack
+select -assert-count 1  t:$pmux
+select -assert-count 16 t:$eq
+select -assert-count 8  t:$reduce_or

misc_reviewed/muxpack/top.v

+module mux2 (S,A,B,Y);
+    input S;
+    input A,B;
+    output reg Y;
+
+    always @(*)
+		Y = (S)? B : A;
+endmodule
+
+module mux4 ( S, D, Y );
+
+input[1:0] S;
+input[3:0] D;
+output Y;
+
+reg Y;
+wire[1:0] S;
+wire[3:0] D;
+
+always @*
+    if (S == 0) Y <= D[0];
+    else if (S == 1) Y <= D[1];
+    else if (S == 2) Y <= D[2];
+    else if (S == 3) Y <= D[3];
+    else Y <= 1'bx;
+
+endmodule
+
+module mux8 ( S, D, Y );
+
+input[2:0] S;
+input[7:0] D;
+output Y;
+
+reg Y;
+wire[2:0] S;
+wire[7:0] D;
+
+always @*
+    if (S == 0) Y <= D[0];
+    else if (S == 1) Y <= D[1];
+    else if (S == 2) Y <= D[2];
+    else if (S == 3) Y <= D[3];
+    else if (S == 4) Y <= D[4];
+    else if (S == 5) Y <= D[5];
+    else if (S == 6) Y <= D[6];
+    else if (S == 7) Y <= D[7];
+    else Y <= 1'bx;
+
+endmodule
+
+module mux16 (D, S, Y);
+ 	input  [15:0] D;
+ 	input  [3:0] S;
+ 	output Y;
+
+reg Y;
+wire[3:0] S;
+wire[15:0] D;
+
+always @*
+     begin
+        case( S )
+            0 : Y = D[0];
+            1 : Y = D[1];
+            2 : Y = D[2];
+            3 : Y = D[3];
+            4 : Y = D[4];
+            5 : Y = D[5];
+            6 : Y = D[6];
+            7 : Y = D[7];
+            8 : Y = D[8];
+            9 : Y = D[9];
+            10 : Y = D[10];
+            11 : Y = D[11];
+            12 : Y = D[12];
+            13 : Y = D[13];
+            14 : Y = D[14];
+            15 : Y = D[15];
+            default: Y = 1'bx;
+        endcase
+     end
+
+endmodule
+
+
+module top (
+input [3:0] S,
+input [15:0] D,
+output M2,M4,M8,M16
+);
+
+mux2 u_mux2 (
+        .S (S[0]),
+        .A (D[0]),
+        .B (D[1]),
+        .Y (M2)
+    );
+
+
+mux4 u_mux4 (
+        .S (S[1:0]),
+        .D (D[3:0]),
+        .Y (M4)
+    );
+
+mux8 u_mux8 (
+        .S (S[2:0]),
+        .D (D[7:0]),
+        .Y (M8)
+    );
+
+mux16 u_mux16 (
+        .S (S[3:0]),
+        .D (D[15:0]),
+        .Y (M16)
+    );
+
+endmodule

misc_reviewed/muxpack/top_reduce.v

+module mux (D, S, Y);
+ 	input  [7:0] D;
+ 	input  [3:0] S;
+ 	output Y;
+
+reg Y;
+wire[3:0] S;
+wire[7:0] D;
+
+always @*
+     begin
+        case( S )
+            0,1 : Y = D[0];
+            2,3 : Y = D[1];
+            4,5 : Y = D[2];
+            6,7 : Y = D[3];
+            8,9 : Y = D[4];
+            10,11 : Y = D[5];
+            12,13 : Y = D[6];
+            14,15 : Y = D[7];
+            default: Y = 1'bx;
+        endcase
+     end
+
+endmodule
+
+module mux4 ( S, D, Y );
+
+input[1:0] S;
+input[3:0] D;
+output Y;
+
+reg Y;
+wire[1:0] S;
+wire[3:0] D;
+
+always @*
+    if (S != 0) Y <= D[0];
+    else if (S != 1) Y <= D[1];
+    else if (S != 2) Y <= D[2];
+    else if (S != 3) Y <= D[3];
+    else Y <= 1'bx;
+
+endmodule
+

misc_reviewed/onehot/onehot.ys

+read_verilog ../top.v
+proc
+pmux2shiftx -onehot ignore
+
+onehot
+tee -o result.out 

misc_reviewed/onehot/onehot_v.ys

+read_verilog ../top.v
+proc
+pmux2shiftx -onehot ignore
+onehot -v
+

misc_reviewed/onehot/onehot_vv.ys

+read_verilog ../top.v
+proc
+pmux2shiftx -onehot ignore
+onehot -vv
+

misc_reviewed/onehot/onehot_vv_1.ys

+read_verilog ../top_1.v
+proc
+pmux2shiftx -onehot ignore
+onehot -vv
+

misc_reviewed/onehot/onehot_vv_2.ys

+read_verilog ../top_2.v
+proc
+pmux2shiftx -onehot ignore
+onehot -vv
+

misc_reviewed/onehot/onehot_vv_3.ys

+read_verilog ../top_3.v
+proc
+pmux2shiftx -onehot ignore
+onehot -vv
+

misc_reviewed/onehot/onehot_vv_4.ys

+read_verilog ../top_4.v
+proc
+pmux2shiftx -onehot ignore
+onehot -vv
+

misc_reviewed/onehot/onehot_vv_5.ys

+read_verilog ../top_5.v
+proc
+pmux2shiftx -onehot ignore
+onehot -vv
+

misc_reviewed/onehot/onehot_vv_6.ys

+read_verilog ../top_6.v
+proc
+pmux2shiftx -onehot ignore
+onehot -vv
+

misc_reviewed/onehot/onehot_vv_fsm.ys

+read_verilog ../top_fsm.v
+proc
+pmux2shiftx -onehot ignore
+onehot -vv
+

misc_reviewed/onehot/top.v

+module top(C, S, Y);
+input C;
+input [1:0] S;
+output reg [3:0] Y;
+
+initial Y = 0;
+
+always @(posedge C) begin
+        case (S)
+                2'b00: Y <= 4'b0001;
+                2'b01: Y <= 4'b0010;
+                2'b10: Y <= 4'b0100;
+                2'b11: Y <= 4'b1000;
+        endcase
+end
+
+endmodule

misc_reviewed/onehot/top_1.v

+module mux (sel, res);
+  input [2:0] sel;
+  output [7:0] res;
+  reg [7:0] res;
+
+  always @(sel or res)
+  begin
+    case (sel)
+       3'b000 : res = 8'b00000001;
+       3'b001 : res = 8'b00000010;
+       3'b010 : res = 8'b00000100;
+      3'b011 : res = 8'b00001000;
+      3'b100 : res = 8'b00010000;
+      3'b101 : res = 8'b00100000;
+      3'b110 : res = 8'b01000000;
+      default : res = 8'b10000000;
+    endcase
+  end
+endmodule

misc_reviewed/onehot/top_2.v

+module mux (sel, res);
+  input [2:0] sel;
+  output [7:0] res;
+  reg [7:0] res;
+
+  always @(sel)
+  begin
+    case (sel)
+      3'b000 : res = 8'b11111110;
+      3'b001 : res = 8'b11111101;
+      3'b010 : res = 8'b11111011;
+      3'b011 : res = 8'b11110111;
+      3'b100 : res = 8'b11101111;
+      3'b101 : res = 8'b11011111;
+      3'b110 : res = 8'b10111111;
+      default : res = 8'b01111111;
+    endcase
+  end
+endmodule

misc_reviewed/onehot/top_3.v

+module mux (sel, res);
+  input [2:0] sel;
+  output [7:0] res;
+  reg [7:0] res;
+
+  always @(sel)
+  begin
+    case (sel)
+      3'b000 : res = 8'b00000001;
+      // unused decoder output
+      3'b001 : res = 8'bxxxxxxxx;
+      3'b010 : res = 8'b00000100;
+      3'b011 : res = 8'b00001000;
+      3'b100 : res = 8'b00010000;
+      3'b101 : res = 8'b00100000;
+      3'b110 : res = 8'b01000000;
+      default : res = 8'b10000000;
+    endcase
+  end
+endmodule

misc_reviewed/onehot/top_4.v

+module mux (sel, res);
+  input [2:0] sel;
+  output [7:0] res;
+  reg [7:0] res;
+
+  always @(sel or res)
+  begin
+    case (sel)
+      3'b000 : res = 8'b00000001;
+      3'b001 : res = 8'b00000010;
+      3'b010 : res = 8'b00000100;
+      3'b011 : res = 8'b00001000;
+      3'b100 : res = 8'b00010000;
+      3'b101 : res = 8'b00100000;
+      // 110 and 111 selector values are unused
+      default : res = 8'bxxxxxxxx;
+    endcase
+  end
+endmodule

misc_reviewed/onehot/top_5.v

+module priority (sel, code);
+  input [7:0] sel;
+  output [2:0] code;
+  reg [2:0] code;
+
+  always @(sel)
+  begin
+        if (sel[0]) code <= 3'b000;
+   else if (sel[1]) code <= 3'b001;
+   else if (sel[2]) code <= 3'b010;
+   else if (sel[3]) code <= 3'b011;
+   else if (sel[4]) code <= 3'b100;
+   else if (sel[5]) code <= 3'b101;
+   else if (sel[6]) code <= 3'b110;
+   else if (sel[7]) code <= 3'b111;
+   else code <= 3'bxxx;
+  end
+endmodule

misc_reviewed/onehot/top_6.v

+module lshift (DI, SEL, SO);
+input  [7:0] DI;
+input  [1:0] SEL;
+output [7:0] SO;
+reg[7:0] SO;
+
+  always @(DI or SEL)
+  begin
+    case (SEL)
+      2'b00   : SO <= DI;
+      2'b01   : SO <= DI << 1;
+      2'b10   : SO <= DI << 3;
+      default : SO <= DI << 2;
+    endcase
+  end
+endmodule

misc_reviewed/onehot/top_fsm.v

+ module fsm (
+ clock,
+ reset,
+ req_0,
+ req_1,
+ gnt_0,
+ gnt_1      
+ );
+ input   clock,reset,req_0,req_1;
+ output  gnt_0,gnt_1;
+ wire    clock,reset,req_0,req_1;
+ reg     gnt_0,gnt_1;
+ 
+ parameter SIZE = 3           ;
+ parameter IDLE  = 3'b001,GNT0 = 3'b010,GNT1 = 3'b100,GNT2 = 3'b101 ;
+ 
+ reg [SIZE-1:0] state;
+ reg [SIZE-1:0] next_state;
+ 
+ always @ (posedge clock)
+ begin : FSM
+ if (reset == 1'b1) begin
+   state <=  #1  IDLE;
+   gnt_0 <= 0;
+   gnt_1 <= 0;
+ end else
+  case(state)
+    IDLE : if (req_0 == 1'b1) begin
+                 state <=  #1  GNT0;
+`ifndef BUG        
+                 gnt_0 <= 1;
+`else
+                 gnt_0 <= 1'bZ;
+`endif
+               end else if (req_1 == 1'b1) begin
+                 gnt_1 <= 1;
+                 state <=  #1  GNT0;
+               end else begin
+                 state <=  #1  IDLE;
+               end
+    GNT0 : if (req_0 == 1'b1) begin
+                 state <=  #1  GNT0;
+               end else begin
+                 gnt_0 <= 0;
+                 state <=  #1  IDLE;
+               end
+    GNT1 : if (req_1 == 1'b1) begin
+                 state <=  #1  GNT2;
+				 gnt_1 <= req_0;
+               end
+    GNT2 : if (req_0 == 1'b1) begin
+                 state <=  #1  GNT1;
+				 gnt_1 <= req_1;
+               end 
+    default : state <=  #1  IDLE;
+ endcase
+ end
+ 
+ endmodule
+ 
+ module top (
+input clk,
+input rst,
+input a,
+input b,
+output g0,
+output g1
+);
+
+fsm u_fsm ( .clock(clk),
+            .reset(rst), 
+            .req_0(a), 
+            .req_1(b), 
+            .gnt_0(g0), 
+            .gnt_1(g1));
+
+endmodule

misc_reviewed/opt_rmdff_sat/bc.v

+
+module bc #(
+            parameter SIZE=2,
+            parameter WIDTH=16
+            )
+   (
+    input                        clk,
+    input                        rst,
+
+    output wire                  din_ready,
+    input wire                   din_valid,
+    input wire [WIDTH-1:0]       din_data,
+
+    input wire [SIZE-1:0]        dout_ready,
+    output wire [SIZE-1:0]       dout_valid,
+    output wire [WIDTH*SIZE-1:0] dout_data
+    );
+
+   reg [SIZE-1 : 0] ready_reg;
+   wire [SIZE-1 : 0] ready_all;
+   genvar           i;
+
+   initial begin
+      ready_reg = 0;
+   end
+
+   generate
+      for (i = 0; i < SIZE; i=i+1) begin
+         assign ready_all[i]  = dout_ready[i] | ready_reg[i];
+         assign dout_valid[i] = din_valid & !ready_reg[i];
+         assign dout_data[(i+1)*WIDTH-1:i*WIDTH]   = din_data;
+
+         always @(posedge clk) begin
+            if (rst || (!din_valid) || din_ready) begin
+               ready_reg[i] <= 1'b0;
+            end else if (dout_ready[i]) begin
+               ready_reg[i] <= 1'b1;
+            end
+         end
+      end
+   endgenerate
+   assign din_ready = &ready_all;
+
+endmodule

misc_reviewed/opt_rmdff_sat/demux.v

+
+module demux
+(
+    input clk,
+    input rst,
+    output reg  din_ready,
+    input  wire din_valid,
+    input  wire [2:0] din_data,
+    input  wire         dout0_ready,
+    output reg          dout0_valid,
+    output wire  [0:0] dout0_data,
+    input  wire         dout1_ready,
+    output reg          dout1_valid,
+    output wire  [1:0] dout1_data
+
+);
+    wire [2:0] din_s; // u1 | u2
+    wire [1:0] din_s_data; // u2
+    assign din_s_data = din_s[1:0];
+    wire [0:0] din_s_ctrl; // u1
+    assign din_s_ctrl = din_s[2:2];
+
+
+    assign din_s = din_data;
+
+
+    assign dout0_data = din_data;
+    assign dout1_data = din_data;
+
+    always @*
+    begin
+        din_ready = 1'bx;
+        dout0_valid = 0;
+        dout1_valid = 0;
+
+        if (din_valid) begin
+            case(din_s_ctrl)
+                0 : begin
+                    din_ready = dout0_ready;
+                    dout0_valid = din_valid;
+                end
+                1 : begin
+                    din_ready = dout1_ready;
+                    dout1_valid = din_valid;
+                end
+                default: begin
+                    din_ready = 1'bx;
+                    dout0_valid = 1'bx;
+                    dout1_valid = 1'bx;
+                end
+            endcase
+        end
+    end
+
+
+
+endmodule

misc_reviewed/opt_rmdff_sat/mux.v

+
+module mux
+(
+    input clk,
+    input rst,
+    output reg  ctrl_ready,
+    input  wire ctrl_valid,
+    input  wire [0:0] ctrl_data,
+    output reg  din0_ready,
+    input  wire din0_valid,
+    input  wire [0:0] din0_data,
+    output reg  din1_ready,
+    input  wire din1_valid,
+    input  wire [1:0] din1_data,
+    input  wire         dout_ready,
+    output reg          dout_valid,
+    output wire  [2:0] dout_data
+
+);
+    wire [0:0] ctrl_s; // u1
+
+    wire [0:0] din0_s; // u1
+
+    wire [1:0] din1_s; // u2
+
+    reg [2:0] dout_s; // u1 | u2
+    reg [1:0] dout_s_data; // u2
+    assign dout_s[1:0] = dout_s_data;
+    reg [0:0] dout_s_ctrl; // u1
+    assign dout_s[2:2] = dout_s_ctrl;
+
+
+    assign ctrl_s = ctrl_data;
+    assign din0_s = din0_data;
+    assign din1_s = din1_data;
+
+    assign dout_data = dout_s;
+
+    wire handshake;
+    reg din_valid_sel;
+
+    assign handshake = dout_valid && dout_ready;
+
+    always @*
+    begin
+        din0_ready = din0_valid ? 0 : dout_ready;
+        din1_ready = din1_valid ? 0 : dout_ready;
+        dout_s_data = { 2 {1'bx}};
+        din_valid_sel = 0;
+        if (ctrl_valid) begin
+            case( ctrl_data )
+                0 : begin
+                    din_valid_sel = din0_valid;
+                    dout_s_data[0:0] = din0_s;
+                    din0_ready = din0_valid ? handshake : dout_ready;
+                end
+                1 : begin
+                    din_valid_sel = din1_valid;
+                    dout_s_data[1:0] = din1_s;
+                    din1_ready = din1_valid ? handshake : dout_ready;
+                end
+                default: begin
+                    din0_ready = dout_ready;
+                    din1_ready = dout_ready;
+                    din_valid_sel = 1'bx;
+                end
+            endcase
+        end
+    end
+
+    assign ctrl_ready = ctrl_valid ? handshake : dout_ready;
+    assign dout_s_ctrl = ctrl_s;
+    assign dout_valid = ctrl_valid && din_valid_sel;
+
+
+
+endmodule
\ No newline at end of file

misc_reviewed/opt_rmdff_sat/opt_rmdff_sat.ys

+read_verilog  ../top.v
+read_verilog  ../bc.v
+read_verilog  ../demux.v
+read_verilog  ../mux.v
+
+prep -flatten
+opt_rmdff -sat
+synth
+tee -o result.log select -assert-count 0 t:$_DFF_P_

misc_reviewed/opt_rmdff_sat/top.v

+module top(
+    input clk,
+    input rst,
+
+    output wire  din_ready,
+    input  wire din_valid,
+    input  wire [2:0] din_data,
+    input  wire         dout_ready,
+    output wire          dout_valid,
+    output wire  [2:0] dout_data
+
+);
+
+   wire                dout1_ready;
+   wire                dout1_valid;
+   wire [0:0]          dout1_data;
+
+   wire                dout2_ready;
+   wire                dout2_valid;
+   wire [1:0]          dout2_data;
+
+   wire [1:0]          din_bc_ready;
+   wire [1:0]          din_bc_valid;
+   wire [5:0]          din_bc_data;
+
+   bc #(
+        .SIZE(2'd2),
+        .WIDTH(2'd3)
+        )
+   bc_din (
+           .clk(clk),
+           .rst(rst),
+
+           .din_valid(din_valid),
+           .din_ready(din_ready),
+           .din_data(din_data),
+
+           .dout_valid(din_bc_valid),
+           .dout_ready(din_bc_ready),
+           .dout_data(din_bc_data)
+           );
+
+
+   demux demux (
+                           .clk(clk),
+                           .rst(rst),
+
+                           .din_valid(din_bc_valid[0]),
+                           .din_ready(din_bc_ready[0]),
+                           .din_data(din_bc_data[2:0]),
+
+                           .dout0_valid(dout1_valid),
+                           .dout0_ready(dout1_ready),
+                           .dout0_data(dout1_data),
+
+                           .dout1_valid(dout2_valid),
+                           .dout1_ready(dout2_ready),
+                           .dout1_data(dout2_data)
+                           );
+
+   mux mux (
+            .clk(clk),
+            .rst(rst),
+
+            .ctrl_valid(din_bc_valid[1]),
+            .ctrl_ready(din_bc_ready[1]),
+            .ctrl_data(din_bc_data[2]),
+
+            .din0_valid(dout1_valid),
+            .din0_ready(dout1_ready),
+            .din0_data(dout1_data),
+
+            .din1_valid(dout2_valid),
+            .din1_ready(dout2_ready),
+            .din1_data(dout2_data),
+
+            .dout_valid(dout_valid),
+            .dout_ready(dout_ready),
+            .dout_data(dout_data)
+            );
+
+
+
+endmodule

misc_reviewed/plugin/plugin.ys

+tee -o result.log plugin

misc_reviewed/plugin/plugin_a.ys

+read_verilog ../top.v
+tee -o result.log plugin -i /usr/local/share/yosys/plugins/vhdl.so -a alias

misc_reviewed/plugin/plugin_error_fail.pat

+ERROR: Can't load module

misc_reviewed/plugin/plugin_error_fail.ys

+read_verilog ../top.v
+tee -o result.log plugin -l
+plugin -i uu -a alias
+tee -o result.log plugin -l

misc_reviewed/plugin/plugin_i.ys

+read_verilog ../top.v
+tee -o result.log plugin -i /usr/local/share/yosys/plugins/vhdl.so

misc_reviewed/plugin/plugin_l.ys

+read_verilog ../top.v
+tee -o result.log plugin -l
+plugin -i /usr/local/share/yosys/plugins/vhdl.so -a alias
+tee -o result.log plugin -l

misc_reviewed/plugin/top.v

+module top
+    ( input d, clk, output reg q );
+	always @( posedge clk )
+            q <= d;
+endmodule

misc_reviewed/pmux2shiftx/pmux2shiftx.ys

+read_verilog ../top.v
+proc
+select -assert-count 0 t:$shiftx
+pmux2shiftx
+select -assert-count 1 t:$shiftx
+

misc_reviewed/pmux2shiftx/pmux2shiftx_2.ys

+read_verilog ../top_2.v
+proc
+select -assert-count 0 t:$shiftx
+pmux2shiftx
+select -assert-count 1 t:$shiftx
+

misc_reviewed/pmux2shiftx/pmux2shiftx_fsm.ys

+read_verilog ../top_fsm.v
+proc
+select -assert-count 0 t:$shiftx
+pmux2shiftx
+select -assert-count 2 t:$shiftx
+

misc_reviewed/pmux2shiftx/pmux2shiftx_min_choices_0.ys

+read_verilog ../top_fsm.v
+proc
+pmux2shiftx -min_choices 0
+onehot
+

misc_reviewed/pmux2shiftx/pmux2shiftx_min_choices_3000.ys

+read_verilog ../top_fsm.v
+proc
+pmux2shiftx -min_choices 3000
+

misc_reviewed/pmux2shiftx/pmux2shiftx_min_dens_0.ys

+read_verilog ../top_fsm.v
+proc
+pmux2shiftx -min_density 0
+onehot
+

misc_reviewed/pmux2shiftx/pmux2shiftx_min_dens_3000.ys

+read_verilog ../top_fsm.v
+proc
+pmux2shiftx -min_density 3000
+

misc_reviewed/pmux2shiftx/pmux2shiftx_norange.ys

+read_verilog ../top_fsm.v
+proc
+pmux2shiftx -norange
+onehot
+

misc_reviewed/pmux2shiftx/pmux2shiftx_onehot_ignore.ys

+read_verilog ../top_fsm.v
+proc
+pmux2shiftx -onehot ignore
+onehot
+

misc_reviewed/pmux2shiftx/pmux2shiftx_onehot_pmux.ys

+read_verilog ../top_fsm.v
+proc
+pmux2shiftx -onehot pmux
+

misc_reviewed/pmux2shiftx/pmux2shiftx_onehot_shiftx.ys

+read_verilog ../top_fsm.v
+proc
+pmux2shiftx -onehot shiftx
+onehot
+

misc_reviewed/pmux2shiftx/pmux2shiftx_top.ys

+read_verilog ../top.v
+proc
+select -assert-count 0 t:$shiftx
+pmux2shiftx top
+select -assert-count 1 t:$shiftx
+

misc_reviewed/pmux2shiftx/pmux2shiftx_v.ys

+read_verilog ../top_fsm.v
+proc
+select -assert-count 0 t:$shiftx
+pmux2shiftx -v
+select -assert-count 2 t:$shiftx
+

misc_reviewed/pmux2shiftx/pmux2shiftx_vv.ys

+read_verilog ../top_fsm.v
+proc
+pmux2shiftx -vv
+

misc_reviewed/pmux2shiftx/top.v

+module top(C, S, Y);
+input C;
+input [1:0] S;
+output reg [3:0] Y;
+
+initial Y = 0;
+
+always @(posedge C) begin
+        case (S)
+                2'b00: Y <= 4'b0001;
+                2'b01: Y <= 4'b0010;
+                2'b10: Y <= 4'b0100;
+                2'b11: Y <= 4'b1000;
+        endcase
+end
+
+endmodule

misc_reviewed/pmux2shiftx/top_2.v

+module top(input [7:0] i, output o);
+always @*
+case (i[6:3])
+    4: o <= i[0];
+    3: o <= i[2];
+    7: o <= i[3];
+    default: o <= 1'b0;
+endcase
+endmodule

misc_reviewed/pmux2shiftx/top_fsm.v

+ module fsm (
+ clock,
+ reset,
+ req_0,
+ req_1,
+ gnt_0,
+ gnt_1
+ );
+ input   clock,reset,req_0,req_1;
+ output  gnt_0,gnt_1;
+ wire    clock,reset,req_0,req_1;
+ reg     gnt_0,gnt_1;
+
+ parameter SIZE = 3           ;
+ parameter IDLE  = 3'b001,GNT0 = 3'b010,GNT1 = 3'b100,GNT2 = 3'b101 ;
+
+ reg [SIZE-1:0] state;
+ reg [SIZE-1:0] next_state;
+
+ always @ (posedge clock)
+ begin : FSM
+ if (reset == 1'b1) begin
+   state <=  #1  IDLE;
+   gnt_0 <= 0;
+   gnt_1 <= 0;
+ end else
+  case(state)
+    IDLE : if (req_0 == 1'b1) begin
+                 state <=  #1  GNT0;
+                 gnt_0 <= 1;
+               end else if (req_1 == 1'b1) begin
+                 gnt_1 <= 1;
+                 state <=  #1  GNT0;
+               end else begin
+                 state <=  #1  IDLE;
+               end
+    GNT0 : if (req_0 == 1'b1) begin
+                 state <=  #1  GNT0;
+               end else begin
+                 gnt_0 <= 0;
+                 state <=  #1  IDLE;
+               end
+    GNT1 : if (req_1 == 1'b1) begin
+                 state <=  #1  GNT2;
+				 gnt_1 <= req_0;
+               end
+    GNT2 : if (req_0 == 1'b1) begin
+                 state <=  #1  GNT1;
+				 gnt_1 <= req_1;
+               end
+    default : state <=  #1  IDLE;
+ endcase
+ end
+
+ endmodule
+
+ module top (
+input clk,
+input rst,
+input a,
+input b,
+output g0,
+output g1
+);
+
+fsm u_fsm ( .clock(clk),
+            .reset(rst),
+            .req_0(a),
+            .req_1(b),
+            .gnt_0(g0),
+            .gnt_1(g1));
+
+endmodule

misc_reviewed/pmuxtree/pmuxtree.ys

+read_verilog ../top.v
+proc
+pmuxtree
+select -assert-none t:$pmuxtree
+select -assert-count 3 t:$mux

misc_reviewed/pmuxtree/pmuxtree_1.ys

+read_verilog ../top_1.v
+proc
+pmuxtree
+select -assert-none t:$pmuxtree
+select -assert-count 7 t:$mux

misc_reviewed/pmuxtree/top.v

+module top(C, S, Y);
+input C;
+input [1:0] S;
+output reg [3:0] Y;
+
+initial Y = 0;
+
+always @(posedge C) begin
+        case (S)
+                2'b00: Y <= 4'b0001;
+                2'b01: Y <= 4'b0010;
+                2'b10: Y <= 4'b0100;
+                2'b11: Y <= 4'b1000;
+        endcase
+end
+
+endmodule

misc_reviewed/pmuxtree/top_1.v

+module mux (sel, res);
+  input [2:0] sel;
+  output [7:0] res;
+  reg [7:0] res;
+
+  always @(sel or res)
+  begin
+    case (sel)
+       3'b000 : res = 8'b00000001;
+       3'b001 : res = 8'b00000010;
+       3'b010 : res = 8'b00000100;
+      3'b011 : res = 8'b00001000;
+      3'b100 : res = 8'b00010000;
+      3'b101 : res = 8'b00100000;
+      3'b110 : res = 8'b01000000;
+      default : res = 8'b10000000;
+    endcase
+  end
+endmodule

misc_reviewed/qwp/qwp.pat

+attribute \\qwp_position

misc_reviewed/qwp/qwp.ys

+read_verilog ../top.v
+proc
+qwp
+tee -o result.out dump

misc_reviewed/qwp/qwp_alpha.pat

+attribute \\qwp_position

misc_reviewed/qwp/qwp_alpha.ys

+read_verilog ../top.v
+proc
+qwp -alpha
+tee -o result.out dump
+

misc_reviewed/qwp/qwp_dump.pat

+attribute \\qwp_position

misc_reviewed/qwp/qwp_dump.ys

+read_verilog ../top.v
+proc
+qwp -dump out.html
+tee -o result.out dump
+

misc_reviewed/qwp/qwp_grid.pat

+attribute \\qwp_position

misc_reviewed/qwp/qwp_grid.ys

+read_verilog ../top.v
+proc
+qwp -grid 4
+tee -o result.out dump

misc_reviewed/qwp/qwp_ltr.pat

+attribute \\qwp_position

misc_reviewed/qwp/qwp_ltr.ys

+read_verilog ../top.v
+proc
+qwp -ltr
+tee -o result.out dump
+

misc_reviewed/qwp/qwp_v.pat

+> System size: 3^2
+> Edge constraints: 2
+> Node constraints: 3
+> Solving
+> Solved
+> Update nodes
+> System size: 3^2
+> Edge constraints: 2
+> Node constraints: 3
+> Solving
+> Solved
+> Update nodes

misc_reviewed/qwp/qwp_v.ys

+read_verilog ../top.v
+proc
+tee -o result.out qwp -v
+

misc_reviewed/qwp/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output cout
+ );
+ wire o;
+
+always @(posedge cin)
+	A <= o;
+
+assign cout =  cin? y : x;
+
+middle u_mid (x,y,o);
+
+endmodule
+
+module middle
+(
+	input x,
+	input y,
+	output o
+);
+
+assign o = x + y;
+endmodule

misc_reviewed/rename/rename.pat

+module \\mid_module

misc_reviewed/rename/rename.ys

+read_verilog ../top.v
+proc
+rename middle mid_module
+tee -o result.out dump

misc_reviewed/rename/rename_enumerate.pat

+cell $add \\_1_

misc_reviewed/rename/rename_enumerate.ys

+read_verilog ../top.v
+proc
+rename -enumerate  middle mid_module
+tee -o result.out dump

misc_reviewed/rename/rename_enumerate_pat.pat

+cell $mux \\'_3_top'

misc_reviewed/rename/rename_enumerate_pat.ys

+read_verilog ../top.v
+proc
+rename -enumerate -pattern '_%_top' top
+tee -o result.out dump

misc_reviewed/rename/rename_hide.ys

+read_verilog ../top.v
+proc
+rename -hide middle mid

misc_reviewed/rename/rename_invalid_number_of_args_fail.pat

+ERROR: Invalid number of arguments!

misc_reviewed/rename/rename_invalid_number_of_args_fail.ys

+read_verilog ../top.v
+proc
+tee -o result.log rename

misc_reviewed/rename/rename_invalid_number_of_args_top_fail.pat

+ERROR: Invalid number of arguments!

misc_reviewed/rename/rename_invalid_number_of_args_top_fail.ys

+read_verilog ../top.v
+proc
+tee -o result.log rename -top

misc_reviewed/rename/rename_low.pat

+module \\newlow

misc_reviewed/rename/rename_low.ys

+read_verilog ../top.v
+synth
+rename low newlow
+tee -o result.out dump

misc_reviewed/rename/rename_mode_out_requires_fail.pat

+ERROR: Mode -output requires that there is an active module selected.

misc_reviewed/rename/rename_mode_out_requires_fail.ys

+read_verilog ../top.v
+proc
+tee -o result.log rename -output u uu

misc_reviewed/rename/rename_no_top_module_fail.pat

+ERROR: No top module found!

misc_reviewed/rename/rename_no_top_module_fail.ys

+read_verilog ../top.v
+proc
+tee -o result.log rename -top top

misc_reviewed/rename/rename_obj_not_found_fail.pat

+ERROR: Object `u' not found!

misc_reviewed/rename/rename_obj_not_found_fail.ys

+read_verilog ../top.v
+proc
+tee -o result.log rename u uu

misc_reviewed/rename/rename_src.pat

+cell $add \\../top.v:

misc_reviewed/rename/rename_src.ys

+read_verilog ../top.v
+proc
+rename -src middle mid_module
+tee -o result.out dump

misc_reviewed/rename/rename_top.pat

+module \\new_top

misc_reviewed/rename/rename_top.ys

+read_verilog ../top.v
+synth -top top
+rename -top new_top
+tee -o result.out dump

misc_reviewed/rename/rename_top_top.pat

+module \\new_top

misc_reviewed/rename/rename_top_top.ys

+read_verilog ../top.v
+synth -top top
+rename top new_top
+tee -o result.out dump

misc_reviewed/rename/rename_wire.ys

+read_verilog ../top.v
+proc
+tee -o resulta.out dump
+rename -wire top/o top/t_o
+tee -o result.out dump

misc_reviewed/rename/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output cout
+ );
+ wire o;
+
+always @(posedge cin)
+	A <= o;
+
+assign cout =  cin? y : x;
+
+middle u_mid (x,y,o);
+
+endmodule
+
+module middle
+(
+	input x,
+	input y,
+	output o
+);
+wire dd;
+
+assign o = x + y;
+endmodule
+
+module low ();
+endmodule

misc_reviewed/rmports/rmports.pat

+wire \\cout

misc_reviewed/rmports/rmports.ys

+read_verilog ../top.v
+proc
+rmports top middle
+tee -o result.out dump

misc_reviewed/rmports/top.v

+module top
+(
+ input x,
+ input x,
+ input z,
+ input cin,
+
+ output reg A,
+ output cout
+ );
+ parameter X = 1;
+ wire o;
+
+always @(posedge cin)
+	A <= o;
+
+middle u_mid (.z(z),.x(x),.o(o));
+
+endmodule
+
+module middle
+(
+	input x,
+	input y,
+	input z,
+	output o
+);
+
+assign o = x + y;
+endmodule

misc_reviewed/sat/sat.ys

+read_verilog ../top.v
+proc
+ sat middle

misc_reviewed/sat/sat_all.ys

+read_verilog ../top.v
+proc
+ sat -ignore_unknown_cells -all top

misc_reviewed/sat/sat_all_with_show.ys

+read_verilog -sv ../top_ff.v
+synth
+ sat -ignore_unknown_cells -all -show q adff

misc_reviewed/sat/sat_all_with_tempinduct.ys

+read_verilog ../top.v
+#proc
+ sat -all -prove x 1 -tempinduct middle

misc_reviewed/sat/sat_all_with_tempinduct_ff.ys

+read_verilog ../top_ff.v
+synth
+ sat -ignore_unknown_cells -all -prove clr 1 -tempinduct adff

misc_reviewed/sat/sat_all_with_tempinduct_setinit.disable

+read_verilog -sv ../top_ff.v
+#proc
+ sat -ignore_unknown_cells -all -prove clr 1 -set-init s 1'b1 -tempinduct adff

misc_reviewed/sat/sat_all_with_tempinduct_setinit.ys

+read_verilog -sv ../top_ff.v
+synth
+# sat -ignore_unknown_cells -all -prove clr 1 -set-init q 1 -tempinduct adff
+tee -o result.out sat -ignore_unknown_cells -prove clr 1 -set-init q 1  -tempinduct adff

misc_reviewed/sat/sat_all_with_tempinduct_setinit_fail.pat

+ERROR: Found -set-init bits that are not part of the initial_state: \\o

misc_reviewed/sat/sat_all_with_tempinduct_setinit_fail.ys

+read_verilog ../top.v
+#proc
+ sat -all -prove x 1 -set-init o 0 -tempinduct middle

misc_reviewed/sat/sat_all_with_tempinduct_setinitdef.ys

+read_verilog -sv ../top_initstate.v
+#proc
+ sat -ignore_unknown_cells -all -prove x 1 -set-init-def -tempinduct-def middle

misc_reviewed/sat/sat_all_with_tempinduct_setinitundef.ys

+read_verilog -sv ../top_initstate.v
+#proc
+ sat -ignore_unknown_cells -all -prove x 1 -set-init-undef -tempinduct-def middle

misc_reviewed/sat/sat_all_with_tempinduct_setinitzero.ys

+read_verilog -sv ../top_initstate.v
+#proc
+ sat -ignore_unknown_cells -all -prove x 1 -set-init-zero -tempinduct-def middle

misc_reviewed/sat/sat_cant_open_json_file_fail.pat

+ERROR: Can't open output file `dir/out.json' for writing: No such file or directory

misc_reviewed/sat/sat_cant_open_json_file_fail.ys

+read_verilog ../top.v
+proc
+ sat -dump_json dir/out.json middle

misc_reviewed/sat/sat_cant_open_vcd_file_fail.pat

+ERROR: Can't open output file `dir/out.vcd' for writing: No such file or directory

misc_reviewed/sat/sat_cant_open_vcd_file_fail.ys

+read_verilog ../top.v
+proc
+ sat -dump_vcd dir/out.vcd middle

misc_reviewed/sat/sat_cant_perform_sat_on_empty_sel_fail.pat

+ERROR: Can't perform SAT on an empty selection!

misc_reviewed/sat/sat_cant_perform_sat_on_empty_sel_fail.ys

+ sat

misc_reviewed/sat/sat_cnf_open_json_file_fail.pat

+ERROR: Can't open output file `dir/out.cnf' for writing: No such file or directory

misc_reviewed/sat/sat_cnf_open_json_file_fail.ys

+read_verilog ../top.v
+proc
+ sat -dump_cnf dir/out.cnf middle

misc_reviewed/sat/sat_dump_cnf.ys

+read_verilog ../top.v
+proc
+ sat -dump_cnf cnf.cnf middle

misc_reviewed/sat/sat_dump_json.ys

+read_verilog ../top.v
+proc
+ sat -dump_json json.json  middle

misc_reviewed/sat/sat_dump_vcd.ys

+read_verilog ../top.v
+proc
+ sat -dump_vcd vcd.vcd  middle

misc_reviewed/sat/sat_enable_undef.ys

+read_verilog ../top.v
+proc
+ sat -enable_undef  middle

misc_reviewed/sat/sat_failed_to_import_cell_fail.pat

+ERROR: Failed to import cell inst_u_rtl (type u_rtl) to SAT database.

misc_reviewed/sat/sat_failed_to_import_cell_fail.ys

+read_verilog ../top.v
+proc
+ sat -prove-skip 1 -prove x 1 -seq 2 top

misc_reviewed/sat/sat_falsify.ys

+read_verilog ../top.v
+proc
+ sat -prove x 1 -falsify  middle

misc_reviewed/sat/sat_falsify_fail.pat

+ERROR: Called with -falsify and found a model!

misc_reviewed/sat/sat_falsify_fail.ys

+read_verilog ../top.v
+proc
+ sat -falsify middle

misc_reviewed/sat/sat_falsify_no_timeout.ys

+read_verilog ../top.v
+proc
+ sat -prove x 1 -falsify-no-timeout  middle

misc_reviewed/sat/sat_fsm_dump_cnf.ys

+read_verilog ../top_fsm.v
+proc
+ sat -dump_cnf cnf.cnf -ignore_unknown_cells fsm

misc_reviewed/sat/sat_fsm_dump_json.ys

+read_verilog ../top_fsm.v
+proc
+ sat -dump_json json.json -ignore_unknown_cells fsm

misc_reviewed/sat/sat_fsm_dump_vcd.ys

+read_verilog ../top_fsm.v
+proc
+ sat -dump_vcd vcd.vcd -ignore_unknown_cells fsm

misc_reviewed/sat/sat_got_tempinduct_but_nothing_to_prove_fail.pat

+ERROR: Got -tempinduct but nothing to prove!

misc_reviewed/sat/sat_got_tempinduct_but_nothing_to_prove_fail.ys

+read_verilog ../top.v
+ sat -tempinduct middle

misc_reviewed/sat/sat_ignore_div_by_zero.ys

+read_verilog ../top_div_by_zery.v
+proc
+ sat -ignore_div_by_zero middle

misc_reviewed/sat/sat_ignore_unknown_cells.pat

+Warning: Failed to import cell

misc_reviewed/sat/sat_ignore_unknown_cells.ys

+read_verilog ../top_fsm.v
+proc
+tee -o result.out sat -ignore_unknown_cells fsm

misc_reviewed/sat/sat_initsteps.pat

+Skipping prove for this step (-initsteps 1).

misc_reviewed/sat/sat_initsteps.ys

+read_verilog ../top.v
+proc
+tee -o result.out sat -initsteps 3 -tempinduct-skip 1 -prove x 0 -set-def-at 3 x  -tempinduct middle

misc_reviewed/sat/sat_max.ys

+read_verilog ../top.v
+proc
+ sat -max 3  middle

misc_reviewed/sat/sat_max_all_with_tempinduct.ys

+read_verilog ../top.v
+proc
+ sat -max 5 -all -prove x 1 -tempinduct middle

misc_reviewed/sat/sat_max_max_undef_with_tempinduct_fail.pat

+ERROR: The options -max, -all, and -max_undef are not supported for temporal induction proofs!

misc_reviewed/sat/sat_max_max_undef_with_tempinduct_fail.ys

+read_verilog ../top.v
+proc
+ sat -max_undef -all -prove x 1 -tempinduct top

misc_reviewed/sat/sat_max_maxundef_all_with_tempinduct_fail.pat

+ERROR: The options -max, -all, and -max_undef are not supported for temporal induction proofs!

misc_reviewed/sat/sat_max_maxundef_all_with_tempinduct_fail.ys

+read_verilog ../top.v
+proc
+ sat -max 1 -max_undef -all -prove x 1 -tempinduct top

misc_reviewed/sat/sat_max_maxundef_with_tempinduct_fail.pat

+ERROR: The options -max, -all, and -max_undef are not supported for temporal induction proofs!

misc_reviewed/sat/sat_max_maxundef_with_tempinduct_fail.ys

+read_verilog ../top.v
+proc
+ sat -max 1 -max_undef -prove x 1 -tempinduct top

misc_reviewed/sat/sat_max_undef.ys

+read_verilog ../top.v
+proc
+ sat -max_undef  middle

misc_reviewed/sat/sat_max_with_tempinduct_fail.pat

+ERROR: The options -max, -all, and -max_undef are not supported for temporal induction proofs!

misc_reviewed/sat/sat_max_with_tempinduct_fail.ys

+read_verilog ../top.v
+proc
+ sat -max 1 -prove x 1 -tempinduct top

misc_reviewed/sat/sat_maxsteps.ys

+read_verilog ../top.v
+proc
+ sat -maxsteps 0  middle

misc_reviewed/sat/sat_maxsteps_only_for_tempinduct_fail.pat

+ERROR: The options -maxsteps is only supported for temporal induction proofs!

misc_reviewed/sat/sat_maxsteps_only_for_tempinduct_fail.ys

+read_verilog ../top.v
+proc
+ sat -maxsteps 3 middle

misc_reviewed/sat/sat_maxundef_with_tempinduct_fail.pat

+ERROR: The options -max, -all, and -max_undef are not supported for temporal induction proofs!

misc_reviewed/sat/sat_maxundef_with_tempinduct_fail.ys

+read_verilog ../top.v
+proc
+ sat -max_undef -prove x 1 -tempinduct top

misc_reviewed/sat/sat_mux.ys

+read_verilog ../top_mux.v
+proc
+ sat mux16

misc_reviewed/sat/sat_only_one_module_must_be_sel_fail.pat

+ERROR: Only one module must be selected for the SAT pass! (selected: u_rtl and middle)

misc_reviewed/sat/sat_only_one_module_must_be_sel_fail.ys

+read_verilog ../top.v
+proc
+ sat

misc_reviewed/sat/sat_prove.ys

+read_verilog ../top.v
+proc
+ sat -ignore_unknown_cells -prove x 1  top

misc_reviewed/sat/sat_prove_and_tempinduct_fail.pat

+ERROR: Options -prove-skip and -tempinduct don't work with each other. Use -seq instead of -prove-skip.

misc_reviewed/sat/sat_prove_and_tempinduct_fail.ys

+read_verilog ../top.v
+proc
+ sat -prove-skip 365 -prove x 1 -tempinduct top

misc_reviewed/sat/sat_prove_asserts.ys

+read_verilog ../top.v
+proc
+ sat -prove-asserts middle

misc_reviewed/sat/sat_prove_diff_size_fail.pat

+ERROR: Proof expression with different lhs and rhs sizes: x (\\x, 1 bits) vs. 2'b11 (2'11, 2 bits)

misc_reviewed/sat/sat_prove_diff_size_fail.ys

+read_verilog ../top.v
+proc
+ sat -prove x 2'b11  middle

misc_reviewed/sat/sat_prove_lhs_fail.pat

+ERROR: Failed to parse lhs proof expression `X'.

misc_reviewed/sat/sat_prove_lhs_fail.ys

+read_verilog ../top.v
+proc
+ sat -prove X 0  middle

misc_reviewed/sat/sat_prove_rhs_fail.pat

+ERROR: Failed to parse rhs proof expression `X'.

misc_reviewed/sat/sat_prove_rhs_fail.ys

+read_verilog ../top.v
+proc
+ sat -prove x X  middle

misc_reviewed/sat/sat_prove_skip.ys

+read_verilog ../top.v
+proc
+ sat -prove-skip 1 -seq 2  middle

misc_reviewed/sat/sat_prove_skip_must_be_smaller_than_seq_fail.pat

+ERROR: The value of -prove-skip must be smaller than the one of -seq.

misc_reviewed/sat/sat_prove_skip_must_be_smaller_than_seq_fail.ys

+read_verilog ../top.v
+proc
+ sat -prove-skip 365 -prove x 1 -seq 1 top

misc_reviewed/sat/sat_prove_x.ys

+read_verilog ../top.v
+proc
+ sat -prove-x x 1  middle

misc_reviewed/sat/sat_provex_diff_size_fail.pat

+ERROR: Proof-x expression with different lhs and rhs sizes: x (\\x, 1 bits) vs. 2'b11 (2'11, 2 bits)

misc_reviewed/sat/sat_provex_diff_size_fail.ys

+read_verilog ../top.v
+proc
+ sat -prove-x x 2'b11  middle

misc_reviewed/sat/sat_provex_lhs_fail.pat

+ERROR: Failed to parse lhs proof-x expression `X'.

misc_reviewed/sat/sat_provex_lhs_fail.ys

+read_verilog ../top.v
+proc
+ sat -prove-x X 0  middle

misc_reviewed/sat/sat_provex_rhs_fail.pat

+ERROR: Failed to parse rhs proof-x expression `X'.

misc_reviewed/sat/sat_provex_rhs_fail.ys

+read_verilog ../top.v
+proc
+ sat -prove-x x X  middle

misc_reviewed/sat/sat_seq.ys

+read_verilog ../top_reg.v
+hierarchy -top dut
+proc
+memory -nomap
+equiv_opt -run :prove -map +/ecp5/cells_sim.v synth_ecp5
+memory
+opt -full
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+tee -o result.out sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter

misc_reviewed/sat/sat_set.pat

+Import set-constraint: \\x = 1'1

misc_reviewed/sat/sat_set.ys

+read_verilog ../top.v
+proc
+tee -o result.out sat -set x 3  middle

misc_reviewed/sat/sat_set_all_undef.ys

+read_verilog ../top.v
+proc
+ sat -set-all-undef x  middle

misc_reviewed/sat/sat_set_all_undef_at.ys

+read_verilog ../top.v
+proc
+tee -o result.out sat -prove x 0 -set-all-undef-at 1 x -tempinduct middle

misc_reviewed/sat/sat_set_all_undef_fail.pat

+ERROR: Failed to parse set-def expression `U'.

misc_reviewed/sat/sat_set_all_undef_fail.ys

+read_verilog ../top.v
+proc
+ sat -set-all-undef U  middle

misc_reviewed/sat/sat_set_any_undef.ys

+read_verilog ../top.v
+proc
+ sat -set-any-undef x  middle

misc_reviewed/sat/sat_set_any_undef_at.ys

+read_verilog ../top.v
+proc
+tee -o result.out sat -prove x 0 -set-any-undef-at 1 x  -tempinduct middle

misc_reviewed/sat/sat_set_assumes.ys

+read_verilog ../top.v
+proc
+ sat -set-assumes middle

misc_reviewed/sat/sat_set_at.pat

+Import set-constraint for this timestep: \\o = 1'1

misc_reviewed/sat/sat_set_at.ys

+read_verilog ../top.v
+proc
+tee -o result.out sat -prove x 0 -set-at 1 o 3  -tempinduct middle

misc_reviewed/sat/sat_set_def.ys

+read_verilog ../top.v
+proc
+ sat -set-def x  middle

misc_reviewed/sat/sat_set_def_at.ys

+read_verilog ../top.v
+proc
+tee -o result.out sat -prove x 0 -set-def-at 3 x  -tempinduct middle

misc_reviewed/sat/sat_set_def_fail.pat

+ERROR: Failed to parse set-def expression `U'.

misc_reviewed/sat/sat_set_def_fail.ys

+read_verilog ../top.v
+proc
+ sat -set-def U  middle

misc_reviewed/sat/sat_set_def_inputs.ys

+read_verilog ../top.v
+proc
+ sat -set-def-inputs  middle

misc_reviewed/sat/sat_set_diff_size_fail.pat

+ERROR: Set expression with different lhs and rhs sizes: x (\\x, 1 bits) vs. 2'b11 (2'11, 2 bits)

misc_reviewed/sat/sat_set_diff_size_fail.ys

+read_verilog ../top.v
+proc
+ sat -set x 2'b11  middle

misc_reviewed/sat/sat_set_init.ys

+read_verilog ../top.v
+proc
+ sat -set-init x 0  middle

misc_reviewed/sat/sat_set_init_def.ys

+read_verilog ../top.v
+proc
+ sat -set-init-def middle

misc_reviewed/sat/sat_set_init_undef.ys

+read_verilog ../top.v
+proc
+ sat -set-init-undef middle

misc_reviewed/sat/sat_set_init_zero.ys

+read_verilog ../top.v
+proc
+ sat -set-init-zero middle

misc_reviewed/sat/sat_set_lhs_fail.pat

+ERROR: Failed to parse lhs set expression

misc_reviewed/sat/sat_set_lhs_fail.ys

+read_verilog ../top.v
+proc
+ sat -set X 0  middle

misc_reviewed/sat/sat_set_rhs_fail.pat

+ERROR: Failed to parse rhs set expression

misc_reviewed/sat/sat_set_rhs_fail.ys

+read_verilog ../top.v
+proc
+ sat -set x X  middle

misc_reviewed/sat/sat_show.ys

+read_verilog ../top.v
+proc
+ sat -show x  middle

misc_reviewed/sat/sat_show_all.ys

+read_verilog ../top.v
+proc
+ sat -show-all middle

misc_reviewed/sat/sat_show_fail.pat

+ERROR: Failed to parse show expression `X'.

misc_reviewed/sat/sat_show_fail.ys

+read_verilog ../top.v
+proc
+ sat -show X middle

misc_reviewed/sat/sat_show_inputs.ys

+read_verilog ../top.v
+proc
+ sat -show-inputs middle

misc_reviewed/sat/sat_show_outputs.ys

+read_verilog ../top.v
+proc
+ sat -show-outputs middle

misc_reviewed/sat/sat_show_ports.ys

+read_verilog ../top.v
+proc
+ sat -show-ports middle

misc_reviewed/sat/sat_show_public.ys

+read_verilog ../top.v
+proc
+ sat -show-public middle

misc_reviewed/sat/sat_show_regs.ys

+read_verilog ../top.v
+proc
+ sat -ignore_unknown_cells -show-regs top

misc_reviewed/sat/sat_si_def_undef_fail.pat

+ERROR: The options -set-init-undef, -set-init-def, and -set-init-zero are exclusive!

misc_reviewed/sat/sat_si_def_undef_fail.ys

+read_verilog ../top.v
+proc
+ sat -set-init-undef -set-init-def middle

misc_reviewed/sat/sat_si_def_undef_zero_fail.pat

+ERROR: The options -set-init-undef, -set-init-def, and -set-init-zero are exclusive!

misc_reviewed/sat/sat_si_def_undef_zero_fail.ys

+read_verilog ../top.v
+proc
+ sat -set-init-undef -set-init-def -set-init-zero middle

misc_reviewed/sat/sat_si_def_zero_fail.pat

+ERROR: The options -set-init-undef, -set-init-def, and -set-init-zero are exclusive!

misc_reviewed/sat/sat_si_def_zero_fail.ys

+read_verilog ../top.v
+proc
+ sat -set-init-def -set-init-zero middle

misc_reviewed/sat/sat_si_undef_zero_fail.pat

+ERROR: The options -set-init-undef, -set-init-def, and -set-init-zero are exclusive!

misc_reviewed/sat/sat_si_undef_zero_fail.ys

+read_verilog ../top.v
+proc
+ sat -set-init-undef -set-init-zero middle

misc_reviewed/sat/sat_stepsize.pat

+Skipping prove for this step (-stepsize 2)

misc_reviewed/sat/sat_stepsize.ys

+read_verilog ../top.v
+proc
+tee -o result.out sat -tempinduct-skip 1 -stepsize 2 -prove x 0 -set-def-at 3 x  -tempinduct middle

misc_reviewed/sat/sat_tempinduct.ys

+read_verilog ../top.v
+proc
+ sat -prove x 1 -tempinduct  middle

misc_reviewed/sat/sat_tempinduct_baseonly.ys

+read_verilog ../top.v
+proc
+ sat -prove x 1 -tempinduct-baseonly  middle

misc_reviewed/sat/sat_tempinduct_baseonly_dump_cnf.ys

+read_verilog ../top.v
+proc
+# sat -prove x 1 -tempinduct-baseonly -maxsteps 6 -dump_cnf cnf.cnf  middle
+tee -o result.out sat -prove x 0 -set-def-at 3 x -dump_cnf cnf.cnf -tempinduct-baseonly middle

misc_reviewed/sat/sat_tempinduct_baseonly_dump_vcd.ys

+read_verilog ../top.v
+proc
+ sat -prove x 1 -tempinduct-baseonly -maxsteps 6 -dump_vcd vcd.vcd  middle

misc_reviewed/sat/sat_tempinduct_baseonly_maxsteps.ys

+read_verilog ../top.v
+proc
+ sat -prove x 1 -tempinduct-baseonly -maxsteps 1  middle

misc_reviewed/sat/sat_tempinduct_baseonly_maxsteps_6.ys

+read_verilog ../top.v
+proc
+ sat -prove x 1 -tempinduct-baseonly -maxsteps 6  middle

misc_reviewed/sat/sat_tempinduct_def.ys

+read_verilog ../top.v
+proc
+ sat -prove x 1 -tempinduct-def  middle

misc_reviewed/sat/sat_tempinduct_dump_cnf.ys

+read_verilog ../top.v
+proc
+tee -o result.out sat -tempinduct-skip 1 -prove x 0 -set-def-at 3 x -dump_cnf cnf.cnf -tempinduct middle

misc_reviewed/sat/sat_tempinduct_inductonly.ys

+read_verilog ../top.v
+proc
+ sat -prove x 1 -tempinduct-inductonly  middle

misc_reviewed/sat/sat_tempinduct_skip.pat

+Skipping prove for this step (-tempinduct-skip 1)

misc_reviewed/sat/sat_tempinduct_skip.ys

+read_verilog ../top.v
+proc
+tee -o result.out sat -tempinduct-skip 1 -prove x 0 -set-def-at 3 x  -tempinduct middle

misc_reviewed/sat/sat_tempinduct_tempinduct_baseonly.ys

+read_verilog ../top.v
+proc
+ sat -prove x 1 -tempinduct -tempinduct-baseonly  middle

misc_reviewed/sat/sat_tempinduct_tempinduct_def.ys

+read_verilog ../top.v
+proc
+ sat -prove x 1 -tempinduct -tempinduct-def  middle

misc_reviewed/sat/sat_timeout.ys

+read_verilog ../top.v
+proc
+ sat -timeout 0  -ignore_unknown_cells top

misc_reviewed/sat/sat_timeout_verify.ys

+read_verilog ../top.v
+proc
+ sat -timeout 1 -verify -ignore_unknown_cells top

misc_reviewed/sat/sat_unset_at.pat

+Import unset-constraint for this timestep: \\o

misc_reviewed/sat/sat_unset_at.ys

+read_verilog ../top.v
+proc
+tee -o result.out sat -prove x 0 -unset-at 1 o -tempinduct middle

misc_reviewed/sat/sat_verify.ys

+read_verilog ../top.v
+proc
+ sat -verify -ignore_unknown_cells -show x,y -set x y -set x 1 top

misc_reviewed/sat/sat_verify_fail.pat

+ERROR: Called with -verify and proof did fail!

misc_reviewed/sat/sat_verify_fail.ys

+read_verilog ../top.v
+proc
+ sat -verify -prove x 1 -tempinduct middle

misc_reviewed/sat/sat_verify_no_timeout.ys

+read_verilog ../top.v
+proc
+ sat -verify-no-timeout -ignore_unknown_cells -show x,y -set x y -set x 1 top

misc_reviewed/sat/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+(* init = 1'h0 *)
+ output reg A,
+ output cout
+ );
+
+ parameter X = 1;
+ wire o;
+
+ initial A = 0;
+ initial cout = 0;
+
+always @(posedge cin)
+	A <= o;
+
+assign cout =  cin? y : x;
+
+middle u_mid (.x(x),.o(o));
+u_rtl inst_u_rtl (.x(x),.o(o));
+
+endmodule
+
+module middle
+(
+	input x,
+	input y,
+	output o
+);
+
+assign o = x + y;
+endmodule
+
+module u_rtl
+(
+	input x,
+	input y,
+	output o
+);
+
+initial o = 0;
+
+assign o = x + y;
+endmodule

misc_reviewed/sat/top_div_by_zery.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+(* init = 1'h0 *)
+ output reg A,
+ output cout
+ );
+
+ parameter X = 1;
+ wire o;
+
+ initial A = 0;
+ initial cout = 0;
+
+always @(posedge cin)
+	A <= o;
+
+assign cout =  cin? y : x;
+
+middle u_mid (.x(x),.o(o));
+u_rtl inst_u_rtl (.x(x),.o(o));
+
+endmodule
+
+module middle
+(
+	input x,
+	input y,
+	output o
+);
+
+assign o = x + y;
+endmodule
+
+module u_rtl
+(
+	input x,
+	input y,
+	output o
+);
+
+initial o = 0;
+
+assign o = x / 0;
+endmodule

misc_reviewed/sat/top_ff.v

+module adff
+    (d, clk, clr, q);
+     input d, clk, clr;
+	(* init = 1'h0 *)
+    output reg q;
+    initial begin
+      q = 0;
+    end
+	always @( posedge clk, posedge clr )
+		if ( clr )
+			q <= 1'b0;
+		else
+            q <= d;
+endmodule

misc_reviewed/sat/top_fsm.v

+ module fsm (
+ clock,
+ reset,
+ req_0,
+ req_1,
+ gnt_0,
+ gnt_1
+ );
+ input   clock,reset,req_0,req_1;
+ output  gnt_0,gnt_1;
+ wire    clock,reset,req_0,req_1;
+ reg     gnt_0,gnt_1;
+
+ parameter SIZE = 3           ;
+ parameter IDLE  = 3'b001,GNT0 = 3'b010,GNT1 = 3'b100,GNT2 = 3'b101 ;
+
+ reg [SIZE-1:0] state;
+ reg [SIZE-1:0] next_state;
+
+ always @ (posedge clock)
+ begin : FSM
+ if (reset == 1'b1) begin
+   state <=  #1  IDLE;
+   gnt_0 <= 0;
+   gnt_1 <= 0;
+ end else
+  case(state)
+    IDLE : if (req_0 == 1'b1) begin
+                 state <=  #1  GNT0;
+                 gnt_0 <= 1;
+               end else if (req_1 == 1'b1) begin
+                 gnt_1 <= 1;
+                 state <=  #1  GNT0;
+               end else begin
+                 state <=  #1  IDLE;
+               end
+    GNT0 : if (req_0 == 1'b1) begin
+                 state <=  #1  GNT0;
+               end else begin
+                 gnt_0 <= 0;
+                 state <=  #1  IDLE;
+               end
+    GNT1 : if (req_1 == 1'b1) begin
+                 state <=  #1  GNT2;
+				 gnt_1 <= req_0;
+               end
+    GNT2 : if (req_0 == 1'b1) begin
+                 state <=  #1  GNT1;
+				 gnt_1 <= req_1;
+               end
+    default : state <=  #1  IDLE;
+ endcase
+ end
+
+ endmodule
+
+ module top (
+input clk,
+input rst,
+input a,
+input b,
+output g0,
+output g1
+);
+
+fsm u_fsm ( .clock(clk),
+            .reset(rst),
+            .req_0(a),
+            .req_1(b),
+            .gnt_0(g0),
+            .gnt_1(g1));
+
+endmodule

misc_reviewed/sat/top_initstate.v

+module middle
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout
+ );
+
+ reg ASSERT = 1;
+ (* anyconst *) reg foo;
+ (* anyseq *) reg too;
+
+ initial begin
+    begin
+        A = 0;
+        cout = 0;
+    end
+ end
+
+always @(posedge x) begin
+    if ($initstate)
+        A <= 0;
+    A <=  y + cin + too;
+    assume(too);
+    assume(s_eventually too);
+end
+always @(negedge x) begin
+    if ($initstate)
+        cout <= 0;
+        cout <=  y + A + foo;
+    assert(ASSERT);
+    assert(s_eventually ASSERT);
+end
+
+endmodule

misc_reviewed/sat/top_mux.v

+module mux2 (S,A,B,Y);
+    input S;
+    input A,B;
+    output reg Y;
+
+    always @(*)
+		Y = (S)? B : A;
+endmodule
+
+module mux4 ( S, D, Y );
+
+input[1:0] S;
+input[3:0] D;
+output Y;
+
+reg Y;
+wire[1:0] S;
+wire[3:0] D;
+
+always @*
+     begin
+        case( S )
+            0 : Y = D[0];
+            1 : Y = D[1];
+            2 : Y = D[2];
+            3 : Y = D[3];
+            default: Y = 1'bx;
+        endcase
+     end
+
+endmodule
+
+module mux8 ( S, D, Y );
+
+input[2:0] S;
+input[7:0] D;
+output Y;
+
+reg Y;
+wire[2:0] S;
+wire[7:0] D;
+
+always @*
+     begin
+        case( S )
+            0 : Y = D[0];
+            1 : Y = D[1];
+            2 : Y = D[2];
+            3 : Y = D[3];
+            4 : Y = D[4];
+            5 : Y = D[5];
+            6 : Y = D[6];
+            7 : Y = D[7];
+            default: Y = 1'bx;
+        endcase
+     end
+
+endmodule
+
+module mux16 (D, S, Y);
+ 	input  [15:0] D;
+ 	input  [3:0] S;
+ 	output Y;
+
+reg Y;
+wire[3:0] S;
+wire[15:0] D;
+
+always @*
+     begin
+        case( S )
+            0 : Y = D[0];
+            1 : Y = D[1];
+            2 : Y = D[2];
+            3 : Y = D[3];
+            4 : Y = D[4];
+            5 : Y = D[5];
+            6 : Y = D[6];
+            7 : Y = D[7];
+            8 : Y = D[8];
+            9 : Y = D[9];
+            10 : Y = D[10];
+            11 : Y = D[11];
+            12 : Y = D[12];
+            13 : Y = D[13];
+            14 : Y = D[14];
+            15 : Y = D[15];
+            default: Y = 1'bx;
+        endcase
+     end
+
+endmodule
+
+
+module top (
+input [3:0] S,
+input [15:0] D,
+output M2,M4,M8,M16
+);
+
+mux2 u_mux2 (
+        .S (S[0]),
+        .A (D[0]),
+        .B (D[1]),
+        .Y (M2)
+    );
+
+
+mux4 u_mux4 (
+        .S (S[1:0]),
+        .D (D[3:0]),
+        .Y (M4)
+    );
+
+mux8 u_mux8 (
+        .S (S[2:0]),
+        .D (D[7:0]),
+        .Y (M8)
+    );
+
+mux16 u_mux16 (
+        .S (S[3:0]),
+        .D (D[15:0]),
+        .Y (M16)
+    );
+
+endmodule

misc_reviewed/sat/top_reg.v

+module dut(
+	input fast_clk, slow_clk,
+	input [3:0] waddr, raddr,
+	input [3:0] wdata,
+	input wen,
+	output [3:0] rdata
+);
+
+	reg [3:0] mem[0:15];
+	reg [3:0] raddr_reg;
+
+	always @(posedge fast_clk) begin
+		if (wen)
+			mem[waddr] <= wdata;
+	end
+
+	always @(posedge slow_clk)
+		raddr_reg <= raddr;
+
+	assign rdata = mem[raddr_reg];
+endmodule

misc_reviewed/scatter/scatter.pat

+wire $auto$scatter

misc_reviewed/scatter/scatter.ys

+read_verilog ../top.v
+proc
+scatter
+tee -o result.out dump

misc_reviewed/scatter/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output cout
+ );
+ wire o;
+
+always @(posedge cin)
+	A <= o;
+
+assign cout =  cin? y : x;
+
+middle u_mid (x,y,o);
+
+endmodule
+
+module middle
+(
+	input x,
+	input y,
+	output o
+);
+
+assign o = x + y;
+endmodule

misc_reviewed/scc/scc.pat

+Found 1 SCCs in module top.

misc_reviewed/scc/scc.ys

+read_verilog ../top.v
+scc top
+proc
+scc top
+synth
+tee -o result.out scc top

misc_reviewed/scc/scc_all_cell_types.ys

+read_verilog ../top.v
+proc
+ scc -all_cell_types top

misc_reviewed/scc/scc_expect.pat

+Found and expected 0 SCCs.

misc_reviewed/scc/scc_expect.ys

+read_verilog ../top_no_feedback.v
+proc
+tee -o result.out scc -expect 0 top

misc_reviewed/scc/scc_expect_fail.pat

+ERROR: Found 1 SCCs but expected 0.

misc_reviewed/scc/scc_expect_fail.ys

+read_verilog ../top.v
+proc
+ scc -expect 0 top

misc_reviewed/scc/scc_hier_feedback.ys

+read_verilog ../top_hier_feedback.v
+ scc top
+proc
+ scc top
+synth
+ scc top

misc_reviewed/scc/scc_max_depth.ys

+read_verilog ../top.v
+proc
+ scc -max_depth 2 top

misc_reviewed/scc/scc_no_feedback.ys

+read_verilog ../top_no_feedback.v
+ scc top
+proc
+ scc top
+synth
+ scc top

misc_reviewed/scc/scc_nofeedback.ys

+read_verilog ../top.v
+proc
+ scc -nofeedback top

misc_reviewed/scc/scc_select.ys

+read_verilog ../top.v
+synth -top top
+ scc -select top

misc_reviewed/scc/scc_set_attr.ys

+read_verilog ../top.v
+proc
+ scc -set_attr attr true top

misc_reviewed/scc/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output cout
+ );
+ parameter X = 1;
+ wire o_mid,o_rtl;
+
+always @(posedge cin)
+	A <= o_mid;
+
+assign o_mid = x & o_rtl;
+assign o_rtl = y & o_mid;
+
+endmodule

misc_reviewed/scc/top_hier_feedback.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output cout
+ );
+ parameter X = 1;
+ wire o_mid,o_rtl;
+
+always @(posedge cin)
+	A <= o_mid;
+
+middle u_mid (.x(x),.y(o_rtl),.o(o_mid));
+u_rtl inst_u_rtl (.x(o_mid),.y(y),.o(o_rtl));
+
+endmodule
+
+module middle
+(
+	input x,
+	input y,
+	output o
+);
+
+wire o1,o2;
+
+assign o1 = x & o2;
+assign o2 = y & o1;
+assign o = o1;
+endmodule
+
+module u_rtl
+(
+	input x,
+	input y,
+	output o
+);
+
+
+wire o1,o2;
+
+assign o1 = x & o2;
+assign o2 = y & o1;
+assign o = o1;
+endmodule

misc_reviewed/scc/top_no_feedback.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output cout
+ );
+ wire o;
+
+always @(posedge cin)
+	A <= o;
+
+assign cout =  cin? y : x;
+
+middle u_mid (x,y,o);
+
+endmodule
+
+module middle
+(
+	input x,
+	input y,
+	output o
+);
+
+assign o = x + y;
+endmodule

misc_reviewed/script/script.ys

+read_verilog ../top.v
+tee -o result.log dump

misc_reviewed/script/script_from_to.ys

+tee -o result.log script ../script.ys 1:3

misc_reviewed/script/script_no_opt.ys

+tee -o result.log script ../script.ys

misc_reviewed/script/script_scriptwire.ys

+tee -o result.log script -scriptwire ../script.ys

misc_reviewed/script/top.v

+(* black_box *) module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output A,
+ output cout
+ );
+
+assign {cout,A} =  cin + y + x;
+
+endmodule

misc_reviewed/select/select.ys

+read_verilog ../top.v
+proc
+ select
+ select -list

misc_reviewed/select/select_%.pat

+top/$ternary
+top/$ternary

misc_reviewed/select/select_%.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %coe:+[Y] */t:$mux %
+ select */t:$mux %coe:+[Y] */t:$mux %%
+tee -o result.out select -list

misc_reviewed/select/select_%C.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %coe:+[Y] */t:$mux %C

misc_reviewed/select/select_%D.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %x:+[A] */t:$mux %D
+ select -list

misc_reviewed/select/select_%M.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %coe:+[Y] */t:$mux %M
+ select -list

misc_reviewed/select/select_%R.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %coe:+[Y] */t:$mux %R
+ select */w:o %R
+ select -list

misc_reviewed/select/select_%R4.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %coe:+[Y] */t:$mux %R 4
+ select -list

misc_reviewed/select/select_%a.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %coe:+[Y] */t:$mux %a
+ select -list

misc_reviewed/select/select_%c.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %coe:+[Y] */t:$mux %c

misc_reviewed/select/select_%ci.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %ci:+[A] */t:$mux

misc_reviewed/select/select_%cie.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %cie:+[A] */t:$mux

misc_reviewed/select/select_%co.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %co:+[Y] */t:$mux
+ select -list

misc_reviewed/select/select_%coe.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %coe:+[Y] */t:$mux
+ select -list

misc_reviewed/select/select_%d.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %x:+[A] */t:$mux %d
+ select -list

misc_reviewed/select/select_%i.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %coe:+[Y] */t:$mux %i
+ select -list

misc_reviewed/select/select_%i_mem.ys

+read_verilog ../top_mem.v
+proc
+ select * * * %i
+ select -list

misc_reviewed/select/select_%m.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %coe:+[Y] */t:$mux %m
+ select -list

misc_reviewed/select/select_%n.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %coe:+[Y] */t:$mux %n
+ select -list

misc_reviewed/select/select_%n_full_sel.ys

+read_verilog ../top_mem.v
+ select * %n
+proc
+ select * %n
+ select -list

misc_reviewed/select/select_%n_mem.ys

+read_verilog ../top_mem.v
+ select */p:$proc %coe:+[Y] */p:$proc %n
+ select */t:$memrd %coe:+[Y] */t:$memwr %n
+proc
+ select */t:$memrd %coe:+[Y] */t:$memwr %n
+ select -list

misc_reviewed/select/select_%s.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %coe:+[Y] */t:$mux %s
+ select -list

misc_reviewed/select/select_%s_full_sel.ys

+read_verilog ../top.v
+proc
+ select * %s
+ select -list

misc_reviewed/select/select_%u.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %coe:+[Y] */t:$mux %u
+ select -list

misc_reviewed/select/select_%x_%D.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %x:+[A] */t:$mux %D
+ select -list

misc_reviewed/select/select_%x_%d.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %x:+[A] */t:$mux %d
+ select -list

misc_reviewed/select/select_%xe.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %xe:+[A] */t:$mux
+ select -list

misc_reviewed/select/select_add.ys

+read_verilog ../top.v
+proc
+ select -add top
+ select -list

misc_reviewed/select/select_add_A.pat

+middle
+middle/$add$../top.v:32$3_Y
+middle/o
+middle/y
+middle/x
+middle/$add$../top.v:32$3
+top
+top/$ternary$../top.v:16$2_Y
+top/$0\A[0:0]
+top/o
+top/cout
+top/A
+top/cin
+top/y
+top/x
+top/$procdff$4
+top/u_mid
+top/$ternary$../top.v:16$2

misc_reviewed/select/select_add_A.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add A:\cells_not_processed
+tee -o result.out select -list

misc_reviewed/select/select_add_A_eq.pat

+middle
+middle/$add$../top.v:32$3_Y
+middle/o
+middle/y
+middle/x
+middle/$add$../top.v:32$3
+top
+top/$ternary$../top.v:16$2_Y
+top/$0\A[0:0]
+top/o
+top/cout
+top/A
+top/cin
+top/y
+top/x
+top/$procdff$4
+top/u_mid
+top/$ternary$../top.v:16$2

misc_reviewed/select/select_add_A_eq.ys

+read_verilog ../top.v
+proc
+ select -del *
+select -add A:\cells_not_processed=1
+tee -o result.out select -list

misc_reviewed/select/select_add_A_less.pat

+middle
+middle/$add$../top.v:32$3_Y
+middle/o
+middle/y
+middle/x
+middle/$add$../top.v:32$3
+top
+top/$ternary$../top.v:16$2_Y
+top/$0\A[0:0]
+top/o
+top/cout
+top/A
+top/cin
+top/y
+top/x
+top/$procdff$4
+top/u_mid
+top/$ternary$../top.v:16$2

misc_reviewed/select/select_add_A_less.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add A:\cells_not_processed<2
+tee -o result.out select -list

misc_reviewed/select/select_add_A_lesseq.pat

+middle
+middle/$add$../top.v:32$3_Y
+middle/o
+middle/y
+middle/x
+middle/$add$../top.v:32$3
+top
+top/$ternary$../top.v:16$2_Y
+top/$0\A[0:0]
+top/o
+top/cout
+top/A
+top/cin
+top/y
+top/x
+top/$procdff$4
+top/u_mid
+top/$ternary$../top.v:16$2

misc_reviewed/select/select_add_A_lesseq.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add A:\cells_not_processed<=1
+tee -o result.out select -list

misc_reviewed/select/select_add_A_more.pat

+middle
+middle/$add$../top.v:32$3_Y
+middle/o
+middle/y
+middle/x
+middle/$add$../top.v:32$3
+top
+top/$ternary$../top.v:16$2_Y
+top/$0\A[0:0]
+top/o
+top/cout
+top/A
+top/cin
+top/y
+top/x
+top/$procdff$4
+top/u_mid
+top/$ternary$../top.v:16$2

misc_reviewed/select/select_add_A_more.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add A:\cells_not_processed>0
+tee -o result.out select -list

misc_reviewed/select/select_add_A_moreeq.pat

+middle
+middle/$add$../top.v:32$3_Y
+middle/o
+middle/y
+middle/x
+middle/$add$../top.v:32$3
+top
+top/$ternary$../top.v:16$2_Y
+top/$0\A[0:0]
+top/o
+top/cout
+top/A
+top/cin
+top/y
+top/x
+top/$procdff$4
+top/u_mid
+top/$ternary$../top.v:16$2

misc_reviewed/select/select_add_A_moreeq.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add A:\cells_not_processed>=1
+tee -o result.out select -list

misc_reviewed/select/select_add_A_neq.pat

+middle
+middle/$add$../top.v:32$3_Y
+middle/o
+middle/y
+middle/x
+middle/$add$../top.v:32$3
+top
+top/$ternary$../top.v:16$2_Y
+top/$0\A[0:0]
+top/o
+top/cout
+top/A
+top/cin
+top/y
+top/x
+top/$procdff$4
+top/u_mid
+top/$ternary$../top.v:16$2

misc_reviewed/select/select_add_A_neq.ys

+read_verilog ../top.v
+proc
+ select -del *
+select -add A:\cells_not_processed!=0
+tee -o result.out select -list

misc_reviewed/select/select_add_a.pat

+top/u_mid

misc_reviewed/select/select_add_a.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add a:\module_not_derived
+tee -o result.out select -list

misc_reviewed/select/select_add_a_eq.pat

+top/u_mid

misc_reviewed/select/select_add_a_eq.ys

+read_verilog ../top.v
+proc
+ select -del *
+select -add a:\module_not_derived=1
+tee -o result.out select -list

misc_reviewed/select/select_add_a_less.pat

+top/u_mid

misc_reviewed/select/select_add_a_less.ys

+read_verilog ../top.v
+proc
+ select -del *
+select -add a:\module_not_derived<2
+tee -o result.out select -list

misc_reviewed/select/select_add_a_lesseq.pat

+top/u_mid

misc_reviewed/select/select_add_a_lesseq.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add a:\module_not_derived<=2
+tee -o result.out select -list

misc_reviewed/select/select_add_a_mem.ys

+read_verilog ../top_mem.v
+proc
+ select -add a:*

misc_reviewed/select/select_add_a_more.pat

+top/u_mid

misc_reviewed/select/select_add_a_more.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add a:\module_not_derived>0
+tee -o result.out select -list

misc_reviewed/select/select_add_a_moreeq.pat

+top/u_mid

misc_reviewed/select/select_add_a_moreeq.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add a:\module_not_derived>=1
+tee -o result.out select -list

misc_reviewed/select/select_add_a_proc.pat

+middle
+middle/$add
+middle/o
+middle/y
+middle/x
+middle/$add
+top
+top/$ternary
+top/$0\\A\[0:0\]
+top/o
+top/cout
+top/A
+top/cin
+top/y
+top/x
+top/u_mid
+top/$ternary
+top/$proc

misc_reviewed/select/select_add_a_proc.ys

+read_verilog ../top.v
+ select -del *
+ select -add a:\src
+tee -o result.out select -list

misc_reviewed/select/select_add_all.ys

+read_verilog ../top.v
+proc
+ select -add *
+ select -list

misc_reviewed/select/select_add_c.pat

+procdff

misc_reviewed/select/select_add_c.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add c:$procdff$*
+tee -o result.out select -list

misc_reviewed/select/select_add_i.pat

+middle/x
+top/x

misc_reviewed/select/select_add_i.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add i:x
+tee -o result.out select -list

misc_reviewed/select/select_add_m.ys

+read_verilog ../top.v
+proc
+ select -add m:*
+ select -list

misc_reviewed/select/select_add_m_mem.pat

+top/ram

misc_reviewed/select/select_add_m_mem.ys

+read_verilog ../top_mem.v
+proc
+ select -del *
+ select -add m:\ram
+tee -o result.out select -list

misc_reviewed/select/select_add_mid.pat

+top/u_mid

misc_reviewed/select/select_add_mid.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add c:\u_mid
+tee -o result.out select -list

misc_reviewed/select/select_add_n.pat

+top/u_mid

misc_reviewed/select/select_add_n.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add n:\u_mid
+tee -o result.out select -list

misc_reviewed/select/select_add_n_mem.ys

+read_verilog ../top_mem.v
+ select -add n:*
+proc
+ select -add n:*
+ select -list

misc_reviewed/select/select_add_o.pat

+top/A

misc_reviewed/select/select_add_o.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add o:A
+tee -o result.out select -list

misc_reviewed/select/select_add_obj.ys

+read_verilog ../top.v
+proc
+ select -add top/o
+ select -list

misc_reviewed/select/select_add_p.pat

+top/$proc

misc_reviewed/select/select_add_p.ys

+read_verilog ../top.v
+ select -del *
+ select -add p:$proc*
+tee -o result.out select -list

misc_reviewed/select/select_add_r.pat

+top/$ternary

misc_reviewed/select/select_add_r.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add r:\WIDTH
+tee -o result.out select -list

misc_reviewed/select/select_add_r_eq.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add r:\WIDTH=1
+tee -o result.out select -list

misc_reviewed/select/select_add_r_eq_str.ys

+read_verilog ../top_mem.v
+proc
+ select -del *
+ select -add r:\MEMID="\\ram"
+tee -o result.out select -list

misc_reviewed/select/select_add_r_less.pat

+top/$ternary

misc_reviewed/select/select_add_r_less.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add r:\WIDTH<2
+tee -o result.out select -list

misc_reviewed/select/select_add_r_less_str.ys

+read_verilog ../top_mem.v
+proc
+ select -del *
+ select -add r:\MEMID<"\\ram"
+tee -o result.out select -list

misc_reviewed/select/select_add_r_lesseq.pat

+top/$ternary

misc_reviewed/select/select_add_r_lesseq.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add r:\WIDTH<=1
+tee -o result.out select -list

misc_reviewed/select/select_add_r_lesseq_str.ys

+read_verilog ../top_mem.v
+proc
+ select -del *
+ select -add r:\MEMID<="\\ram"
+tee -o result.out select -list

misc_reviewed/select/select_add_r_more.pat

+top/$ternary

misc_reviewed/select/select_add_r_more.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add r:\WIDTH>0
+tee -o result.out select -list

misc_reviewed/select/select_add_r_more_str.ys

+read_verilog ../top_mem.v
+proc
+ select -del *
+ select -add r:\MEMID>"\\ram"
+tee -o result.out select -list

misc_reviewed/select/select_add_r_moreeq.pat

+top/$ternary

misc_reviewed/select/select_add_r_moreeq.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add r:\WIDTH>=1
+tee -o result.out select -list

misc_reviewed/select/select_add_r_moreeq_str.ys

+read_verilog ../top_mem.v
+proc
+ select -del *
+ select -add r:\MEMID>="\\ram"
+tee -o result.out select -list

misc_reviewed/select/select_add_r_neq.pat

+top/$ternary

misc_reviewed/select/select_add_r_neq.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add r:\WIDTH!0
+tee -o result.out select -list

misc_reviewed/select/select_add_r_neq_str.pat

+$memwr

misc_reviewed/select/select_add_r_neq_str.ys

+read_verilog ../top_mem.v
+proc
+ select -del *
+ select -add r:\MEMID!"\\rom"
+tee -o result.out select -list

misc_reviewed/select/select_add_s.pat

+middle/$add
+middle/o
+middle/y
+middle/x
+top/$ternary
+top/$0\\A\[0:0\]
+top/o
+top/cout
+top/A
+top/cin
+top/y
+top/x

misc_reviewed/select/select_add_s.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add s:1
+tee -o result.out select -list

misc_reviewed/select/select_add_ss.pat

+middle/$add
+middle/o
+middle/y
+middle/x
+top/$ternary
+top/$0\\A\[0:0\]
+top/o
+top/cout
+top/A
+top/cin
+top/y
+top/x

misc_reviewed/select/select_add_ss.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add s:1:6
+tee -o result.out select -list

misc_reviewed/select/select_add_t.pat

+middle/$add

misc_reviewed/select/select_add_t.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add t:$add
+tee -o result.out select -list

misc_reviewed/select/select_add_w.pat

+middle/o
+top/o

misc_reviewed/select/select_add_w.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add w:o
+tee -o result.out select -list

misc_reviewed/select/select_add_with_del_fail.pat

+ERROR: Options -add, -del, -assert-none, -assert-any, assert-count, -assert-max or -assert-min can not be combined.

misc_reviewed/select/select_add_with_del_fail.ys

+read_verilog ../top.v
+proc
+ select -add -del
+ select -list

misc_reviewed/select/select_add_x.pat

+middle/o

misc_reviewed/select/select_add_x.ys

+read_verilog ../top.v
+proc
+ select -del *
+ select -add x:o
+tee -o result.out select -list

misc_reviewed/select/select_all.pat

+top
+top/$ternary
+top/cout
+top/cin
+top/y
+top/x
+top/$ternary

misc_reviewed/select/select_all.ys

+read_verilog ../top_mux.v
+proc
+ select -del *
+ select *
+tee -o result.out select -list

misc_reviewed/select/select_assert_any.ys

+read_verilog ../top.v
+ select -assert-any  top
+proc
+ select -assert-any  top

misc_reviewed/select/select_assert_any_failed_fail.pat

+ERROR: Assertion failed: selection is empty: uuu

misc_reviewed/select/select_assert_any_failed_fail.ys

+read_verilog ../top.v
+proc
+ select -assert-any uuu
+ select -list

misc_reviewed/select/select_assert_any_with_count_fail.pat

+ERROR: Options -add, -del, -assert-none, -assert-any, assert-count, -assert-max or -assert-min can not be combined.

misc_reviewed/select/select_assert_any_with_count_fail.ys

+read_verilog ../top.v
+proc
+ select -assert-any -assert-count 3 top
+ select -list

misc_reviewed/select/select_assert_count.ys

+read_verilog ../top.v
+ select -assert-count 11 top
+proc
+ select -assert-count 11 top

misc_reviewed/select/select_assert_count_failed_fail.pat

+ERROR: Assertion failed: selection contains 11 elements instead of the asserted 30: top
+Selection contains:

misc_reviewed/select/select_assert_count_failed_fail.ys

+read_verilog ../top.v
+proc
+ select -assert-count 30 top
+ select -list

misc_reviewed/select/select_assert_count_mem.ys

+read_verilog ../top_mem.v
+ select -assert-count 32 top
+proc
+ select -assert-count 62 top

misc_reviewed/select/select_assert_list_with_assert_max_fail.pat

+ERROR: Options -list, -write and -count can not be combined with -add, -del, -assert-none, -assert-any, assert-count, -assert-max, or -assert-min.

misc_reviewed/select/select_assert_list_with_assert_max_fail.ys

+read_verilog ../top.v
+proc
+ select -list -assert-max 3 top
+ select -list

misc_reviewed/select/select_assert_list_with_del_fail.pat

+ERROR: Options -list, -write and -count can not be combined with -add, -del, -assert-none, -assert-any, assert-count, -assert-max, or -assert-min.

misc_reviewed/select/select_assert_list_with_del_fail.ys

+read_verilog ../top.v
+proc
+ select -list -del
+ select -list

misc_reviewed/select/select_assert_max.ys

+read_verilog ../top.v
+ select -assert-max 15 top
+proc
+ select -assert-max 15 top

misc_reviewed/select/select_assert_max_failed_fail.pat

+ERROR: Assertion failed: selection contains 11 elements, more than the maximum number 1: top

misc_reviewed/select/select_assert_max_failed_fail.ys

+read_verilog ../top.v
+proc
+ select -assert-max 1 top
+ select -list

misc_reviewed/select/select_assert_max_mem.ys

+read_verilog ../top_mem.v
+ select -assert-max 32 top
+proc
+ select -assert-max 62 top

misc_reviewed/select/select_assert_max_with_del_fail.pat

+ERROR: Options -add, -del, -assert-none, -assert-any, assert-count, -assert-max or -assert-min can not be combined.

misc_reviewed/select/select_assert_max_with_del_fail.ys

+read_verilog ../top.v
+proc
+ select  -del -assert-max 3 top
+ select -list

misc_reviewed/select/select_assert_min.ys

+read_verilog ../top.v
+ select -assert-min 2 top
+proc
+ select -assert-min 2 top

misc_reviewed/select/select_assert_min_failed_fail.pat

+ERROR: Assertion failed: selection contains 11 elements, less than the minimum number 30: top

misc_reviewed/select/select_assert_min_failed_fail.ys

+read_verilog ../top.v
+proc
+ select -assert-min 30 top
+ select -list

misc_reviewed/select/select_assert_none.ys

+read_verilog ../top.v
+select -none
+ select -assert-none x
+proc
+select -none
+ select -assert-none x

misc_reviewed/select/select_assert_none_failed_fail.pat

+ERROR: Assertion failed: selection is not empty: top

misc_reviewed/select/select_assert_none_failed_fail.ys

+read_verilog ../top.v
+proc
+select *
+ select -assert-none top
+ select -list

misc_reviewed/select/select_assert_none_with_min_fail.pat

+ERROR: Options -add, -del, -assert-none, -assert-any, assert-count, -assert-max or -assert-min can not be combined.

misc_reviewed/select/select_assert_none_with_min_fail.ys

+read_verilog ../top.v
+proc
+ select -assert-none -assert-min 3 top
+ select -list

misc_reviewed/select/select_cant_open_for_reading_fail.pat

+ERROR: Can't open 'txt.txt' for reading: No such file or directory

misc_reviewed/select/select_cant_open_for_reading_fail.ys

+read_verilog ../top.v
+proc
+ select -read txt.txt
+ select -list

misc_reviewed/select/select_cant_open_for_writing_fail.pat

+ERROR: Can't open './tt/ot.txt' for writing: No such file or directory

misc_reviewed/select/select_cant_open_for_writing_fail.ys

+read_verilog ../top.v
+proc
+ select -write ./tt/ot.txt
+ select -list

misc_reviewed/select/select_clear.ys

+read_verilog ../top.v
+proc
+select -add top -add middle
+ select -clear
+ select -list

misc_reviewed/select/select_clear_with_other_opt_fail.pat

+ERROR: Option -clear can not be combined with any other options.

misc_reviewed/select/select_clear_with_other_opt_fail.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %x:+[A] */t:$mux %D -clear
+ select -list

misc_reviewed/select/select_count.pat

+16 objects.

misc_reviewed/select/select_count.ys

+read_verilog ../top.v
+proc
+tee -o result.out select -count

misc_reviewed/select/select_count_with_assert_min_fail.pat

+ERROR: Options -list, -write and -count can not be combined with -add, -del, -assert-none, -assert-any, assert-count, -assert-max, or -assert-min.

misc_reviewed/select/select_count_with_assert_min_fail.ys

+read_verilog ../top.v
+proc
+ select -count 11 -assert-min 33 top
+ select -list

misc_reviewed/select/select_count_with_assert_none_fail.pat

+ERROR: Options -list, -write and -count can not be combined with -add, -del, -assert-none, -assert-any, assert-count, -assert-max, or -assert-min.

misc_reviewed/select/select_count_with_assert_none_fail.ys

+read_verilog ../top.v
+proc
+ select  -assert-none -count 3 top
+ select -list

misc_reviewed/select/select_del.pat

+middle
+middle/$add
+middle/o
+middle/y
+middle/x
+middle/$add

misc_reviewed/select/select_del.ys

+read_verilog ../top.v
+proc
+ select -del top
+tee -o result.out select -list

misc_reviewed/select/select_error_in_expand_op_fail.pat

+ERROR: Syntax error in expand operator '%x:'.

misc_reviewed/select/select_error_in_expand_op_fail.ys

+read_verilog ../top.v
+proc
+ select select */t:$mux %x: */t:$mux %d
+ select -list

misc_reviewed/select/select_list.pat

+top
+top/$ternary
+top/cout
+top/cin
+top/y
+top/x
+top/$ternary

misc_reviewed/select/select_list.ys

+read_verilog ../top_mux.v
+proc
+tee -o result.out select -list

misc_reviewed/select/select_module.pat

+middle
+middle/$add
+middle/o
+middle/y
+middle/x
+middle/$add

misc_reviewed/select/select_module.ys

+read_verilog ../top.v
+proc
+select -add top -add middle
+ select -module middle
+tee -o result.out select -list

misc_reviewed/select/select_module_mem.pat

+read_verilog ../top_mem.v
+proc
+select -add top -add top
+ select -module top

misc_reviewed/select/select_module_mem.ys

+read_verilog ../top_mem.v
+proc
+select -add top -add top
+ select -module top
+tee -o result.out select -list

misc_reviewed/select/select_no_sel_to_check_as_any_fail.pat

+ERROR: No selection to check.

misc_reviewed/select/select_no_sel_to_check_as_any_fail.ys

+read_verilog ../top.v
+proc
+ select -assert-any
+ select -list

misc_reviewed/select/select_no_sel_to_check_as_count_fail.pat

+ERROR: No selection to check.

misc_reviewed/select/select_no_sel_to_check_as_count_fail.ys

+read_verilog ../top.v
+proc
+ select -assert-count 3
+ select -list

misc_reviewed/select/select_no_sel_to_check_as_max_fail.pat

+ERROR: No selection to check.

misc_reviewed/select/select_no_sel_to_check_as_max_fail.ys

+read_verilog ../top.v
+proc
+ select -assert-max 3
+ select -list

misc_reviewed/select/select_no_sel_to_check_as_min_fail.pat

+ERROR: No selection to check.

misc_reviewed/select/select_no_sel_to_check_as_min_fail.ys

+read_verilog ../top.v
+proc
+ select -assert-min 3
+ select -list

misc_reviewed/select/select_no_sel_to_check_as_none_fail.pat

+ERROR: No selection to check.

misc_reviewed/select/select_no_sel_to_check_as_none_fail.ys

+read_verilog ../top.v
+proc
+ select -assert-none
+ select -list

misc_reviewed/select/select_no_such_module_fail.pat

+ERROR: No such module: x

misc_reviewed/select/select_no_such_module_fail.ys

+read_verilog ../top.v
+proc
+ select -module x
+ select -list

misc_reviewed/select/select_none.ys

+read_verilog ../top.v
+proc
+select -add top -add middle
+ select -none

misc_reviewed/select/select_none_with_other_opt_fail.pat

+ERROR: Option -none can not be combined with any other options.

misc_reviewed/select/select_none_with_other_opt_fail.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %x:+[A] */t:$mux %D -none
+ select -list

misc_reviewed/select/select_nothing_to_add_fail.pat

+ERROR: Nothing to add to selection.

misc_reviewed/select/select_nothing_to_add_fail.ys

+read_verilog ../top.v
+proc
+ select -add
+ select -list

misc_reviewed/select/select_nothing_to_del_fail.pat

+ERROR: Nothing to delete from selection.

misc_reviewed/select/select_nothing_to_del_fail.ys

+read_verilog ../top.v
+proc
+ select -del
+ select -list

misc_reviewed/select/select_one_elem_for__C_fail.pat

+ERROR: Must have at least one element on the stack for operator %C.

misc_reviewed/select/select_one_elem_for__C_fail.ys

+read_verilog ../top.v
+proc
+ select %C
+ select -list

misc_reviewed/select/select_one_elem_for__D_fail.pat

+Must have at least two elements on the stack for operator %D.

misc_reviewed/select/select_one_elem_for__D_fail.ys

+read_verilog ../top.v
+proc
+ select %D
+ select -list

misc_reviewed/select/select_one_elem_for__M_fail.pat

+ERROR: Must have at least one element on the stack for operator %M.

misc_reviewed/select/select_one_elem_for__M_fail.ys

+read_verilog ../top.v
+proc
+ select %M
+ select -list

misc_reviewed/select/select_one_elem_for__R_fail.pat

+ERROR: Must have at least one element on the stack for operator %R.

misc_reviewed/select/select_one_elem_for__R_fail.ys

+read_verilog ../top.v
+proc
+ select %R
+ select -list

misc_reviewed/select/select_one_elem_for__a_fail.pat

+ERROR: Must have at least one element on the stack for operator %a.

misc_reviewed/select/select_one_elem_for__a_fail.ys

+read_verilog ../top.v
+proc
+ select %a
+ select -list

misc_reviewed/select/select_one_elem_for__c_fail.pat

+ERROR: Must have at least one element on the stack for operator %c.

misc_reviewed/select/select_one_elem_for__c_fail.ys

+read_verilog ../top.v
+proc
+ select %c
+ select -list

misc_reviewed/select/select_one_elem_for__ci_fail.pat

+ERROR: Must have at least one element on the stack for operator %ci.

misc_reviewed/select/select_one_elem_for__ci_fail.ys

+read_verilog ../top.v
+proc
+ select %ci
+ select -list

misc_reviewed/select/select_one_elem_for__cie_fail.pat

+ERROR: Must have at least one element on the stack for operator %cie.

misc_reviewed/select/select_one_elem_for__cie_fail.ys

+read_verilog ../top.v
+proc
+ select %cie
+ select -list

misc_reviewed/select/select_one_elem_for__co_fail.pat

+ERROR: Must have at least one element on the stack for operator %co.

misc_reviewed/select/select_one_elem_for__co_fail.ys

+read_verilog ../top.v
+proc
+ select %co
+ select -list

misc_reviewed/select/select_one_elem_for__coe_fail.pat

+ERROR: Must have at least one element on the stack for operator %coe.

misc_reviewed/select/select_one_elem_for__coe_fail.ys

+read_verilog ../top.v
+proc
+ select %coe
+ select -list

misc_reviewed/select/select_one_elem_for__d_fail.pat

+ERROR: Must have at least two elements on the stack for operator %d.

misc_reviewed/select/select_one_elem_for__d_fail.ys

+read_verilog ../top.v
+proc
+ select %d
+ select -list

misc_reviewed/select/select_one_elem_for__i_fail.pat

+ERROR: Must have at least two elements on the stack for operator %i.

misc_reviewed/select/select_one_elem_for__i_fail.ys

+read_verilog ../top.v
+proc
+ select %i
+ select -list

misc_reviewed/select/select_one_elem_for__m_fail.pat

+ERROR: Must have at least one element on the stack for operator %m.

misc_reviewed/select/select_one_elem_for__m_fail.ys

+read_verilog ../top.v
+proc
+ select %m
+ select -list

misc_reviewed/select/select_one_elem_for__n_fail.pat

+ERROR: Must have at least one element on the stack for operator %n.

misc_reviewed/select/select_one_elem_for__n_fail.ys

+read_verilog ../top.v
+proc
+ select %n
+ select -list

misc_reviewed/select/select_one_elem_for__s_fail.pat

+ERROR: Must have at least one element on the stack for operator %s.

misc_reviewed/select/select_one_elem_for__s_fail.ys

+read_verilog ../top.v
+proc
+ select %s
+ select -list

misc_reviewed/select/select_one_elem_for__u_fail.pat

+ERROR: Must have at least two elements on the stack for operator %u.

misc_reviewed/select/select_one_elem_for__u_fail.ys

+read_verilog ../top.v
+proc
+ select %u
+ select -list

misc_reviewed/select/select_one_elem_for__x_fail.pat

+ERROR: Must have at least one element on the stack for operator %x.

misc_reviewed/select/select_one_elem_for__x_fail.ys

+read_verilog ../top.v
+proc
+ select %x */t %d
+ select -list

misc_reviewed/select/select_one_elem_for__xe_fail.pat

+ERROR: Must have at least one element on the stack for operator %xe.

misc_reviewed/select/select_one_elem_for__xe_fail.ys

+read_verilog ../top.v
+proc
+ select %xe
+ select -list

misc_reviewed/select/select_read.pat

+middle
+middle/$add
+middle/o
+middle/y
+middle/x
+middle/$add

misc_reviewed/select/select_read.ys

+read_verilog ../top.v
+proc
+select -del *
+select -add middle
+select -write select_f
+ select -read select_f
+tee -o result.out select -list

misc_reviewed/select/select_read_with_selection_expr_fail.pat

+ERROR: Option -read can not be combined with a selection expression.

misc_reviewed/select/select_read_with_selection_expr_fail.ys

+read_verilog ../top.v
+proc
+ select -read -add x:o
+ select -list

misc_reviewed/select/select_selection_isnt_defined_fail.pat

+ERROR: Selection @ is not defined!

misc_reviewed/select/select_selection_isnt_defined_fail.ys

+read_verilog ../top.v
+proc
+ select @
+ select -list

misc_reviewed/select/select_set.pat

+top
+top/$ternary
+top/$0\\A\[0:0\]
+top/o
+top/cout
+top/A
+top/cin
+top/y
+top/x
+top/$procdff
+top/u_mid
+top/$ternary

misc_reviewed/select/select_set.ys

+read_verilog ../top.v
+proc
+select -add top
+ select -set top top
+ select @top
+tee -o result.out select -list

misc_reviewed/select/select_set_with_assert_any_fail.pat

+ERROR: Option -set can not be combined with -list, -write, -count, -add, -del, -assert-none, -assert-any, -assert-count, -assert-max, or -assert-min.

misc_reviewed/select/select_set_with_assert_any_fail.ys

+read_verilog ../top.v
+proc
+ select -set aa -assert-any top
+ select -list

misc_reviewed/select/select_set_with_assert_max_fail.pat

+ERROR: Option -set can not be combined with -list, -write, -count, -add, -del, -assert-none, -assert-any, -assert-count, -assert-max, or -assert-min.

misc_reviewed/select/select_set_with_assert_max_fail.ys

+read_verilog ../top.v
+proc
+ select -set a -assert-max 2 top
+ select -list

misc_reviewed/select/select_set_with_count_fail.pat

+ERROR: Option -set can not be combined with -list, -write, -count, -add, -del, -assert-none, -assert-any, -assert-count, -assert-max, or -assert-min.

misc_reviewed/select/select_set_with_count_fail.ys

+read_verilog ../top.v
+proc
+ select -set a -assert-count 3 top
+ select -list

misc_reviewed/select/select_set_with_del_fail.pat

+ERROR: Option -set can not be combined with -list, -write, -count, -add, -del, -assert-none, -assert-any, -assert-count, -assert-max, or -assert-min.

misc_reviewed/select/select_set_with_del_fail.ys

+read_verilog ../top.v
+proc
+ select -set a -del a
+ select -list

misc_reviewed/select/select_set_with_list_fail.pat

+ERROR: Option -set can not be combined with -list, -write, -count, -add, -del, -assert-none, -assert-any, -assert-count, -assert-max, or -assert-min.

misc_reviewed/select/select_set_with_list_fail.ys

+read_verilog ../top.v
+proc
+ select -set a -list
+ select -list

misc_reviewed/select/select_unknown_opt_fail.pat

+ERROR: Unknown option -x.

misc_reviewed/select/select_unknown_opt_fail.ys

+read_verilog ../top.v
+proc
+ select -x
+ select -list

misc_reviewed/select/select_unknown_selection_fail.pat

+ERROR: Unknown selection operator '%xmux'.

misc_reviewed/select/select_unknown_selection_fail.ys

+read_verilog ../top.v
+proc
+ select */t:$mux %xmux */t:$mux %d
+ select -list

misc_reviewed/select/select_write.ys

+read_verilog ../top.v
+proc
+select -add top -add middle
+ select -write select_f

misc_reviewed/select/select_write_with_assert_count_fail.pat

+ERROR: Options -list, -write and -count can not be combined with -add, -del, -assert-none, -assert-any, assert-count, -assert-max, or -assert-min.

misc_reviewed/select/select_write_with_assert_count_fail.ys

+read_verilog ../top.v
+proc
+ select -write out.txt -assert-count 4 top
+ select -list

misc_reviewed/select/select_write_with_del_fail.pat

+ERROR: Options -list, -write and -count can not be combined with -add, -del, -assert-none, -assert-any, assert-count, -assert-max, or -assert-min.

misc_reviewed/select/select_write_with_del_fail.ys

+read_verilog ../top.v
+proc
+ select -write out.txt -del
+ select -list

misc_reviewed/select/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output cout
+ );
+ wire o;
+
+always @(posedge cin)
+	A <= o;
+
+assign cout =  cin? y : x;
+
+middle u_mid (x,y,o);
+
+endmodule
+
+module middle
+(
+	input x,
+	input y,
+	output o
+);
+
+assign o = x + y;
+endmodule

misc_reviewed/select/top_mem.v

+module top
+(
+	input [7:0] data_a, data_b,
+	input [5:0] addr_a, addr_b,
+	input we_a, we_b, clk,
+	output reg [7:0] q_a, q_b
+);
+	// Declare the RAM variable
+	reg [7:0] ram[63:0];
+
+	// Port A
+	always @ (posedge clk)
+	begin
+		if (we_a)
+		begin
+			ram[addr_a] <= data_a;
+			q_a <= data_a;
+		end
+		else
+		begin
+			q_a <= ram[addr_a];
+		end
+	end
+
+	// Port B
+	always @ (posedge clk)
+	begin
+		if (we_b)
+		begin
+			ram[addr_b] <= data_b;
+			q_b <= data_b;
+		end
+		else
+		begin
+			q_b <= ram[addr_b];
+		end
+	end
+
+endmodule

misc_reviewed/select/top_mux.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+ output cout
+ );
+
+assign cout =  cin? y : x;
+
+endmodule