Improve SVA tests, add Makefile and scripts

11 files changed, 110 insertions, 9 deletions

diff --git a/tests/sva/.gitignore b/tests/sva/.gitignore
new file mode 100644
index 000000000..254013047
--- /dev/null
+++ b/tests/sva/.gitignore
@@ -0,0 +1,5 @@
+/*_pass.sby
+/*_fail.sby
+/*_pass
+/*_fail
+/*.ok
diff --git a/tests/sva/Makefile b/tests/sva/Makefile
new file mode 100644
index 000000000..c2ee5e9d8
--- /dev/null
+++ b/tests/sva/Makefile
@@ -0,0 +1,13 @@
+
+TESTS = $(basename $(wildcard *.sv))
+
+all: $(addsuffix .ok,$(TESTS))
+
+%.ok: %.sv
+	bash runtest.sh $<
+
+clean:
+	rm -rf $(addsuffix .ok,$(TESTS))
+	rm -rf $(addsuffix _pass.sby,$(TESTS)) $(addsuffix _pass,$(TESTS))
+	rm -rf $(addsuffix _fail.sby,$(TESTS)) $(addsuffix _fail,$(TESTS))
+
diff --git a/tests/sva/basic00.sv b/tests/sva/basic00.sv
index 387f3deef..30c37f5f1 100644
--- a/tests/sva/basic00.sv
+++ b/tests/sva/basic00.sv
@@ -2,6 +2,11 @@ module top (input clk, reset, antecedent, output reg consequent);
 	always @(posedge clk)
 		consequent <= reset ? 0 : antecedent;
 
+`ifdef FAIL
 	test_assert: assert property ( @(posedge clk) disable iff (reset) antecedent |-> consequent )
 			else $error("Failed with consequent = ", $sampled(consequent));
+`else
+	test_assert: assert property ( @(posedge clk) disable iff (reset) antecedent |=> consequent )
+			else $error("Failed with consequent = ", $sampled(consequent));
+`endif
 endmodule
diff --git a/tests/sva/basic01.sv b/tests/sva/basic01.sv
index 596e48db0..74ab93430 100644
--- a/tests/sva/basic01.sv
+++ b/tests/sva/basic01.sv
@@ -8,5 +8,9 @@ module top (input logic clock, ctrl);
 	end
 	
 	a_rw: assert property ( @(posedge clock) !(read && write) );
+`ifdef FAIL
 	a_wr: assert property ( @(posedge clock) write |-> ready );
+`else
+	a_wr: assert property ( @(posedge clock) write |=> ready );
+`endif
 endmodule
diff --git a/tests/sva/basic02.sv b/tests/sva/basic02.sv
index cf2d72ae7..b34f3aff3 100644
--- a/tests/sva/basic02.sv
+++ b/tests/sva/basic02.sv
@@ -10,7 +10,11 @@ endmodule
 
 module top_properties (input logic clock, read, write, ready);
 	a_rw: assert property ( @(posedge clock) !(read && write) );
+`ifdef FAIL
 	a_wr: assert property ( @(posedge clock) write |-> ready );
+`else
+	a_wr: assert property ( @(posedge clock) write |=> ready );
+`endif
 endmodule
 
 bind top top_properties properties_inst (.*);
diff --git a/tests/sva/basic03.sv b/tests/sva/basic03.sv
index a15f3f3a4..8018de4ca 100644
--- a/tests/sva/basic03.sv
+++ b/tests/sva/basic03.sv
@@ -4,7 +4,9 @@ module top (input logic clk, input logic selA, selB, QA, QB, output logic Q);
 		if (selB) Q <= QB;
 	end
 
-	check_selA: assert property ( @(posedge clk) selA|=> Q == $past(QA) );
-	check_selB: assert property ( @(posedge clk) selB|=> Q == $past(QB) );
-	assume_not_11: assume property ( @(posedge clk) !(selA& selB) );
+	check_selA: assert property ( @(posedge clk) selA |=> Q == $past(QA) );
+	check_selB: assert property ( @(posedge clk) selB |=> Q == $past(QB) );
+`ifndef FAIL
+	assume_not_11: assume property ( @(posedge clk) !(selA & selB) );
+`endif
 endmodule
diff --git a/tests/sva/basic04.sv b/tests/sva/basic04.sv
index 6f02f3c19..bc46be9f6 100644
--- a/tests/sva/basic04.sv
+++ b/tests/sva/basic04.sv
@@ -1,6 +1,10 @@
 module top_properties (input logic clock, read, write, ready);
 	a_rw: assert property ( @(posedge clock) !(read && write) );
+`ifdef FAIL
 	a_wr: assert property ( @(posedge clock) write |-> ready );
+`else
+	a_wr: assert property ( @(posedge clock) write |=> ready );
+`endif
 endmodule
 
 bind top top_properties properties_inst (.*);
diff --git a/tests/sva/basic04.vhd b/tests/sva/basic04.vhd
index 889bef0d2..f2ec305ec 100644
--- a/tests/sva/basic04.vhd
+++ b/tests/sva/basic04.vhd
@@ -10,9 +10,9 @@ entity top is
 end entity;
 
 architecture rtl of top is
-	signal read : std_logic;
-	signal write : std_logic;
-	signal ready : std_logic;
+	signal read : std_logic := '0';
+	signal write : std_logic := '0';
+	signal ready : std_logic := '0';
 begin
 	process (clock) begin
 		if (rising_edge(clock)) then
diff --git a/tests/sva/basic05.sv b/tests/sva/basic05.sv
index 03854aaac..816ee1da7 100644
--- a/tests/sva/basic05.sv
+++ b/tests/sva/basic05.sv
@@ -11,5 +11,9 @@ module top (input logic clock, ctrl);
 	assign ready = uut.ready;
 
 	a_rw: assert property ( @(posedge clock) !(read && write) );
+`ifdef FAIL
 	a_wr: assert property ( @(posedge clock) write |-> ready );
+`else
+	a_wr: assert property ( @(posedge clock) write |=> ready );
+`endif
 endmodule
diff --git a/tests/sva/basic05.vhd b/tests/sva/basic05.vhd
index 930f1ba22..8d42f71e8 100644
--- a/tests/sva/basic05.vhd
+++ b/tests/sva/basic05.vhd
@@ -10,9 +10,9 @@ entity demo is
 end entity;
 
 architecture rtl of demo is
-	signal read : std_logic;
-	signal write : std_logic;
-	signal ready : std_logic;
+	signal read : std_logic := '0';
+	signal write : std_logic := '0';
+	signal ready : std_logic := '0';
 begin
 	process (clock) begin
 		if (rising_edge(clock)) then
diff --git a/tests/sva/runtest.sh b/tests/sva/runtest.sh
new file mode 100644
index 000000000..004a172ba
--- /dev/null
+++ b/tests/sva/runtest.sh
@@ -0,0 +1,60 @@
+#!/bin/bash
+
+set -ex
+
+prefix=${1%.sv}
+test -f $prefix.sv
+
+generate_sby() {
+	cat <<- EOT
+		[options]
+		mode bmc
+		depth 10
+		expect $1
+
+		[engines]
+		smtbmc yices
+
+		[script]
+	EOT
+
+	if [ "$1" = "fail" ]; then
+		echo "verific -sv ${prefix}_fail.sv"
+	else
+		echo "verific -sv $prefix.sv"
+	fi
+
+	if [ -f $prefix.vhd ]; then
+		echo "verific -vhdl2008 $prefix.vhd"
+	fi
+
+	cat <<- EOT
+		verific -import -extnets -all top
+		prep -top top
+
+		[files]
+		$prefix.sv
+	EOT
+
+	if [ -f $prefix.vhd ]; then
+		echo "$prefix.vhd"
+	fi
+
+	if [ "$1" = "fail" ]; then
+		cat <<- EOT
+
+			[file ${prefix}_fail.sv]
+			\`define FAIL
+			\`include "$prefix.sv"
+		EOT
+	fi
+}
+
+generate_sby pass > ${prefix}_pass.sby
+generate_sby fail > ${prefix}_fail.sby
+
+sby --yosys $PWD/../../yosys -f ${prefix}_pass.sby
+sby --yosys $PWD/../../yosys -f ${prefix}_fail.sby
+
+touch $prefix.ok
+