From 36d6da1943dd0cdbab3c673de8b371cd2ac3a287 Mon Sep 17 00:00:00 2001 From: tmeissner Date: Tue, 24 Mar 2020 14:39:09 +0100 Subject: [PATCH] Minor updates to README file (cherry picked from commit 1ef9d692c8ad53bfb34f45024507e892e1ff8415) --- README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index a369fbd..e3ac6ad 100644 --- a/README.md +++ b/README.md @@ -3,17 +3,17 @@ The original repository is located on my own git-server at [https://git.goodclea It is mirrored to github with every push, so both should be in sync. -# formal_verification +# 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](https://github.com/YosysHQ). Some examples use the VHDL/SystemVerilog frontend plugin by Verific which isn't free SW and not included in the free Yosys version. See on the [Symbiotic EDA website](https://www.symbioticeda.com) for more information. There is a branch named [ghdl-synth](https://github.com/tmeissner/formal_hw_verification/tree/ghdl-synth) which uses [ghdlsynth-beta](https://github.com/tgingold/ghdlsynth-beta) as VHDL frontend plugin for SymbiYosys. Furthermore using GHDL(synth) as synthesis frontend allows using PSL as verification language. Only the vai_reg design can be verified in this branch at the moment. ### alu -A simple ALU design in VHDL, together with a formal testbench written in SystemVerilog. The testbench contains various simple SVA properties used by assert & cover directives which are proved with the SymbiYosys tool. +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, together with a formal testbench written in SystemVerilog. The testbench contains various simple SVA properties used by assert & cover directives which are proved with the SymbiYosys tool. +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.