formal_hw_verification's Introduction

The original repository is located on my own git-server at https://git.goodcleanfun.de/tmeissner/formal_hw_verification

It is mirrored to github with every push, so both should be in sync.

formal_hw_verification

Tests and examples of using formal verification to check correctness of digital hardware designs. All tests are done with SymbiYosys, a front-end for formal verification flows based on Yosys.

All stuff in the master branch uses ghdl-yosys-plugin and GHDL as VHDL front-end plugin for (Symbi)Yosys. Using GHDL as synthesis frontend allows using PSL as verification language.

Some examples in the verific branch use the commercial VHDL/SystemVerilog frontend plugin by Verific which isn't free SW. It's included in the Tabby CAD Suite but not in the free Yosys version. See on the Yosys HQ website for more information.

You can use the hdlc/formal:all docker image provided by the hdl containers project (recommended). Or you build a docker image on your own machine using my Dockerfiles for SymbiYosys & GHDL. With both you have the latest tool versions available.

alu

A simple ALU design in VHDL. The formal checks contain various simple properties used by assert & cover directives which are proved with the SymbiYosys tool.

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.

fifo

A simple synchronous FIFO with various checks for write/read pointers, data and flags.

fwft_fifo

A simple synchronous FIFO with first-word fall-through behaviour. Uses fifo as sub-unit. This design serves as an example how to verify designs with sub-units containing formal checks.

vai_fifo

A simple FIFO with valid-accept interface. Consists of fwft_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.

formal_hw_verification's People

Contributors

Stargazers

Watchers

formal_hw_verification's Issues

FIFO empty flag calculation wrong when reading from empty FIFO

Maybe the FIFO is empty after reset. If one write & read then at the same time, the FIFO don't goes out of empty state. This is caused by the condition to deassert the empty flag:

if (Wen_i = '1' and Ren_i = '0') then
  if ((s_write_pnt = s_read_pnt - 1) or
      (s_write_pnt = t_fifo_mem'high and s_read_pnt = t_fifo_mem'low)) then
    Full_o <= '1';
  end if;
  Empty_o <= '0';
end if;

At the same time, an read is ignored when FIFO is empty (and an read error is asserted). So the data is written into the FIFO memory but not read. Write pointer is incremented, read pointer not. So, the FIFO should be not empty after the first data was written into it, as the read from the empty FIFO before was ignored.

It's awful that these bug wasn't found by the formal checks. It shows that such simple low-level checks are not only tedious to write, but also often only incompletely test the design behaviour.

Recommend Projects

tmeissner / formal_hw_verification Goto Github PK

formal_hw_verification's Introduction

formal_hw_verification

alu

counter

fifo

fwft_fifo

vai_fifo

vai_reg

formal_hw_verification's People

Contributors

Stargazers

Watchers

Forkers

formal_hw_verification's Issues

FIFO empty flag calculation wrong when reading from empty FIFO

Recommend Projects

React

Vue.js

Typescript

TensorFlow

Django

Laravel

D3

Recommend Topics

javascript

web

server

Machine learning

Visualization

Game

Recommend Org

Facebook

Microsoft

Google

Alibaba

D3

Tencent