mirror of https://github.com/YosysHQ/yosys.git
efa278e232
The initial list of hits was generated with the codespell command
below, and each hit was evaluated and fixed manually while taking
context into consideration.
DIRS="kernel/ frontends/ backends/ passes/ techlibs/"
DIRS="${DIRS} libs/ezsat/ libs/subcircuit"
codespell $DIRS -S *.o -L upto,iff,thru,synopsys,uint
More hits were found by looking through comments and strings manually.
|
||
|---|---|---|
| .. | ||
| Makefile.inc | ||
| README | ||
| example.sby | ||
| example.sv | ||
| verific.cc | ||
| verific.h | ||
| verificsva.cc | ||
README
This directory contains Verific bindings for Yosys. See http://www.verific.com/ for details. Building Yosys with the 32 bit Verific eval library on amd64: ============================================================= 1.) Use a Makefile.conf like the following one: --snip-- CONFIG := gcc ENABLE_TCL := 0 ENABLE_PLUGINS := 0 ENABLE_VERIFIC := 1 CXXFLAGS += -m32 LDFLAGS += -m32 VERIFIC_DIR = /usr/local/src/verific_lib_eval --snap-- 2.) Install the necessary multilib packages Hint: On debian/ubuntu the multilib packages have names such as libreadline-dev:i386 or lib32readline6-dev, depending on the exact version of debian/ubuntu you are working with. 3.) Build and test make -j8 ./yosys -p 'verific -sv frontends/verific/example.sv; verific -import top' Verific Features that should be enabled in your Verific library =============================================================== database/DBCompileFlags.h: DB_PRESERVE_INITIAL_VALUE Testing Verific+Yosys+SymbiYosys for formal verification ======================================================== Install Yosys+Verific, SymbiYosys, and Yices2. Install instructions: http://symbiyosys.readthedocs.io/en/latest/quickstart.html#installing Then run in the following command in this directory: sby -f example.sby This will generate approximately one page of text outpout. The last lines should be something like this: SBY [example] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0) SBY [example] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0) SBY [example] summary: engine_0 (smtbmc yices) returned PASS for basecase SBY [example] summary: engine_0 (smtbmc yices) returned PASS for induction SBY [example] summary: successful proof by k-induction. SBY [example] DONE (PASS, rc=0)