\begin{verbatim}
yosys [selstage]> eval -set-undef -set d[3:1] 0 -table s1,d[0]
- 15. Executing EVAL pass (evaluate the circuit given an input).
+ 10. Executing EVAL pass (evaluate the circuit given an input).
Full command line: eval -set-undef -set d[3:1] 0 -table s1,d[0]
\s1 \d [0] | \n1 \n2
\end{verbatim}
}
+Note that the {\tt eval} command (as well as the {\tt sat} command discussed in
+the next sections) does only operate on flattened modules. It can not analyze
+signals that are passed through design hierarchy levels. So the {\tt flatten}
+command must be used on modules that instantiate other modules before this
+commands can be applied.
+
\subsection{Solving combinatorial SAT problems}
-\FIXME
+\begin{figure}[b]
+\lstinputlisting{APPNOTE_011_Design_Investigation/primetest.v}
+\caption{A simple miter circuit for testing if a number is prime}
+\label{primetest}
+\end{figure}
+
+\begin{figure*}[!t]
+\begin{lstlisting}[basicstyle=\ttfamily\small]
+yosys [primetest]> sat -prove ok 1 -set p 31
+
+8. Executing SAT pass (solving SAT problems in the circuit).
+Full command line: sat -prove ok 1 -set p 31
+
+Setting up SAT problem:
+Import set-constraint: \p = 16'0000000000011111
+Final constraint equation: \p = 16'0000000000011111
+Imported 6 cells to SAT database.
+Import proof-constraint: \ok = 1'1
+Final proof equation: \ok = 1'1
+
+Solving problem with 2790 variables and 8241 clauses..
+SAT proof finished - model found: FAIL!
+
+ ______ ___ ___ _ _ _ _
+ (_____ \ / __) / __) (_) | | | |
+ _____) )___ ___ ___ _| |__ _| |__ _____ _| | _____ __| | |
+ | ____/ ___) _ \ / _ (_ __) (_ __|____ | | || ___ |/ _ |_|
+ | | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_
+ |_| |_| \___/ \___/ |_| |_| \_____|_|\_)_____)\____|_|
+
+
+ Signal Name Dec Hex Bin
+ -------------------- ---------- ---------- ---------------------
+ \a 15029 3ab5 0011101010110101
+ \b 4099 1003 0001000000000011
+ \ok 0 0 0
+ \p 31 1f 0000000000011111
+
+yosys [primetest]> sat -prove ok 1 -set p 31 -set a[15:8],b[15:8] 0
+
+9. Executing SAT pass (solving SAT problems in the circuit).
+Full command line: sat -prove ok 1 -set p 31 -set a[15:8],b[15:8] 0
+
+Setting up SAT problem:
+Import set-constraint: \p = 16'0000000000011111
+Import set-constraint: { \a [15:8] \b [15:8] } = 16'0000000000000000
+Final constraint equation: { \a [15:8] \b [15:8] \p } = { 16'0000000000000000 16'0000000000011111 }
+Imported 6 cells to SAT database.
+Import proof-constraint: \ok = 1'1
+Final proof equation: \ok = 1'1
+
+Solving problem with 2790 variables and 8257 clauses..
+SAT proof finished - no model found: SUCCESS!
+
+ /$$$$$$ /$$$$$$$$ /$$$$$$$
+ /$$__ $$ | $$_____/ | $$__ $$
+ | $$ \ $$ | $$ | $$ \ $$
+ | $$ | $$ | $$$$$ | $$ | $$
+ | $$ | $$ | $$__/ | $$ | $$
+ | $$/$$ $$ | $$ | $$ | $$
+ | $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$
+ \____ $$$|__/|________/|__/|_______/|__/
+ \__/
+\end{lstlisting}
+\caption{Experiments with the miter circuit from Fig.~\ref{primetest}. The first attempt of proving that 31
+is prime failed because the SAT solver found a creative way of factorizing 31 using integer overflow.}
+\label{primesat}
+\end{figure*}
+
+Often the opposite of the {\tt eval} command is needed, i.e. the circuits
+output is given and we want to find the matching input signals. For small
+circuits with only a few input bits this can be accomplished by trying all
+possible input combinations, as it is done by the {\tt eval -table} command.
+For larger circuits however, Yosys provides the {\tt sat} command that uses
+a SAT \cite{CircuitSAT} solver \cite{MiniSAT} to solve this kind of problems.
+
+The {\tt sat} command works very similar to the {\tt eval} command. The main
+difference is that it is now also possible to set output values and find the
+corresponding input values. For Example:
+
+{\scriptsize
+\begin{verbatim}
+ yosys [selstage]> sat -show s1,s2,d -set s1 s2 -set n2,n1 4'b1001
+
+ 11. Executing SAT pass (solving SAT problems in the circuit).
+ Full command line: sat -show s1,s2,d -set s1 s2 -set n2,n1 4'b1001
+
+ Setting up SAT problem:
+ Import set-constraint: \s1 = \s2
+ Import set-constraint: { \n2 \n1 } = 4'1001
+ Final constraint equation: { \n2 \n1 \s1 } = { 4'1001 \s2 }
+ Imported 3 cells to SAT database.
+ Import show expression: { \s1 \s2 \d }
+
+ Solving problem with 81 variables and 207 clauses..
+ SAT solving finished - model found:
+
+ Signal Name Dec Hex Bin
+ -------------------- ---------- ---------- ---------------
+ \d 9 9 1001
+ \s1 0 0 00
+ \s2 0 0 00
+\end{verbatim}
+}
+
+Note that the {\tt sat} command support signal names in both arguments
+to the {\tt -set} option. In the above example we used {\tt -set s1 s2}
+to constraint {\tt s1} and {\tt s2} to be equal. When more complex
+constraints are needed, a wrapper circuit must be constructed that
+checks the constraints and signals if the constraint was met using an
+extra output port, which then can be forced to a value using the {\tt
+-set} option. (Such a circuit that contains the circuit under test
+plus additional constraint checking circuitry is called a {\tt miter\/}
+circuit.)
+
+Fig.~\ref{primetest} shows a miter circuit that is supposed to be used as a
+prime number test. If {\tt ok} is 1 for all input values {\tt a} and {\tt b}
+for a given {\tt p}, then {\tt p} is prime, or at least that is the idea.
+
+The Yosys shell session shown in Fig.~\ref{primesat} demonstrate that SAT
+solvers can even find the unexpected solutions to a problem: Using integer
+overflow there actually is a way of "`factorizing"' 31. A solution would of
+course be to perform the test in 32 bits, for example by replacing {\tt
+p != a*b} in the miter with {\tt p != \{16'd0,a\}*b}. But as 31 fits well into
+8 bits, we can also simply force the upper 8 bits of {\tt a} and {\tt b}
+to zero, as is done in the second command in Fig.~\ref{primesat}.
+
+The {\tt -prove} option used in this example works similar to {\tt -set}, but
+tries to find a case in which the two arguments are not equal. If such a case is
+not found, the property proven to hold for all inputs that satisfy the other
+constraints.
+
+It might be worth noting, that SAT solvers are not particularly efficient at
+factorizing large numbers. But if a small factorization problem occurs as
+part of a larger circuit problem, the Yosys SAT solver is perfectly capable
+of solving it. This can, for example, be an issue when using SAT solvers
+to prove the correct behavior of ALU circuits.
\subsection{Solving sequential SAT problems}
Graphviz - Graph Visualization Software.
\url{http://www.graphviz.org/}
+\bibitem{CircuitSAT}
+{\it Circuit satisfiability problem} on Wikipedia
+\url{http://en.wikipedia.org/wiki/Circuit_satisfiability}
+
+\bibitem{MiniSAT}
+MiniSat minimalistic, open-source SAT solver.
+\url{http://minisat.se/}
+
\end{thebibliography}
\end{document}
projects / yosys.git / commitdiff