Improve SVA tests, add Makefile and scripts

tests/sva/.gitignore

@@ -0,0 +1,5 @@
+/*_pass.sby
+/*_fail.sby
+/*_pass
+/*_fail
+/*.ok

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))
+

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

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

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 (.*);

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

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 (.*);

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

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

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

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
+