Progress on AppNote 011

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}

manual/APPNOTE_011_Design_Investigation/primetest.v

@@ -0,0 +1,4 @@
+module primetest(p, a, b, ok);
+input [15:0] p, a, b;
+output ok = p != a*b || a == 1 || b == 1;
+endmodule