commit b0d52f1534247fdcedb4a4ed79a4361f06dfc100
Author: Torsten Meissner <programming@goodcleanfun.de>
Date:   Tue Jan 22 14:03:23 2019 +0100

    Initial commit

diff --git a/symbiotic_01/Makefile b/symbiotic_01/Makefile
new file mode 100644
index 0000000..d8bd2a4
--- /dev/null
+++ b/symbiotic_01/Makefile
@@ -0,0 +1,30 @@
+SYMBI_SRC_FILE := /opt/symbiotic.sh
+
+TASKS := flag_check
+
+
+.PHONY: all
+all: flag_check
+
+
+define taskTemplate
+
+.PHONY: $(1)
+$(1):
+	source $(SYMBI_SRC_FILE); sby -f symbiyosys.sby $(1)
+
+endef
+
+$(foreach task, $(TASKS), $(eval $(call taskTemplate,$(task))))
+
+
+wave:
+ifndef wf
+	$(error please give wave parameter)
+endif
+	gtkwave -a trace.gtkw $(wf)
+
+
+.PHONY: clean
+clean:
+	rm -rf symbiyosys_*
diff --git a/symbiotic_01/Properties.sv b/symbiotic_01/Properties.sv
new file mode 100644
index 0000000..b4055b7
--- /dev/null
+++ b/symbiotic_01/Properties.sv
@@ -0,0 +1,37 @@
+module Properties (
+  // global
+  input        clk,
+  input        resetn,
+  input  [1:0] sel,
+  input  [3:0] we
+);
+
+
+  // Constrain reset
+
+  reg init_flag = 1;
+
+  always @(*) begin
+    if (init_flag) assume (!resetn);
+    if (!init_flag) assume (resetn);
+  end
+
+  always @(posedge clk)
+    init_flag <= 0;
+
+
+  default clocking
+    @(posedge clk);
+  endclocking
+
+  default disable iff (!resetn);
+
+
+  assert property (we[0] |=> sel == 0);
+
+
+endmodule
+
+
+
+bind TestDesign Properties i_Properties (.*);
diff --git a/symbiotic_01/TestDesign.vhd b/symbiotic_01/TestDesign.vhd
new file mode 100644
index 0000000..de9f830
--- /dev/null
+++ b/symbiotic_01/TestDesign.vhd
@@ -0,0 +1,37 @@
+library ieee;
+  use ieee.std_logic_1164.all;
+  use ieee.numeric_std.all;
+
+
+
+entity TestDesign is
+  port (
+    clk    : in  std_logic;
+    resetn : in  std_logic;
+    sel    : in  std_logic_vector(1 downto 0);
+    we     : out std_logic_vector(3 downto 0)
+  );
+end entity TestDesign;
+
+
+
+architecture rtl of TestDesign is
+
+
+begin
+
+
+  process (CLK, RESETn) is
+  begin
+    if (RESETn = '0') then
+      we <= (others => '0');
+    elsif (rising_edge(CLK)) then
+      we(0) <= '0' when sel = "00" else '1';
+      we(1) <= '0' when sel = "01" else '1';
+      we(2) <= '0' when sel = "10" else '1';
+      we(3) <= '0' when sel = "11" else '1';
+    end if;
+  end process;
+
+
+end architecture;
diff --git a/symbiotic_01/symbiyosys.sby b/symbiotic_01/symbiyosys.sby
new file mode 100644
index 0000000..d9a6e5d
--- /dev/null
+++ b/symbiotic_01/symbiyosys.sby
@@ -0,0 +1,20 @@
+[tasks]
+flag_check
+
+[options]
+mode prove
+depth 30
+
+[engines]
+abc pdr
+
+[script]
+verific -vhdl TestDesign.vhd
+verific -sv   Properties.sv
+verific -import -extnets -all TestDesign
+prep -top TestDesign
+setundef -anyseq -undriven
+
+[files]
+Properties.sv
+TestDesign.vhd