From 3da2f2df9e49b86efc4e5d2e78ad30f3a95c65d0 Mon Sep 17 00:00:00 2001 From: tmeissner Date: Mon, 8 Jun 2020 12:38:30 +0200 Subject: [PATCH] Update README to renamed branches --- README.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index feece6a..9b4357c 100644 --- a/README.md +++ b/README.md @@ -5,9 +5,11 @@ 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](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. +Tests and examples of using formal verification to check correctness of digital hardware designs. All tests are done with [SymbiYosys](https://github.com/YosysHQ/SymbiYosys), a front-end for formal verification flows based on [Yosys](https://github.com/YosysHQ/yosys). -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. The alu, counter & vai_reg designs can be verified in this branch at the moment. +All stuff in the master branch uses [ghdl-yosys-plugin](https://github.com/ghdl/ghdl-yosys-plugin) and [GHDL](https://github.com/ghdl/ghdl) as VHDL front-end plugin for (Symbi)Yosys. Using GHDL as synthesis frontend allows using PSL as verification language. The alu, counter & vai_reg designs can be verified with that combination at the moment. + +Some examples in the [verific branch](https://github.com/tmeissner/formal_hw_verification/tree/verific) use the commercial 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. ### 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. @@ -16,7 +18,7 @@ A simple ALU design in VHDL. The formal checks contain various simple properties 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. +A simple test design which generates the `Unsupported cell type $dlatchsr` error using with Verific plugin (verific branch). ### vai_reg A simple register file with VAI (valid-accept-interface) which serves as test design to try formal verification of FSMs. \ No newline at end of file