mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-08-27 21:48:58 +00:00
Code Activity

Spell check (by Larry Doolittle)

Browse source
This commit is contained in:
Clifford Wolf 2015-08-14 10:56:05 +02:00
parent 80910d13a6
commit 84bf862f7c
63 changed files with 220 additions and 220 deletions
Download patch file Download diff file Expand all files Collapse all files

8
manual/PRESENTATION_ExOth.tex
View file

@ -34,7 +34,7 @@ are connected.
\item
Commands such as {\tt submod}, {\tt expose}, {\tt splice}, \dots can be used
to transform the design into an equivialent design that is easier to analyse.
to transform the design into an equivalent design that is easier to analyse.
\item
Commands such as {\tt eval} and {\tt sat} can be used to investigate the
@ -102,7 +102,7 @@ Symbolic Model Checking (SMC) is used to formally prove that a circuit has
(or has not) a given property.
\bigskip
One appliction is Formal Equivalence Checking: Proving that two circuits
One application is Formal Equivalence Checking: Proving that two circuits
are identical. For example this is a very useful feature when debugging custom
passes in Yosys.
@ -143,11 +143,11 @@ rename test test_mapped
# apply the techmap only to test_mapped
techmap -map techmap_01_map.v test_mapped
# create a miter circuit to test equivialence
# create a miter circuit to test equivalence
miter -equiv -make_assert -make_outputs test_orig test_mapped miter
flatten miter
# run equivialence check
# run equivalence check
sat -verify -prove-asserts -show-inputs -show-outputs miter
\end{lstlisting}