From 445c013e5cbb9449b5c5bd0b5387b184a320e461 Mon Sep 17 00:00:00 2001
From: Torsten Meissner <programming@goodcleanfun.de>
Date: Tue, 13 Nov 2018 15:43:36 +0100
Subject: [PATCH] Add example for dlatchsr error

---
 dlatchsr/Makefile     |  7 +++++++
 dlatchsr/dlatch.vhd   | 42 ++++++++++++++++++++++++++++++++++++++++++
 dlatchsr/dlatch_f.sby | 17 +++++++++++++++++
 dlatchsr/dlatch_t.sv  | 36 ++++++++++++++++++++++++++++++++++++
 4 files changed, 102 insertions(+)
 create mode 100644 dlatchsr/Makefile
 create mode 100644 dlatchsr/dlatch.vhd
 create mode 100644 dlatchsr/dlatch_f.sby
 create mode 100644 dlatchsr/dlatch_t.sv

diff --git a/dlatchsr/Makefile b/dlatchsr/Makefile
new file mode 100644
index 0000000..e19d839
--- /dev/null
+++ b/dlatchsr/Makefile
@@ -0,0 +1,7 @@
+.PHONY: dlatch
+dlatch: dlatch.vhd dlatch_t.sv dlatch_f.sby
+	sby -f -d work dlatch_f.sby
+
+.PHONY: clean
+clean:
+	rm -rf work
diff --git a/dlatchsr/dlatch.vhd b/dlatchsr/dlatch.vhd
new file mode 100644
index 0000000..85b9538
--- /dev/null
+++ b/dlatchsr/dlatch.vhd
@@ -0,0 +1,42 @@
+library ieee;
+use ieee.std_logic_1164.all;
+use ieee.numeric_std.all;
+
+
+
+entity dlatch is
+  generic (
+    Init : std_logic_vector(31 downto 0) := x"DEADBEEF"
+  );
+  port (
+    Reset_n_i : in  std_logic;
+    Clk_i     : in  std_logic;
+    Wen_i     : in  std_logic;
+    Data_i    : in  std_logic_vector(15 downto 0);
+    Data_o    : out std_logic_vector(31 downto 0)
+  );
+end entity dlatch;
+
+
+
+architecture rtl of dlatch is
+
+
+begin
+
+
+  process (Reset_n_i, Clk_i) is
+  begin
+    if (Reset_n_i = '0') then
+      Data_o <= Init;
+    elsif (rising_edge(Clk_i)) then
+      if (Wen_i = '1') then
+        Data_o(7 downto 0) <= Data_i(7 downto 0);
+	Data_o(23 downto 16) <= Data_i(15 downto 8);
+      end if;
+    end if;
+  end process;
+
+
+end architecture rtl;
+
diff --git a/dlatchsr/dlatch_f.sby b/dlatchsr/dlatch_f.sby
new file mode 100644
index 0000000..4128723
--- /dev/null
+++ b/dlatchsr/dlatch_f.sby
@@ -0,0 +1,17 @@
+[options]
+mode prove
+depth 20
+# falis with multiclock disabled
+multiclock off
+
+[engines]
+smtbmc
+
+[script]
+verific -vhdl dlatch.vhd
+verific -formal dlatch_t.sv
+prep -top dlatch_t
+
+[files]
+dlatch.vhd
+dlatch_t.sv
diff --git a/dlatchsr/dlatch_t.sv b/dlatchsr/dlatch_t.sv
new file mode 100644
index 0000000..ef3fc1a
--- /dev/null
+++ b/dlatchsr/dlatch_t.sv
@@ -0,0 +1,36 @@
+module dlatch_t (
+    input         Reset_n_i,
+    input         Clk_i,
+    input         Wen_i,
+    input  [15:0] Data_i,
+    output [31:0] Data_o
+);
+
+
+  `define INIT_VALUE 32'hDEADBEEF
+
+
+  dlatch #(.Init(`INIT_VALUE)) dlatch_i (
+    .Reset_n_i(Reset_n_i),
+    .Clk_i(Clk_i),
+    .Wen_i(Wen_i),
+    .Data_i(Data_i),
+    .Data_o(Data_o)
+  );
+
+
+  reg init_state = 1;
+
+  always @(*)
+    if (init_state) assume (!Reset_n_i);
+
+  always @(posedge Clk_i)
+    init_state = 0;
+
+
+  always @(*)
+    if (!Reset_n_i) assert (Data_o == `INIT_VALUE);
+
+
+endmodule
+