diff options
Diffstat (limited to 'manual/APPNOTE_011_Design_Investigation.tex')
| -rw-r--r-- | manual/APPNOTE_011_Design_Investigation.tex | 154 |
1 files changed, 152 insertions, 2 deletions
diff --git a/manual/APPNOTE_011_Design_Investigation.tex b/manual/APPNOTE_011_Design_Investigation.tex index fb55c1ecb..1f5b9d382 100644 --- a/manual/APPNOTE_011_Design_Investigation.tex +++ b/manual/APPNOTE_011_Design_Investigation.tex @@ -738,7 +738,7 @@ The {\tt -table} option can be used to create a truth table. For example: \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 @@ -756,9 +756,151 @@ The {\tt -table} option can be used to create a truth table. For example: \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} @@ -786,6 +928,14 @@ Lecture Notes in Electrical Engineering. Volume 265, 2014, pp 201-221.\/} 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} |