27 files changed, 565 insertions, 4 deletions
diff --git a/tests/sat/sizebits.sv b/tests/sat/sizebits.sv
new file mode 100644
index 00000000..d7ce2326
--- /dev/null
+++ b/tests/sat/sizebits.sv
@@ -0,0 +1,32 @@
+module functions01;
+
+wire [5:2]x;
+wire [3:0]y[2:7];
+wire [3:0]z[7:2][2:9];
+
+//wire [$size(x)-1:0]x_size;
+//wire [$size({x, x})-1:0]xx_size;
+//wire [$size(y)-1:0]y_size;
+//wire [$size(z)-1:0]z_size;
+
+assert property ($size(x) == 4);
+assert property ($size({3{x}}) == 3*4);
+assert property ($size(y) == 6);
+assert property ($size(y, 1) == 6);
+assert property ($size(y, (1+1)) == 4);
+
+assert property ($size(z) == 6);
+assert property ($size(z, 1) == 6);
+assert property ($size(z, 2) == 8);
+assert property ($size(z, 3) == 4);
+// This should trigger an error if enabled (it does).
+//assert property ($size(z, 4) == 4);
+
+//wire [$bits(x)-1:0]x_bits;
+//wire [$bits({x, x})-1:0]xx_bits;
+
+assert property ($bits(x) == 4);
+assert property ($bits(y) == 4*6);
+assert property ($bits(z) == 4*6*8);
+
+endmodule
diff --git a/tests/sat/sizebits.ys b/tests/sat/sizebits.ys
new file mode 100644
index 00000000..689227a4
--- /dev/null
+++ b/tests/sat/sizebits.ys
@@ -0,0 +1,2 @@
+read_verilog -sv sizebits.sv
+prep; sat -verify -prove-asserts
diff --git a/tests/simple/arraycells.v b/tests/simple/arraycells.v
index 704ca3fd..fd85a119 100644
--- a/tests/simple/arraycells.v
+++ b/tests/simple/arraycells.v
@@ -2,7 +2,7 @@
 module array_test001(a, b, c, y);
 	input a;
 	input [31:0] b, c;
-	input [31:0] y;
+	output [31:0] y;
 
 	aoi12 p [31:0] (a, b, c, y);
 endmodule
diff --git a/tests/simple/graphtest.v b/tests/simple/graphtest.v
index 74788dbb..9b16b61c 100644
--- a/tests/simple/graphtest.v
+++ b/tests/simple/graphtest.v
@@ -25,7 +25,7 @@ assign Z[7:4] = {1'b0, B[2:0]};          // Concat of CV and PI connect to PO
 always @* begin
   if (A == 4'b1111) begin                // All-Const at port (eq)
     X = B;
-  end 
+  end
   else begin
     X = 4'b0000;                         // All-Const at port (mux)
   end
diff --git a/tests/simple/hierdefparam.v b/tests/simple/hierdefparam.v
new file mode 100644
index 00000000..ff92c38b
--- /dev/null
+++ b/tests/simple/hierdefparam.v
@@ -0,0 +1,23 @@
+module hierdefparam_top(input [7:0] A, output [7:0] Y);
+  generate begin:foo
+    hierdefparam_a mod_a(.A(A), .Y(Y));
+  end endgenerate
+  defparam foo.mod_a.bar[0].mod_b.addvalue = 42;
+  defparam foo.mod_a.bar[1].mod_b.addvalue = 43;
+endmodule
+
+module hierdefparam_a(input [7:0] A, output [7:0] Y);
+  genvar i;
+  generate
+    for (i = 0; i < 2; i=i+1) begin:bar
+      wire [7:0] a, y;
+      hierdefparam_b mod_b(.A(a), .Y(y));
+    end
+  endgenerate
+  assign bar[0].a = A, bar[1].a = bar[0].y, Y = bar[1].y;
+endmodule
+
+module hierdefparam_b(input [7:0] A, output [7:0] Y);
+  parameter [7:0] addvalue = 44;
+  assign Y = A + addvalue;
+endmodule
diff --git a/tests/simple/specify.v b/tests/simple/specify.v
new file mode 100644
index 00000000..f19418d9
--- /dev/null
+++ b/tests/simple/specify.v
@@ -0,0 +1,31 @@
+module test_specify;
+
+specparam a=1;
+
+specify
+endspecify
+
+specify
+(A => B) = ( 1 ) ;
+(A- => B) = ( 1,2 ) ;
+(A+ => B) = ( 1,2,3 ) ;
+(A => B) = (
+ 1.1, 2, 3,
+ 4, 5.5, 6.6
+) ;
+(A => B) = (
+ 1.1, 2, 3,
+ 4, 5.5, 6.6 ,
+ 7.7, 8.8, 9,
+ 10.1, 11, 12
+) ;
+specparam b=1;
+specparam [1:2] asasa=1;
+endspecify
+
+specify
+specparam c=1:2:3;
+endspecify
+
+endmodule
+
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
diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh
index d0b0a89d..d6216244 100755
--- a/tests/tools/autotest.sh
+++ b/tests/tools/autotest.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 libs=""
 genvcd=false
@@ -100,7 +100,7 @@ do
 		echo -n "Test: $bn "
 	fi
 
-	rm -f ${bn}.{err,log,sikp}
+	rm -f ${bn}.{err,log,skip}
 	mkdir -p ${bn}.out
 	rm -rf ${bn}.out/*
 
diff --git a/tests/unit/Makefile b/tests/unit/Makefile
new file mode 100644
index 00000000..9f1e5c99
--- /dev/null
+++ b/tests/unit/Makefile
@@ -0,0 +1,35 @@
+GTESTFLAG := -lgtest -lgtest_main
+RPATH := -Wl,-rpath
+EXTRAFLAGS := -lyosys -pthreads
+
+OBJTEST := objtest
+BINTEST := bintest
+
+ALLTESTFILE := $(shell find -name '*Test.cc' -printf '%P ')
+TESTDIRS := $(sort $(dir $(ALLTESTFILE)))
+TESTS := $(addprefix $(BINTEST)/, $(basename $(ALLTESTFILE:%Test.cc=%Test.o)))
+
+# Prevent make from removing our .o files
+.SECONDARY:
+
+all: prepare $(TESTS) run-tests
+
+$(BINTEST)/%: $(OBJTEST)/%.o
+	$(CXX) -L$(ROOTPATH) $(RPATH)=$(ROOTPATH) -o $@ $^ $(LDLIBS) \
+		$(GTESTFLAG) $(EXTRAFLAGS)
+
+$(OBJTEST)/%.o: $(basename $(subst $(OBJTEST),.,%)).cc
+	$(CXX) -o $@ -c -I$(ROOTPATH) $(CPPFLAGS) $(CXXFLAGS) $^
+
+.PHONY: prepare run-tests clean
+
+run-tests: $(TESTS)
+	$(subst Test ,Test; ,$^)
+
+prepare:
+	mkdir -p $(addprefix $(BINTEST)/,$(TESTDIRS))
+	mkdir -p $(addprefix $(OBJTEST)/,$(TESTDIRS))
+
+clean:
+	rm -rf $(OBJTEST)
+	rm -rf $(BINTEST)
diff --git a/tests/unit/kernel/logTest.cc b/tests/unit/kernel/logTest.cc
new file mode 100644
index 00000000..62b4f3b9
--- /dev/null
+++ b/tests/unit/kernel/logTest.cc
@@ -0,0 +1,14 @@
+#include <gtest/gtest.h>
+
+#include "kernel/yosys.h"
+#include "kernel/log.h"
+
+YOSYS_NAMESPACE_BEGIN
+
+TEST(KernelLogTest, logvValidValues)
+{
+	//TODO: Implement log test
+	EXPECT_EQ(7, 7);
+}
+
+YOSYS_NAMESPACE_END
diff --git a/tests/unit/kernel/rtlilTest.cc b/tests/unit/kernel/rtlilTest.cc
new file mode 100644
index 00000000..d9eeed55
--- /dev/null
+++ b/tests/unit/kernel/rtlilTest.cc
@@ -0,0 +1,14 @@
+#include <gtest/gtest.h>
+
+#include "kernel/yosys.h"
+#include "kernel/rtlil.h"
+
+YOSYS_NAMESPACE_BEGIN
+
+TEST(KernelRtlilTest, getReferenceValid)
+{
+	//TODO: Implement rtlil test
+	EXPECT_EQ(33, 33);
+}
+
+YOSYS_NAMESPACE_END
diff --git a/tests/various/reg_wire_error.sv b/tests/various/reg_wire_error.sv
new file mode 100644
index 00000000..fe5ff3ab
--- /dev/null
+++ b/tests/various/reg_wire_error.sv
@@ -0,0 +1,74 @@
+module sub_mod(input i_in, output o_out);
+assign o_out = i_in;
+endmodule
+
+module test(i_clk, i, i_reg, o_reg, o_wire, o_mr, o_mw, o_ml);
+input i_clk;
+input i;
+input i_reg;
+output o_reg;
+output o_wire;
+output o_mr, o_mw, o_ml;
+
+// Enable this to see how it doesn't fail on yosys although it should
+//reg o_wire;
+// Enable this instead of the above to see how logic can be mapped to a wire
+logic o_wire;
+// Enable this to see how it doesn't fail on yosys although it should
+//reg i_reg;
+// Disable this to see how it doesn't fail on yosys although it should
+//reg o_reg;
+
+logic l_reg;
+
+// Enable this to tst if logic-turne-reg will catch assignments even if done before it turned into a reg
+assign l_reg = !o_reg;
+initial o_reg = 1'b0;
+always @(posedge i_clk)
+begin
+  o_reg <= !o_reg;
+  l_reg <= !o_reg;
+end
+
+assign o_wire = !o_reg;
+// Uncomment this to see how a logic already turned intoa reg can be freely assigned on yosys
+assign l_reg = !o_reg;
+
+sub_mod sm_inst (
+  .i_in(1'b1),
+  .o_out(o_reg)
+);
+
+wire   mw1[0:1];
+wire   mw2[0:1];
+wire   mw3[0:1];
+reg    mr1[0:1];
+reg    mr2[0:1];
+reg    mr3[0:1];
+logic  ml1[0:1];
+logic  ml2[0:1];
+logic  ml3[0:1];
+
+assign o_mw = mw1[i];
+assign o_mr = mr1[i];
+assign o_ml = ml1[i];
+
+assign mw1[1] = 1'b1;
+//assign mr1[1] = 1'b1;
+assign ml1[1] = 1'b1;
+always @(posedge i_clk)
+begin
+  mr2[0] = 1'b0;
+  mw2[0] = 1'b0;
+  ml2[0] = 1'b0;
+end
+
+always @(posedge i_clk)
+begin
+  mr3[0] <= 1'b0;
+  mw3[0] <= 1'b0;
+  ml3[0] <= 1'b0;
+end
+
+endmodule
+
diff --git a/tests/various/reg_wire_error.ys b/tests/various/reg_wire_error.ys
new file mode 100644
index 00000000..b9d03155
--- /dev/null
+++ b/tests/various/reg_wire_error.ys
@@ -0,0 +1 @@
+read_verilog -sv reg_wire_error.sv