diff --git a/COPYING b/COPYING index eba1da2..dd111ea 100644 --- a/COPYING +++ b/COPYING @@ -1,4 +1,4 @@ -SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows +SBY -- Front-end for Yosys-based formal verification flows Copyright (C) 2016 Claire Xenia Wolf diff --git a/Makefile b/Makefile index fa07df3..eb745c7 100644 --- a/Makefile +++ b/Makefile @@ -21,7 +21,7 @@ endif help: @echo "" @echo "sudo make install" - @echo " build and install SymbiYosys (sby)" + @echo " build and install SBY" @echo "" @echo "make html" @echo " build documentation in docs/build/html/" diff --git a/README.md b/README.md index 905830b..cd5c800 100644 --- a/README.md +++ b/README.md @@ -1,10 +1,10 @@ -SymbiYosys (sby) is a front-end driver program for [Yosys](https://yosyshq.net/yosys/)-based formal hardware verification flows. See [https://yosyshq.readthedocs.io/projects/sby/](https://yosyshq.readthedocs.io/projects/sby/) for documentation on how to use SymbiYosys. +SBY is a front-end driver program for [Yosys](https://yosyshq.net/yosys/)-based formal hardware verification flows. See [https://yosyshq.readthedocs.io/projects/sby/](https://yosyshq.readthedocs.io/projects/sby/) for documentation on how to use SBY. -SymbiYosys (sby) itself is licensed under the ISC license, note that the solvers and other components used by SymbiYosys come with their own license terms. There is some more details in the ["Selecting the right engine" section of the documentation](https://yosyshq.readthedocs.io/projects/sby/en/latest/quickstart.html#selecting-the-right-engine). +SBY itself is licensed under the ISC license, note that the solvers and other components used by SBY come with their own license terms. There is some more details in the ["Selecting the right engine" section of the documentation](https://yosyshq.readthedocs.io/projects/sby/en/latest/quickstart.html#selecting-the-right-engine). --- -SymbiYosys (sby) is part of the [Tabby CAD Suite](https://www.yosyshq.com/tabby-cad-datasheet) and the [OSS CAD Suite](https://github.com/YosysHQ/oss-cad-suite-build)! The easiest way to use sby is to install the binary software suite, which contains all required dependencies, including all supported solvers. +SBY is part of the [Tabby CAD Suite](https://www.yosyshq.com/tabby-cad-datasheet) and the [OSS CAD Suite](https://github.com/YosysHQ/oss-cad-suite-build)! The easiest way to use sby is to install the binary software suite, which contains all required dependencies, including all supported solvers. * [Contact YosysHQ](https://www.yosyshq.com/contact) for a [Tabby CAD Suite](https://www.yosyshq.com/tabby-cad-datasheet) Evaluation License and download link * OR go to https://github.com/YosysHQ/oss-cad-suite-build/releases to download the free OSS CAD Suite diff --git a/docs/Makefile b/docs/Makefile index b5a7167..7f1b57d 100644 --- a/docs/Makefile +++ b/docs/Makefile @@ -91,9 +91,9 @@ qthelp: @echo @echo "Build finished; now you can run "qcollectiongenerator" with the" \ ".qhcp project file in $(BUILDDIR)/qthelp, like this:" - @echo "# qcollectiongenerator $(BUILDDIR)/qthelp/SymbiYosys.qhcp" + @echo "# qcollectiongenerator $(BUILDDIR)/qthelp/SBY.qhcp" @echo "To view the help file:" - @echo "# assistant -collectionFile $(BUILDDIR)/qthelp/SymbiYosys.qhc" + @echo "# assistant -collectionFile $(BUILDDIR)/qthelp/SBY.qhc" .PHONY: applehelp applehelp: @@ -110,8 +110,8 @@ devhelp: @echo @echo "Build finished." @echo "To view the help file:" - @echo "# mkdir -p $$HOME/.local/share/devhelp/SymbiYosys" - @echo "# ln -s $(BUILDDIR)/devhelp $$HOME/.local/share/devhelp/SymbiYosys" + @echo "# mkdir -p $$HOME/.local/share/devhelp/SBY" + @echo "# ln -s $(BUILDDIR)/devhelp $$HOME/.local/share/devhelp/SBY" @echo "# devhelp" .PHONY: epub diff --git a/docs/source/index.rst b/docs/source/index.rst index ab67043..e4f6c3d 100644 --- a/docs/source/index.rst +++ b/docs/source/index.rst @@ -1,9 +1,9 @@ -SymbiYosys (sby) Documentation +SBY Documentation ============================== -SymbiYosys (sby) is a front-end driver program for Yosys-based formal -hardware verification flows. SymbiYosys provides flows for the following +SBY is a front-end driver program for Yosys-based formal +hardware verification flows. SBY provides flows for the following formal tasks: * Bounded verification of safety properties (assertions) diff --git a/docs/source/install.rst b/docs/source/install.rst index ad2075b..6c0c498 100644 --- a/docs/source/install.rst +++ b/docs/source/install.rst @@ -8,7 +8,7 @@ This document will guide you through the process of installing sby. CAD suite(s) ************ -Sby (SymbiYosys) is part of the `Tabby CAD Suite +Sby (SBY) is part of the `Tabby CAD Suite `_ and the `OSS CAD Suite `_! The easiest way to use sby is to install the binary software suite, which contains all required diff --git a/docs/source/license.rst b/docs/source/license.rst index 786dc59..0521751 100644 --- a/docs/source/license.rst +++ b/docs/source/license.rst @@ -1,12 +1,12 @@ -SymbiYosys license +SBY license ================== -SymbiYosys (sby) itself is licensed under the ISC license: +SBY itself is licensed under the ISC license: .. code-block:: text - SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows + SBY -- Front-end for Yosys-based formal verification flows Copyright (C) 2016 Claire Xenia Wolf @@ -22,6 +22,6 @@ SymbiYosys (sby) itself is licensed under the ISC license: ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. -Note that the solvers and other components used by SymbiYosys come with their +Note that the solvers and other components used by SBY come with their own license terms. diff --git a/docs/source/quickstart.rst b/docs/source/quickstart.rst index 0105dc6..b98e7bb 100644 --- a/docs/source/quickstart.rst +++ b/docs/source/quickstart.rst @@ -99,10 +99,10 @@ difference in addresses, and then compare with the count signal. :end-at: ; :dedent: -SymbiYosys +SBY ********** -SymbiYosys (sby) uses a .sby file to define a set of tasks used for +SBY uses a .sby file to define a set of tasks used for verification. **basic** diff --git a/docs/source/verilog.rst b/docs/source/verilog.rst index 457ac36..11a06de 100644 --- a/docs/source/verilog.rst +++ b/docs/source/verilog.rst @@ -3,7 +3,7 @@ Formal extensions to Verilog ============================ Any Verilog file may be read using ``read -formal `` within the -SymbiYosys ``script`` section. Multiple files may be given on the sames +SBY ``script`` section. Multiple files may be given on the sames line, or various files may be read in subsequent lines. ``read -formal`` will also define the ``FORMAL`` macro, which can be used @@ -28,7 +28,7 @@ example above. Refer to :doc:`verific` for more on the Verific front end. SystemVerilog Immediate Assertions ---------------------------------- -SymbiYosys supports three basic immediate assertion types. +SBY supports three basic immediate assertion types. 1. ``assume();`` @@ -39,15 +39,15 @@ SymbiYosys supports three basic immediate assertion types. 2. ``assert();`` An assertion is something the solver will try to make false. Any time - SymbiYosys is run with ``mode bmc``, the proof will fail if some set + SBY is run with ``mode bmc``, the proof will fail if some set of inputs can cause the ```` within the assertion to be zero (false). - When SymbiYosys is run with ``mode prove``, the proof may also yield an + When SBY is run with ``mode prove``, the proof may also yield an ``UNKNOWN`` result if an assertion can be made to fail during the induction step. 3. ``cover();`` - A cover statement only applies when SymbiYosys is ran with option + A cover statement only applies when SBY is ran with option ``mode cover``. In this case, the formal solver will start at the beginning of time (i.e. when all initial statements are true), and it will try to find some clock when ```` can be made to be true. Such a diff --git a/sbysrc/sby.py b/sbysrc/sby.py index 2d5a1da..e868f33 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -1,6 +1,6 @@ #!/usr/bin/env python3 # -# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows +# SBY -- Front-end for Yosys-based formal verification flows # # Copyright (C) 2016 Claire Xenia Wolf # diff --git a/sbysrc/sby_autotune.py b/sbysrc/sby_autotune.py index aa40134..b1b27dd 100644 --- a/sbysrc/sby_autotune.py +++ b/sbysrc/sby_autotune.py @@ -1,5 +1,5 @@ # -# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows +# SBY -- Front-end for Yosys-based formal verification flows # # Copyright (C) 2022 Jannis Harder # diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 7a67cd3..971104d 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -1,5 +1,5 @@ # -# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows +# SBY -- Front-end for Yosys-based formal verification flows # # Copyright (C) 2016 Claire Xenia Wolf # diff --git a/sbysrc/sby_design.py b/sbysrc/sby_design.py index 234e7f8..151f714 100644 --- a/sbysrc/sby_design.py +++ b/sbysrc/sby_design.py @@ -1,5 +1,5 @@ # -# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows +# SBY -- Front-end for Yosys-based formal verification flows # # Copyright (C) 2022 N. Engelhardt # diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py index 42dbd0a..10b54c8 100644 --- a/sbysrc/sby_engine_abc.py +++ b/sbysrc/sby_engine_abc.py @@ -1,5 +1,5 @@ # -# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows +# SBY -- Front-end for Yosys-based formal verification flows # # Copyright (C) 2016 Claire Xenia Wolf # diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index 72add92..011e33d 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -1,5 +1,5 @@ # -# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows +# SBY -- Front-end for Yosys-based formal verification flows # # Copyright (C) 2016 Claire Xenia Wolf # diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index b938397..58ead87 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -1,5 +1,5 @@ # -# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows +# SBY -- Front-end for Yosys-based formal verification flows # # Copyright (C) 2016 Claire Xenia Wolf # diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index 0364929..2da731e 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -1,5 +1,5 @@ # -# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows +# SBY -- Front-end for Yosys-based formal verification flows # # Copyright (C) 2016 Claire Xenia Wolf # diff --git a/sbysrc/sby_jobserver.py b/sbysrc/sby_jobserver.py index 57d751d..67d61bf 100644 --- a/sbysrc/sby_jobserver.py +++ b/sbysrc/sby_jobserver.py @@ -1,5 +1,5 @@ # -# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows +# SBY -- Front-end for Yosys-based formal verification flows # # Copyright (C) 2022 Jannis Harder # diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py index 173812f..0969e64 100644 --- a/sbysrc/sby_mode_bmc.py +++ b/sbysrc/sby_mode_bmc.py @@ -1,5 +1,5 @@ # -# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows +# SBY -- Front-end for Yosys-based formal verification flows # # Copyright (C) 2016 Claire Xenia Wolf # diff --git a/sbysrc/sby_mode_cover.py b/sbysrc/sby_mode_cover.py index c94c639..4cee958 100644 --- a/sbysrc/sby_mode_cover.py +++ b/sbysrc/sby_mode_cover.py @@ -1,5 +1,5 @@ # -# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows +# SBY -- Front-end for Yosys-based formal verification flows # # Copyright (C) 2016 Claire Xenia Wolf # diff --git a/sbysrc/sby_mode_live.py b/sbysrc/sby_mode_live.py index 89bcc57..7d21b38 100644 --- a/sbysrc/sby_mode_live.py +++ b/sbysrc/sby_mode_live.py @@ -1,5 +1,5 @@ # -# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows +# SBY -- Front-end for Yosys-based formal verification flows # # Copyright (C) 2016 Claire Xenia Wolf # diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py index e50fbfd..0f71bff 100644 --- a/sbysrc/sby_mode_prove.py +++ b/sbysrc/sby_mode_prove.py @@ -1,5 +1,5 @@ # -# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows +# SBY -- Front-end for Yosys-based formal verification flows # # Copyright (C) 2016 Claire Xenia Wolf # diff --git a/sbysrc/sby_sim.py b/sbysrc/sby_sim.py index 32789fb..cf2af73 100644 --- a/sbysrc/sby_sim.py +++ b/sbysrc/sby_sim.py @@ -1,5 +1,5 @@ # -# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows +# SBY -- Front-end for Yosys-based formal verification flows # # Copyright (C) 2022 Jannis Harder #