2 Bit Adder

Next: Inductive Interference Up: Some SAT Benchmarks Visualised Previous: Some SAT Benchmarks Visualised

2 Bit Adder

VLSI design of a 2 bit adder, from the Beijing benchmark suite, problem 2bitadd_10.cnf. Under various graph interpretations, the hardware verification problems have significant structural properties that suggests modularity and repetition. This suggests that there maybe something for a search algorithm to exploit, possibly using partitioning and unification techniques.

**Figure 1:** 2 Bit Adder, Cooccurrence of Variables
$\begin{figure}\par\epsfig{figure=images/2bitadd_10_vco,width={1.4\textwidth}} \end{figure}$

**Figure 2:** 2 Bit Adder, Cooccurrence of Literals
$\begin{figure}\epsfig{figure=images/2bitadd_10_lco,width=\textwidth} \end{figure}$

**Figure 3:** 2 Bit Adder, Basic Implicative Interpretation
$\begin{figure}\epsfig{figure=images/2bitadd_10_imp,width=\textwidth} \end{figure}$

Last modified: 2004-03-17
Andrew Slater