Initial commit

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_*

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

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;

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