Update backends group.

- write_aiger;
- write_blif;
- write_btor;
- write_edif;
- write_firrtl;
- write_ilang.

backends_reviewed/.gitignore

+*/work_*/
+/.stamp
+/run-test.mk

backends_reviewed/Makefile

+PYTHON_EXECUTABLE := $(shell if python3 -c ""; then echo "python3"; else echo "python"; fi)
+
+all:: run-test.mk
+	@touch .stamp
+	@$(MAKE) -f run-test.mk 
+clean:: run-test.mk
+	@rm -f .stamp
+	@$(MAKE) -f run-test.mk clean
+
+run-test.mk: ../generate.py
+	@$(PYTHON_EXECUTABLE) ../generate.py > run-test.mk
+
+.PHONY: all clean

backends_reviewed/write_aiger/top3.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout
+ );
+
+ initial begin
+    A = 0;
+    cout = 0;
+ end
+
+
+always @(posedge x) begin
+    A <=  y + cin;
+end
+always @(negedge x) begin
+    cout <=  y + A;
+end
+
+endmodule

backends_reviewed/write_aiger/top_diff_cells.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
+
+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

backends_reviewed/write_aiger/top_two_mods.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
+
+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
+
+module top2
+(
+ 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

backends_reviewed/write_aiger/top_x_z.v

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

backends_reviewed/write_aiger/write_aiger.pat

+aig 5 5 0 2 0
+2
+10
+c

backends_reviewed/write_aiger/write_aiger.ys

+read_verilog -sv ../top3.v
+aigmap
+write_aiger result.out
+design -reset
+read_aiger result.out

backends_reviewed/write_aiger/write_aiger_B.pat

+aig 5 5 0 2 0 1 0 0 0
+2
+10
+0
+c

backends_reviewed/write_aiger/write_aiger_B.ys

+read_verilog -sv ../top3.v
+aigmap
+write_aiger -B result.out
+design -reset
+read_aiger result.out

backends_reviewed/write_aiger/write_aiger_I.ys

+read_verilog -sv ../top3.v
+aigmap
+write_aiger -I aiger.aiger
+design -reset
+read_aiger aiger.aiger

backends_reviewed/write_aiger/write_aiger_O.ys

+read_verilog -sv ../top3.v
+aigmap
+write_aiger -O aiger.aiger
+design -reset
+read_aiger aiger.aiger

backends_reviewed/write_aiger/write_aiger_ascii.pat

+aag 5 5 0 2 0
+2
+4
+6
+8
+10
+2
+10
+c

backends_reviewed/write_aiger/write_aiger_ascii.ys

+read_verilog -sv ../top3.v
+aigmap
+write_aiger -ascii result.out
+design -reset
+read_aiger result.out

backends_reviewed/write_aiger/write_aiger_ascii_diff_cells.ys

+read_verilog -sv ../top_diff_cells.v
+aigmap
+write_aiger -ascii aiger.aiger

backends_reviewed/write_aiger/write_aiger_cant_find_top_module_fail.pat

+ERROR: Can't find top module in current design!

backends_reviewed/write_aiger/write_aiger_cant_find_top_module_fail.ys

+read_verilog -sv ../top_two_mods.v
+aigmap
+write_aiger aiger.aiger

backends_reviewed/write_aiger/write_aiger_cant_open_file_fail.pat

+ERROR: Can't open file

backends_reviewed/write_aiger/write_aiger_cant_open_file_fail.ys

+read_verilog -sv ../top_x_z.v
+aigmap
+write_aiger -map tt/tt.map aiger.aiger

backends_reviewed/write_aiger/write_aiger_diff_cells.ys

+read_verilog -sv ../top_diff_cells.v
+aigmap
+write_aiger aiger.aiger

backends_reviewed/write_aiger/write_aiger_diff_cells_proc.ys

+read_verilog -sv ../top_diff_cells.v
+synth
+aigmap
+write_aiger aiger.aiger

backends_reviewed/write_aiger/write_aiger_map.ys

+read_verilog -sv ../top3.v
+aigmap
+write_aiger -map a.map aiger.aiger
+design -reset
+read_aiger aiger.aiger

backends_reviewed/write_aiger/write_aiger_miter.pat

+aig 11 3 2 0 6 2
+16
+22
+8
+10

backends_reviewed/write_aiger/write_aiger_miter.ys

+read_verilog -sv ../top3.v
+synth -top top
+aigmap
+write_aiger -miter result.out
+design -reset
+read_aiger result.out

backends_reviewed/write_aiger/write_aiger_miter_and_asserts_fail.pat

+ERROR: Running AIGER back-end in -miter mode, but design contains \$assert, \$assume, \$live and/or \$fair cells!

backends_reviewed/write_aiger/write_aiger_miter_and_asserts_fail.ys

+read_verilog -sv ../top_x_z.v
+aigmap
+write_aiger -miter aiger.aiger

backends_reviewed/write_aiger/write_aiger_symbols.pat

+i1 x
+i2 y
+i3 cin
+o0 A
+o1 cout

backends_reviewed/write_aiger/write_aiger_symbols.ys

+read_verilog -sv ../top3.v
+aigmap
+write_aiger -symbols result.out
+design -reset
+read_aiger result.out

backends_reviewed/write_aiger/write_aiger_symbols_diff_cells.ys

+read_verilog -sv ../top_diff_cells.v
+aigmap
+write_aiger -symbols aiger.aiger

backends_reviewed/write_aiger/write_aiger_unsupported_cell_type_fail.pat

+ERROR: Unsupported cell type:

backends_reviewed/write_aiger/write_aiger_unsupported_cell_type_fail.ys

+read_verilog -sv ../top_x_z.v
+synth
+write_aiger aiger.aiger

backends_reviewed/write_aiger/write_aiger_vmap.ys

+read_verilog -sv ../top3.v
+aigmap
+write_aiger -vmap a.map aiger.aiger
+design -reset
+read_aiger aiger.aiger

backends_reviewed/write_aiger/write_aiger_zinit.ys

+read_verilog -sv ../top3.v
+aigmap
+write_aiger -zinit aiger.aiger
+design -reset
+read_aiger aiger.aiger

backends_reviewed/write_blif/top.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout
+ );
+
+ reg A1,cout1;
+
+ initial begin
+    A = 0;
+    cout = 0;
+ end
+
+always @(posedge x) begin
+    A1 <=  ~y + &cin;
+end
+always @(negedge x) begin
+    cout1 <= cin ? |y : ^A;
+end
+
+always @(*) begin
+    if (x)
+        A <=  A1|y~&cin;
+end
+always @(*) begin
+    if (~x)
+        cout <=  cout1&cin~|y;
+end
+
+bb ubb (cin,y,x,A);
+
+endmodule
+
+(* black_box *) module bb(in1, in2, clk, out1);
+ input in1;
+ input in2;
+ input clk;
+
+ output reg out1;
+
+ always @(posedge clk)
+	out1 <= in1 & in2;
+endmodule

backends_reviewed/write_blif/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, clk,
+	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 clk)
+	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 clk)
+	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

backends_reviewed/write_blif/top_mux.v

+module mux16 (D, S, Y);
+ 	input  [15:0] D;
+ 	input  [3:0] S;
+ 	output Y;
+
+ 	assign Y = D[S];
+
+endmodule
+
+
+module top (
+input [3:0] S,
+input [15:0] D,
+output M16
+);
+
+mux16 u_mux16 (
+        .S (S[3:0]),
+        .D (D[15:0]),
+        .Y (M16)
+    );
+
+endmodule

backends_reviewed/write_blif/write_blif.ys

+read_verilog -sv ../top.v
+proc
+write_blif blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_abc_and_nor.ys

+read_verilog -sv ../top.v
+synth
+abc -g AND,XOR,NOR
+write_blif blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_abc_lut.ys

+read_verilog -sv ../top.v
+synth
+abc -lut 2
+write_blif blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_abc_sop.ys

+read_verilog -sv ../top.v
+synth
+abc -sop
+write_blif blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_andnot.ys

+read_verilog -sv ../top.v
+synth
+abc -g ANDNOT,ORNOT
+write_blif blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_aoi4.ys

+read_verilog -sv ../top.v
+abc -g AOI4
+synth -top top
+write_blif blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_attr.ys

+read_verilog -sv ../top.v
+synth -top top
+write_blif -attr blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_blackbox.ys

+read_verilog -sv ../top.v
+synth -top top
+write_blif -blackbox blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_buf.ys

+read_verilog -sv ../top.v
+synth -top top
+write_blif -buf a a a blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_cant_find_top_module_fail.pat

+ERROR: Can't find top module

backends_reviewed/write_blif/write_blif_cant_find_top_module_fail.ys

+read_verilog -sv ../top.v
+proc
+write_blif -top u blif1.blif

backends_reviewed/write_blif/write_blif_cmos3.ys

+read_verilog -sv ../top.v
+synth
+abc -g cmos3
+write_blif blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_cmos4.ys

+read_verilog -sv ../top_mux.v
+synth -top top
+abc -g cmos4
+write_blif blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_cname.ys

+read_verilog -sv ../top.v
+synth -top top
+write_blif -cname blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_conn.ys

+read_verilog -sv ../top.v
+synth -top top
+write_blif -conn blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_false.ys

+read_verilog -sv ../top.v
+synth -top top
+write_blif -false a a blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_gates.ys

+read_verilog -sv ../top.v
+synth -top top
+write_blif -gates blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_iattr.ys

+read_verilog -sv ../top.v
+synth -top top
+write_blif -iattr blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_icells.ys

+read_verilog -sv ../top.v
+synth -top top
+write_blif -icells blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_impltf.ys

+read_verilog -sv ../top.v
+synth -top top
+write_blif -impltf blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_iname.ys

+read_verilog -sv ../top.v
+synth -top top
+write_blif -iname blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_noalias.ys

+read_verilog -sv ../top.v
+synth -top top
+write_blif -noalias blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_opt.ys

+read_verilog -sv ../top.v
+proc
+opt
+write_blif blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_param.ys

+read_verilog -sv ../top.v
+synth -top top
+write_blif -param blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_synth_top.ys

+read_verilog -sv ../top.v
+synth -top top
+write_blif blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_top.ys

+read_verilog -sv ../top.v
+synth -top top
+write_blif -top top blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_true.ys

+read_verilog -sv ../top.v
+synth -top top
+write_blif -true a a blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_unbuf.ys

+read_verilog -sv ../top.v
+synth -top top
+write_blif -unbuf a a a blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_undef.ys

+read_verilog -sv ../top.v
+synth -top top
+write_blif -undef a a blif.blif
+design -reset
+read_blif blif.blif

backends_reviewed/write_blif/write_blif_unmapped_mem_fail.pat

+ERROR: Found unmapped memories in module

backends_reviewed/write_blif/write_blif_unmapped_mem_fail.ys

+read_verilog -sv ../top_mem.v
+proc
+write_blif -top u blif1.blif

backends_reviewed/write_blif/write_blif_unmapped_proc_fail.pat

+ERROR: Found unmapped processes in module

backends_reviewed/write_blif/write_blif_unmapped_proc_fail.ys

+read_verilog -sv ../top.v
+write_blif blif1.blif

backends_reviewed/write_btor/top.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
+
+always @(posedge x) begin
+    if ($initstate)
+        A <= 0;
+    A <=  y + cin + too;
+    assume(too);
+    assume(s_eventually too);
+end
+always @(posedge x) begin
+    if ($initstate)
+        cout <= 0;
+        cout <=  y + A + foo;
+    assert(ASSERT);
+    assert(s_eventually ASSERT);
+end
+
+endmodule

backends_reviewed/write_btor/top_and_or.v

+module top
+(
+ input [1:0] x,
+ input [1:0] y,
+ input [1:0] z,
+ input clk,
+
+ input A,
+ output reg B
+ );
+
+ initial begin
+    B = 0;
+ end
+
+always @(posedge clk) begin
+    if (x || y && z)
+        B <=  A & z;
+    if (x || y && !z)
+        B <=  A | x;
+end
+
+endmodule

backends_reviewed/write_btor/top_div_mod.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout,
+ output reg B,C
+ );
+
+ reg ASSERT = 1;
+ (* anyconst *) reg foo;
+ (* anyseq *) reg too;
+
+
+
+
+ initial begin
+    begin
+        A = 0;
+        cout = 0;
+    end
+ end
+
+always @(posedge x) begin
+    A <=  y / too;
+end
+always @(posedge x) begin
+        cout <=  y + A % foo;
+end
+assign {B,C} =  {cout,A} << 1;
+
+endmodule

backends_reviewed/write_btor/top_fsm.v

+module top (
+input clk,
+input rst,
+input en,
+input a,
+input b,
+output s,
+output bs,
+output f
+);
+
+
+    parameter S0 = 4'b0000, S1 = 4'b0001, S2 = 4'b0010, S3 = 4'b0011, S4 = 4'b0100, S5 = 4'b0101, S6 = 4'b0110, S7 = 4'b0111, S8 = 4'b1000, S9 = 4'b1001, S10 = 4'b1010, S11 = 4'b1011, S12 = 4'b1100, S13 = 4'b1101, S14 = 4'b1110;
+
+	reg [3:0] ns, st;
+
+	reg [2:0] count;
+
+
+	always @(posedge clk)
+	begin : CurrstProc
+		if (rst)
+			st <= S0;
+		else
+			st <= ns;
+	end
+
+	always @*
+	begin : NextstProc
+		ns = st;
+		case (st)
+			S0: ns = S1;
+			S1: ns = S2;
+			S2:
+				if (b == 1'b1)
+					ns = S3;
+				else
+					ns = S4;
+			S3: ns = S1;
+			S4: if (count > 7)
+					ns = S10;
+				else
+					ns = S5;
+			S5: if (a == 1'b0)
+					ns = S6;
+				else
+					ns = S3;
+			S6:
+				if (a == 1'b1)
+					ns = S7;
+				else
+					ns = S8;
+			S7:
+				if (a == 1'b1 && b == 1'b1)
+					ns = S5;
+				else
+					ns = S13;
+			S8: ns = S9;
+			S9: ns = S8;
+			S10:
+				if (a == 1'b1 || b == 1'b1)
+					ns = S11;
+				else
+					ns = S4;
+			S11: ns = S12;
+			S12: ns = S10;
+			S13: ;
+			default: ns = S0;
+		endcase;
+	end
+
+	always @(posedge clk)
+		if(~rst)
+			count <= 0;
+		else
+		begin
+			if(st == S4)
+				if (count > 7)
+					count <= 0;
+				else
+					count <= count + 1;
+		end
+
+	//FSM outputs (combinatorial)
+
+	assign s   = (st == S3 || st == S12) ? 1'b1 : 1'b0;
+
+	assign f = (st == S13) ? 1'b1 : 1'b0;
+
+	assign bs   = (st == S8 || st == S9) ? 1'b1 : 1'b0;
+
+endmodule

backends_reviewed/write_btor/top_init_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
+
+always @(posedge x) begin
+    if ($initstate)
+        A <= 0;
+    A <=  y + cin + too;
+    assume(too);
+    assume(s_eventually too);
+end
+always @(posedge x) begin
+    if ($initstate)
+        cout <= 0;
+        cout <=  y + A + foo;
+    assert(ASSERT);
+    assert(s_eventually ASSERT);
+end
+
+endmodule

backends_reviewed/write_btor/top_logic.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout
+ );
+
+ reg A1,cout1;
+
+ initial begin
+    A = 0;
+    cout = 0;
+ end
+
+
+always @(posedge x) begin
+    A1 <=  ~y + &cin;
+end
+always @(posedge x) begin
+    cout1 <= cin ? |y : ~^A;
+end
+
+always @(posedge x) begin
+        A <=  A1|y~&cin~^A1;
+end
+always @(posedge x) begin
+        cout <=  cout1&cin~|y;
+end
+
+endmodule

backends_reviewed/write_btor/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, clk,
+	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 clk)
+	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 clk)
+	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

backends_reviewed/write_btor/top_no_top_mod.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
+
+always @(posedge x) begin
+    if ($initstate)
+        A <= 0;
+    A <=  y + cin + too;
+end
+
+endmodule
+
+module top2
+(
+ 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;
+
+end
+always @(posedge x) begin
+    if ($initstate)
+        cout <= 0;
+        cout <=  y + A + foo;
+
+end
+
+endmodule
+

backends_reviewed/write_btor/top_pmux.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

backends_reviewed/write_btor/top_shift.v

+module top
+(
+ input x,
+ input y,
+ input cin,
+
+ output reg A,
+ output reg cout,
+ output reg B,C
+ );
+
+ reg ASSERT = 1;
+ (* anyconst *) reg foo;
+ (* anyseq *) reg too;
+
+
+
+
+ initial begin
+    begin
+        A = 0;
+        cout = 0;
+    end
+ end
+
+always @(posedge x) begin
+    A <=  y >> too;
+end
+always @(posedge x) begin
+        cout <=  y + A >>> foo;
+end
+assign {B,C} =  {cout,A} << 1;
+
+endmodule

backends_reviewed/write_btor/top_shift_shiftx.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

backends_reviewed/write_btor/top_shiftx.v

+
+// VERIFIC-SKIP
+
+module top(a, y);
+
+input signed [4:0] a;
+output signed y;
+
+integer i = 0, j = 0;
+reg [31:0] lut;
+
+initial begin
+	for (i = 0; i < 32; i = i+1) begin
+		lut[i] = i > 1;
+		for (j = 2; j*j <= i; j = j+1)
+			if (i % j == 0)
+				lut[i] = 0;
+	end
+end
+
+assign y = lut[a];
+
+endmodule

backends_reviewed/write_btor/top_unsupp_cell.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
+
+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

backends_reviewed/write_btor/write_btor.ys

+read_verilog -sv ../top.v
+hierarchy -top top
+proc
+write_btor btor.btor

backends_reviewed/write_btor/write_btor_abc.ys

+read_verilog -sv ../top.v
+synth
+abc
+write_btor btor.btor

backends_reviewed/write_btor/write_btor_abc_and_nor.ys

+read_verilog -sv ../top.v
+synth -top top
+abc -g AND,XOR,NOR
+write_btor btor.btor

backends_reviewed/write_btor/write_btor_and_or.ys

+read_verilog -sv ../top_and_or.v
+proc
+write_btor btor.btor
+design -reset
+read_verilog  -sv ../top_and_or.v
+synth -top top
+write_verilog synth.v

backends_reviewed/write_btor/write_btor_andnot.ys

+read_verilog -sv ../top.v
+synth -top top
+abc -g ANDNOT,ORNOT
+write_btor btor.btor

backends_reviewed/write_btor/write_btor_aoi4.ys

+read_verilog -sv ../top.v
+abc -g cmos4
+synth -top top
+write_btor btor.btor

backends_reviewed/write_btor/write_btor_cmos3.ys

+read_verilog -sv ../top.v
+synth -top top
+abc -g cmos3
+write_btor btor6.btor

backends_reviewed/write_btor/write_btor_div_mod.ys

+read_verilog -sv ../top_div_mod.v
+hierarchy -top top
+proc
+write_btor btor.btor

backends_reviewed/write_btor/write_btor_fsm.ys

+read_verilog -sv ../top_fsm.v
+proc
+pmux2shiftx
+hierarchy -top top
+flatten
+write_btor btor.btor
+write_verilog synth.v

backends_reviewed/write_btor/write_btor_init_assert.ys

+read_verilog -sv ../top_init_assert.v
+hierarchy -top top
+proc
+write_btor btor.btor

backends_reviewed/write_btor/write_btor_logic.ys

+read_verilog -sv ../top_logic.v
+hierarchy -top top
+proc
+write_btor btor.btor

backends_reviewed/write_btor/write_btor_mem.ys

+read_verilog -sv ../top_mem.v
+memory
+proc
+write_btor btor.btor

backends_reviewed/write_btor/write_btor_mem_s.ys

+read_verilog -sv ../top_mem.v
+memory
+proc
+write_btor -s btor.btor

backends_reviewed/write_btor/write_btor_mem_v.ys

+read_verilog -sv ../top_mem.v
+memory
+proc
+write_btor -v btor.btor

backends_reviewed/write_btor/write_btor_no_top_module_fail.pat

+ERROR: No top module found.

backends_reviewed/write_btor/write_btor_no_top_module_fail.ys

+read_verilog -sv ../top_no_top_mod.v
+proc
+write_btor btor.btor

backends_reviewed/write_btor/write_btor_oai3.ys

+read_verilog -sv ../top_fsm.v
+synth -top top
+abc -g cmos3
+write_btor btor6.btor

backends_reviewed/write_btor/write_btor_oai4.ys

+read_verilog -sv ../top_fsm.v
+abc -g OAI4
+synth -top top
+write_btor btor.btor