Browse Source

Removing verific related dlatchsr from master branch

master
T. Meissner 4 years ago
parent
commit
903931b2d9
5 changed files with 0 additions and 105 deletions
  1. +0
    -3
      README.md
  2. +0
    -7
      dlatchsr/Makefile
  3. +0
    -42
      dlatchsr/dlatch.vhd
  4. +0
    -17
      dlatchsr/dlatch_f.sby
  5. +0
    -36
      dlatchsr/dlatch_t.sv

+ 0
- 3
README.md View File

@ -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.

+ 0
- 7
dlatchsr/Makefile View File

@ -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

+ 0
- 42
dlatchsr/dlatch.vhd View File

@ -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;

+ 0
- 17
dlatchsr/dlatch_f.sby View File

@ -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

+ 0
- 36
dlatchsr/dlatch_t.sv View File

@ -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

Loading…
Cancel
Save