Description
Problem 1: You design a combinational circuit C1 with the following requirements. The combinational
logic C1 should contain at least 8 gates which include at least 3 OR and 3 NAND gates. Make sure
that your design be different from those used by other students. If your design is identical to the one
used by other students, further investigation will be conducted and you will be asked to revise your
design and redo the work.
Task 1:
1) Draw your circuit C1.
2) You make an identical copy of C1 and name it as C2. Except the inputs, add the index 1 to all the
wire names of C1, while adding the index 2 to all the wire names of C2. Assume that the
corresponding inputs use the same variable names, respectively.
3) Download a SAT solver for satisfiability.
4) Prove the equivalence of C1 and C2 by a SAT solver.
Task 2:
Get a circuit C3 from C2 by replacing one gate in C2 with a gate of different functionality. Prove or
disprove C1=C3 by a SAT solver.
Problem 2. Equivalence checking by implicit state enumeration.
Consider the product machine with shared input P=S1S2 in your project 2. Following the lecture on
implicit state enumeration, use the implicit state enumeration to check the equivalence of S1 and S2.
The initial states of FFs in both circuits are all the equivalent states. Use the Boolean algebra to do the
reasoning.
