Merge pull request #87 from YosysHQ/qbfsat

Added qbfsat tests

misc/qbfsat/qbf_solution1.txt

+\h=00000010

misc/qbfsat/qbf_solution2.txt

+\h=10101010

misc/qbfsat/qbfsat_demo9.ys

+logger -expect log "Specializing \\demo9 with \\h = 8'b00000010." 1
+read_verilog -formal <<EOT
+module demo9;
+	(* maximize *) wire[7:0] h = $anyconst;
+	wire [7:0] i = $allconst;
+
+	wire [7:0] t0 = ((i << 8'b00000010) + 8'b00000011);
+	wire trigger = (t0 > h)	&& (h < 8'b00000100);
+
+	always @* begin
+		assume(trigger == 1'b1);
+		cover(1);
+	end
+endmodule
+EOT
+proc; techmap
+prep -top demo9 -nordff
+qbfsat -specialize

misc/qbfsat/qbfsat_sat.ys

+read_verilog -formal <<EOT
+module foo(i, trigger1, trigger2, trigger3);
+	wire [7:0] h = $anyconst;
+	input [7:0] i;
+	output trigger1;
+	output trigger2;
+	output trigger3;
+
+	wire [7:0] t0 = (h * i) + (h - 1);
+	assign trigger1 = (t0 < 2);
+	assign trigger2 = trigger1;
+	assign trigger3 = trigger2;
+endmodule
+EOT
+proc; techmap
+prep -top foo -nordff
+qbfsat -unsat -assume-outputs

misc/qbfsat/qbfsat_solnfile1.ys

+logger -expect log "Specializing \\demo9 from file with \\h = 8'b00000010." 1
+
+read_verilog -formal <<EOT
+module demo9(a, b, trigger);
+	input [3:0] a;
+	input [3:0] b;
+	wire [7:0] i = {a, b};
+	(* maximize *) wire [7:0] h;
+       	assign h = $anyconst;
+
+	wire [7:0] t0 = ((i << 8'b00000010) + 8'b00000011);
+	output trigger = (t0 > h) && (h < 8'b00000100);
+
+	always @* begin
+		assume(trigger == 1'b1);
+		cover(1);
+	end
+endmodule
+EOT
+proc; techmap
+prep -top demo9 -nordff
+qbfsat -specialize-from-file ../qbf_solution1.txt

misc/qbfsat/qbfsat_solnfile2.ys

+logger -expect log "Specializing \\demo9 from file with \\h = 8'b10101010." 1
+logger -expect log "Eval result: \\trigger = 1'0." 1
+
+read_verilog -formal <<EOT
+module demo9(a, b, trigger);
+	input [3:0] a;
+	input [3:0] b;
+	wire [7:0] i = {a, b};
+	(* maximize *) wire [7:0] h;
+       	assign h = $anyconst;
+
+	wire [7:0] t0 = ((i << 8'b00000010) + 8'b00000011);
+	output trigger = (t0 > h) && (h < 8'b00000100);
+
+	always @* begin
+		assume(trigger == 1'b1);
+		cover(1);
+	end
+endmodule
+EOT
+proc; techmap
+prep -top demo9 -nordff
+qbfsat -specialize-from-file ../qbf_solution2.txt
+opt
+eval

misc/qbfsat/qbfsat_solnfile3.ys

+logger -expect log "Specializing \\const_mul from file with \\h = 8'b00000010." 1
+logger -expect log "Eval result: \\out = 8'00001000." 1
+
+read_verilog -formal <<EOT
+module const_mul(out);
+	wire [7:0] h;
+	output [7:0] out;
+
+	assign out = h[7]? h[6:0] * 3 : h[6:0] * 4;
+endmodule
+EOT
+proc; techmap
+prep -top const_mul -nordff
+qbfsat -specialize-from-file ../qbf_solution1.txt
+opt
+eval

misc/qbfsat/qbfsat_writesoln.ys

+read_verilog -formal <<EOT
+module foo(i, trigger);
+	wire [7:0] h = $anyconst;
+	input [7:0] i;
+	output trigger;
+
+	wire [7:0] t0 = (h * i) + (h - 1);
+	wire [7:0] t1 = h[7]? t0 : t0 >> 7;
+	assign trigger = (t1 < 2);
+endmodule
+EOT
+proc; techmap
+prep -top foo -nordff
+qbfsat -assume-outputs -write-solution /tmp/qbf_solution.txt
+exec -expect-stdout \\h=[01]{8} -- cat /tmp/qbf_solution.txt