Browse Source

Add example for dlatchsr error

verific_problem
T. Meissner 5 years ago
parent
commit
445c013e5c
4 changed files with 102 additions and 0 deletions
  1. +7
    -0
      dlatchsr/Makefile
  2. +42
    -0
      dlatchsr/dlatch.vhd
  3. +17
    -0
      dlatchsr/dlatch_f.sby
  4. +36
    -0
      dlatchsr/dlatch_t.sv

+ 7
- 0
dlatchsr/Makefile View File

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

+ 42
- 0
dlatchsr/dlatch.vhd View File

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

+ 17
- 0
dlatchsr/dlatch_f.sby View File

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

+ 36
- 0
dlatchsr/dlatch_t.sv View File

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

Loading…
Cancel
Save