You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 

9 lines
647 B

Let $C_1$ and $C_2$ denote the two combinational circuits.
In order to check whether $C_1$ and $C_2$ are equivalent, one has to perform the following steps:
\begin{enumerate}
\item Encode $C_1$ and $C_2$ into two propositional formulas $\varphi_1$ and $\varphi_2$.
\item Compute the Conjunctive Normal Form (CNF) of $\varphi_1 \oplus \varphi_2$,
using Tseitin encoding; i.e., $CNF(\varphi_1 \oplus \varphi_2)$.
\item Give the formula $CNF(\varphi_1 \oplus \varphi_2)$ to a SAT solver and check for satisfiability.
\item $C_1$ and $C_2$ are equivalent if and only if $CNF(\varphi_1 \oplus \varphi_2)$ is UNSAT.
\end{enumerate}