From 4adea23c43552319296008e159378ca3e02da8b1 Mon Sep 17 00:00:00 2001 From: tmeissner Date: Wed, 6 Jan 2021 17:01:49 +0100 Subject: [PATCH] Fix chformal selection parameter; add reset restrict to top-level --- README.md | 2 +- vai_fifo/symbiyosys.sby | 6 ++---- vai_fifo/vai_fifo.vhd | 8 +++++++- 3 files changed, 10 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index deb4823..c4f30a8 100644 --- a/README.md +++ b/README.md @@ -21,7 +21,7 @@ A simple counter design in VHDL. The testbench contains various simple propertie A simple synchronous FIFO with various checks for write/read pointers, data and flags. ### vai_fifo -A simple FIFO with valid-accept interface. Consists of the fifo unit and some glue logic doing fifo<->vai interface conversion. +A simple FIFO with valid-accept-interface. Consists of fifo as sub-unit and some glue logic doing fifo<->vai interface conversion. This design serves as an example how to verify designs with sub-units containing formal checks. ### vai_reg A simple register file with VAI (valid-accept-interface) which serves as test design to try formal verification of FSMs. diff --git a/vai_fifo/symbiyosys.sby b/vai_fifo/symbiyosys.sby index 5e52922..194334c 100644 --- a/vai_fifo/symbiyosys.sby +++ b/vai_fifo/symbiyosys.sby @@ -11,15 +11,13 @@ prove: mode prove [engines] cover: smtbmc z3 -bmc: smtbmc z3 -#abc bmc3 +bmc: abc bmc3 prove: abc pdr [script] ghdl --std=08 -gFormal=true -gDepth=16 -gWidth=16 fifo.vhd vai_fifo.vhd -e vai_fifo prep -top vai_fifo -#chformal -assume -remove vai_fifo/* -chformal -assume -remove vai_fifo/i_fifo +chformal -assume2assert vai_fifo/i_fifo %M [files] ../fifo/fifo.vhd diff --git a/vai_fifo/vai_fifo.vhd b/vai_fifo/vai_fifo.vhd index 7f1e014..dde4459 100644 --- a/vai_fifo/vai_fifo.vhd +++ b/vai_fifo/vai_fifo.vhd @@ -72,8 +72,14 @@ begin default clock is rising_edge(Clk_i); + -- Initial reset + RESTRICT_RESET : restrict + {not Reset_n_i[*3]; Reset_n_i[+]}[*1]; + -- Inputs are low during reset for simplicity - vai_fifo_reset_a : assume always not Reset_n_i -> not Valid_i and not Accept_i; + ASSUME_INPUTS_DURING_RESET : assume always + not Reset_n_i -> + not Valid_i and not Accept_i; end generate FormalG;