Add verific/sva/ directory

Signed-off-by: Clifford Wolf <clifford@clifford.at>

verific/sva/.gitignore

+/*.status
+/*.pass_[0-9][0-9]/
+/*.fail_[0-9][0-9]/
+/*.pass_[0-9][0-9].sby
+/*.fail_[0-9][0-9].sby
+/.stamp

verific/sva/Makefile

+TESTS := until
+
+all: $(addsuffix .status,$(TESTS))
+	touch .stamp
+
+%.status: %.sv run.sh
+	-bash run.sh $(basename $@)
+	test -f $@
+
+clean:
+	rm -rf $(addsuffix .pass_??,$(TESTS))
+	rm -rf $(addsuffix .fail_??,$(TESTS))
+	rm -f $(addsuffix .pass_??.sby,$(TESTS))
+	rm -f $(addsuffix .fail_??.sby,$(TESTS))
+	rm -f $(addsuffix .status,$(TESTS))
+	rm -f .stamp
+
+.PHONY: all clean

verific/sva/run.sh

+#!/bin/bash
+
+set -ex
+test -f $1.sv
+trap "echo FAIL > $1.status" ERR
+
+while read t; do
+	{
+		echo "[options]"
+		echo "mode bmc"
+		echo "depth 32"
+		echo "expect $(echo $t | cut -f1 -d_)"
+		echo ""
+		echo "[engines]"
+		echo "smtbmc yices"
+		echo ""
+		echo "[script]"
+		echo "verific -sv $1.sv"
+		echo "verific -import -v $t"
+		echo "prep -nordff -top $t"
+		echo "chformal -assume -early"
+		echo "opt_clean"
+		echo ""
+		echo "[files]"
+		echo "$1.sv"
+	} > $1.$t.sby
+	sby -f $1.$t.sby
+done < <( egrep '^module (pass|fail)_[0-9][0-9]' $1.sv | gawk '{ print $2; }'; )
+
+echo PASS > $1.status

verific/sva/until.sv

+module sequencer #(
+	//                              01234567890123456789012345678901
+	parameter [32*8-1:0] trace_a = "________________________________",
+	parameter [32*8-1:0] trace_b = "________________________________",
+	parameter [32*8-1:0] trace_c = "________________________________",
+	parameter [32*8-1:0] trace_d = "________________________________"
+
+) (
+	input clock,
+	output A, B, C, D
+);
+	integer t = 0;
+	always @(posedge clock) t <= t + (t < 31);
+
+	assign A = trace_a[8*(31-t) +: 8] == "-";
+	assign B = trace_b[8*(31-t) +: 8] == "-";
+	assign C = trace_c[8*(31-t) +: 8] == "-";
+	assign D = trace_d[8*(31-t) +: 8] == "-";
+endmodule
+
+module pass_00 (input clock);
+	wire A, B, C, D;
+
+	sequencer #(
+		//        01234567890123456789012345678901
+		.trace_a("_-______________________________"),
+		.trace_b("__----__________________________"),
+		.trace_c("____----________________________"),
+		.trace_d("_____--_________________________")
+	) uut (clock, A, B, C, D);
+
+	assert property (@(posedge clock) $rose(A) |=> B ##2 C until D [*2]);
+endmodule
+
+module fail_01 (input clock);
+	wire A, B, C, D;
+
+	sequencer #(
+		//        01234567890123456789012345678901
+		.trace_a("_-______________________________"),
+		.trace_b("__----__________________________"),
+		.trace_c("____----________________________"),
+		.trace_d("____-_-_________________________")
+	) uut (clock, A, B, C, D);
+
+	assert property (@(posedge clock) $rose(A) |=> B ##2 C until D [*2]);
+endmodule
+
+module fail_02 (input clock);
+	wire A, B, C, D;
+
+	sequencer #(
+		//        01234567890123456789012345678901
+		.trace_a("_-______________________________"),
+		.trace_b("__----__________________________"),
+		.trace_c("____----________________________"),
+		.trace_d("_____--_________________________")
+	) uut (clock, A, B, C, D);
+
+	assert property (@(posedge clock) $rose(A) |=> B ##2 C until_with D [*2]);
+endmodule
+
+module pass_03 (input clock);
+	wire A, B, C, D;
+
+	sequencer #(
+		//        01234567890123456789012345678901
+		.trace_a("_-______________________________"),
+		.trace_b("__-----_________________________"),
+		.trace_c("____-----_______________________"),
+		.trace_d("_____--_________________________")
+	) uut (clock, A, B, C, D);
+
+	assert property (@(posedge clock) $rose(A) |=> B ##2 C until_with D [*2]);
+endmodule