diff --git a/CHANGELOG b/CHANGELOG index 372a59d58..a9b0b6591 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1229,7 +1229,7 @@ Yosys 0.7 .. Yosys 0.8 - Added "write_smt2 -stbv" and "write_smt2 -stdt" - Fix equiv_simple, old behavior now available with "equiv_simple -short" - Change to Yices2 as default SMT solver (it is GPL now) - - Added "yosys-smtbmc --presat" (now default in SymbiYosys) + - Added "yosys-smtbmc --presat" (now default in SBY) - Added "yosys-smtbmc --smtc-init --smtc-top --noinit" - Added a brand new "write_btor" command for BTOR2 - Added clk2fflogic memory support and other improvements diff --git a/frontends/verific/README b/frontends/verific/README index 921873af3..931dd2f30 100644 --- a/frontends/verific/README +++ b/frontends/verific/README @@ -15,10 +15,10 @@ database/DBCompileFlags.h: DB_PRESERVE_INITIAL_VALUE -Testing Verific+Yosys+SymbiYosys for formal verification +Testing Verific+Yosys+SBY for formal verification ======================================================== -Install Yosys+Verific, SymbiYosys, and Yices2. Install instructions: +Install Yosys+Verific, SBY, and Yices2. Install instructions: http://symbiyosys.readthedocs.io/en/latest/quickstart.html#installing Then run in the following command in this directory: diff --git a/frontends/verific/example.sby b/frontends/verific/example.sby index ffbf33cab..69d56d2dd 100644 --- a/frontends/verific/example.sby +++ b/frontends/verific/example.sby @@ -1,4 +1,4 @@ -# Simple SymbiYosys example job utilizing Verific +# Simple SBY example job utilizing Verific [options] mode prove