From 903931b2d9d70d46ac757d805659e6f9b081295a Mon Sep 17 00:00:00 2001 From: tmeissner Date: Mon, 8 Jun 2020 13:14:15 +0200 Subject: [PATCH] Removing verific related dlatchsr from master branch --- README.md | 3 --- dlatchsr/Makefile | 7 ------- dlatchsr/dlatch.vhd | 42 ------------------------------------------ dlatchsr/dlatch_f.sby | 17 ----------------- dlatchsr/dlatch_t.sv | 36 ------------------------------------ 5 files changed, 105 deletions(-) delete mode 100644 dlatchsr/Makefile delete mode 100644 dlatchsr/dlatch.vhd delete mode 100644 dlatchsr/dlatch_f.sby delete mode 100644 dlatchsr/dlatch_t.sv diff --git a/README.md b/README.md index 9b4357c..9906e5f 100644 --- a/README.md +++ b/README.md @@ -17,8 +17,5 @@ A simple ALU design in VHDL. The formal checks contain various simple properties ### counter A simple counter design in VHDL. The testbench contains various simple properties used by assert & cover directives which are proved with the SymbiYosys tool. -### dlatch -A simple test design which generates the `Unsupported cell type $dlatchsr` error using with Verific plugin (verific branch). - ### vai_reg A simple register file with VAI (valid-accept-interface) which serves as test design to try formal verification of FSMs. \ No newline at end of file diff --git a/dlatchsr/Makefile b/dlatchsr/Makefile deleted file mode 100644 index e19d839..0000000 --- a/dlatchsr/Makefile +++ /dev/null @@ -1,7 +0,0 @@ -.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 deleted file mode 100644 index 85b9538..0000000 --- a/dlatchsr/dlatch.vhd +++ /dev/null @@ -1,42 +0,0 @@ -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 deleted file mode 100644 index 4128723..0000000 --- a/dlatchsr/dlatch_f.sby +++ /dev/null @@ -1,17 +0,0 @@ -[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 deleted file mode 100644 index ef3fc1a..0000000 --- a/dlatchsr/dlatch_t.sv +++ /dev/null @@ -1,36 +0,0 @@ -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 -