New upstream version 0.7+20180830git0b7a184

15 files changed, 335 insertions, 0 deletions

diff --git a/tests/sva/.gitignore b/tests/sva/.gitignore
new file mode 100644
index 00000000..cc254049
--- /dev/null
+++ b/tests/sva/.gitignore
@@ -0,0 +1,7 @@
+/*_pass.sby
+/*_fail.sby
+/*_pass
+/*_fail
+/*.ok
+/vhdlpsl[0-9][0-9]
+/vhdlpsl[0-9][0-9].sby
diff --git a/tests/sva/Makefile b/tests/sva/Makefile
new file mode 100644
index 00000000..1b217f74
--- /dev/null
+++ b/tests/sva/Makefile
@@ -0,0 +1,13 @@
+
+TESTS = $(sort $(basename $(wildcard *.sv)) $(basename $(wildcard *.vhd)))
+
+all: $(addsuffix .ok,$(TESTS))
+
+%.ok:
+	bash runtest.sh $@
+
+clean:
+	rm -rf $(addsuffix .ok,$(TESTS)) $(addsuffix .sby,$(TESTS)) $(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
new file mode 100644
index 00000000..30c37f5f
--- /dev/null
+++ b/tests/sva/basic00.sv
@@ -0,0 +1,12 @@
+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
new file mode 100644
index 00000000..74ab9343
--- /dev/null
+++ b/tests/sva/basic01.sv
@@ -0,0 +1,16 @@
+module top (input logic clock, ctrl);
+	logic read = 0, write = 0, ready = 0;
+
+	always @(posedge clock) begin
+		read <= !ctrl;
+		write <= ctrl;
+		ready <= write;
+	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
new file mode 100644
index 00000000..b34f3aff
--- /dev/null
+++ b/tests/sva/basic02.sv
@@ -0,0 +1,20 @@
+module top (input logic clock, ctrl);
+	logic read = 0, write = 0, ready = 0;
+
+	always @(posedge clock) begin
+		read <= !ctrl;
+		write <= ctrl;
+		ready <= write;
+	end
+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
new file mode 100644
index 00000000..8018de4c
--- /dev/null
+++ b/tests/sva/basic03.sv
@@ -0,0 +1,12 @@
+module top (input logic clk, input logic selA, selB, QA, QB, output logic Q);
+	always @(posedge clk) begin
+		if (selA) Q <= QA;
+		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) );
+`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
new file mode 100644
index 00000000..bc46be9f
--- /dev/null
+++ b/tests/sva/basic04.sv
@@ -0,0 +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
new file mode 100644
index 00000000..f2ec305e
--- /dev/null
+++ b/tests/sva/basic04.vhd
@@ -0,0 +1,26 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity top is
+	port (
+		clock : in std_logic;
+		ctrl : in std_logic;
+		x : out std_logic
+	);
+end entity;
+
+architecture rtl of top is
+	signal read : std_logic := '0';
+	signal write : std_logic := '0';
+	signal ready : std_logic := '0';
+begin
+	process (clock) begin
+		if (rising_edge(clock)) then
+			read <= not ctrl;
+			write <= ctrl;
+			ready <= write;
+		end if;
+	end process;
+
+	x <= read xor write xor ready;
+end architecture;
diff --git a/tests/sva/basic05.sv b/tests/sva/basic05.sv
new file mode 100644
index 00000000..816ee1da
--- /dev/null
+++ b/tests/sva/basic05.sv
@@ -0,0 +1,19 @@
+module top (input logic clock, ctrl);
+	logic read, write, ready;
+
+	demo uut (
+		.clock(clock),
+		.ctrl(ctrl)
+	);
+
+	assign read = uut.read;
+	assign write = uut.write;
+	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
new file mode 100644
index 00000000..8d42f71e
--- /dev/null
+++ b/tests/sva/basic05.vhd
@@ -0,0 +1,26 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity demo is
+	port (
+		clock : in std_logic;
+		ctrl : in std_logic;
+		x : out std_logic
+	);
+end entity;
+
+architecture rtl of demo is
+	signal read : std_logic := '0';
+	signal write : std_logic := '0';
+	signal ready : std_logic := '0';
+begin
+	process (clock) begin
+		if (rising_edge(clock)) then
+			read <= not ctrl;
+			write <= ctrl;
+			ready <= write;
+		end if;
+	end process;
+
+	x <= read xor write xor ready;
+end architecture;
diff --git a/tests/sva/counter.sv b/tests/sva/counter.sv
new file mode 100644
index 00000000..4f949115
--- /dev/null
+++ b/tests/sva/counter.sv
@@ -0,0 +1,30 @@
+module top (input clk, reset, up, down, output reg [7:0] cnt);
+	always @(posedge clk) begin
+		if (reset)
+			cnt <= 0;
+		else if (up)
+			cnt <= cnt + 1;
+		else if (down)
+			cnt <= cnt - 1;
+	end
+
+	default clocking @(posedge clk); endclocking
+	default disable iff (reset);
+
+	assert property (up |=> cnt == $past(cnt) + 8'd 1);
+	assert property (up [*2] |=> cnt == $past(cnt, 2) + 8'd 2);
+	assert property (up ##1 up |=> cnt == $past(cnt, 2) + 8'd 2);
+
+`ifndef FAIL
+	assume property (down |-> !up);
+`endif
+	assert property (up ##1 down |=> cnt == $past(cnt, 2));
+	assert property (down |=> cnt == $past(cnt) - 8'd 1);
+
+	property down_n(n);
+		down [*n] |=> cnt == $past(cnt, n) - n;
+	endproperty
+
+	assert property (down_n(8'd 3));
+	assert property (down_n(8'd 5));
+endmodule
diff --git a/tests/sva/runtest.sh b/tests/sva/runtest.sh
new file mode 100644
index 00000000..1b65ca9c
--- /dev/null
+++ b/tests/sva/runtest.sh
@@ -0,0 +1,72 @@
+#!/bin/bash
+
+set -ex
+
+prefix=${1%.ok}
+prefix=${prefix%.sv}
+prefix=${prefix%.vhd}
+test -f $prefix.sv -o -f $prefix.vhd
+
+generate_sby() {
+	cat <<- EOT
+		[options]
+		mode bmc
+		depth 10
+		expect $1
+
+		[engines]
+		smtbmc yices
+
+		[script]
+	EOT
+
+	if [ -f $prefix.sv ]; then
+		if [ "$1" = "fail" ]; then
+			echo "verific -sv ${prefix}_fail.sv"
+		else
+			echo "verific -sv $prefix.sv"
+		fi
+	fi
+
+	if [ -f $prefix.vhd ]; then
+		echo "verific -vhdl $prefix.vhd"
+	fi
+
+	cat <<- EOT
+		verific -import -extnets -all top
+		prep -top top
+		chformal -early -assume
+
+		[files]
+	EOT
+
+	if [ -f $prefix.sv ]; then
+		echo "$prefix.sv"
+	fi
+
+	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
+}
+
+if [ -f $prefix.sv ]; then
+	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
+else
+	generate_sby pass > ${prefix}.sby
+	sby --yosys $PWD/../../yosys -f ${prefix}.sby
+fi
+
+touch $prefix.ok
+
diff --git a/tests/sva/sva_not.sv b/tests/sva/sva_not.sv
new file mode 100644
index 00000000..d81a4865
--- /dev/null
+++ b/tests/sva/sva_not.sv
@@ -0,0 +1,34 @@
+module top (
+	input clk,
+	input reset,
+	input ping,
+	input [1:0] cfg,
+	output reg pong
+);
+	reg [2:0] cnt;
+	localparam integer maxdelay = 8;
+
+	always @(posedge clk) begin
+		if (reset) begin
+			cnt <= 0;
+			pong <= 0;
+		end else begin
+			cnt <= cnt - |cnt;
+			pong <= cnt == 1;
+			if (ping) cnt <= 4 + cfg;
+		end
+	end
+
+	assert property (
+		@(posedge clk)
+		disable iff (reset)
+		not (ping ##1 !pong [*maxdelay])
+	);
+
+`ifndef FAIL
+	assume property (
+		@(posedge clk)
+		not (cnt && ping)
+	);
+`endif
+endmodule
diff --git a/tests/sva/sva_range.sv b/tests/sva/sva_range.sv
new file mode 100644
index 00000000..d1569fc8
--- /dev/null
+++ b/tests/sva/sva_range.sv
@@ -0,0 +1,19 @@
+module top (
+	input clk,
+	input a, b, c, d
+);
+	default clocking @(posedge clk); endclocking
+
+	assert property (
+		a ##[*] b |=> c until d
+	);
+
+`ifndef FAIL
+	assume property (
+		b |=> ##5 d
+	);
+	assume property (
+		b || (c && !d) |=> c
+	);
+`endif
+endmodule
diff --git a/tests/sva/sva_throughout.sv b/tests/sva/sva_throughout.sv
new file mode 100644
index 00000000..7e036a06
--- /dev/null
+++ b/tests/sva/sva_throughout.sv
@@ -0,0 +1,19 @@
+module top (
+	input clk,
+	input a, b, c, d
+);
+	default clocking @(posedge clk); endclocking
+
+	assert property (
+		a |=> b throughout (c ##1 d)
+	);
+
+`ifndef FAIL
+	assume property (
+		a |=> b && c
+	);
+	assume property (
+		b && c |=> b && d
+	);
+`endif
+endmodule