Fix chformal selection parameter; add reset restrict to top-level

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.

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

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;