Abstract:
Evolutionary computation uses Darwinian principles to find solutions from a given search
space and forms the basis for evolving digital circuits. One of the most computationally
expensive steps in evolutionary computation is the comparison of the candidate circuit
(chromosome) with the target truth table. We propose to use SAT (satisfiability) solvers
to improve upon the efficiency of this process, which is traditionally done using exhaustive
simulation. However, traditional SAT solvers, which return the satisfiability of a boolean
expression in Yes/No format, cannot be used in this context since we need the percentage
(score) of equivalence between two circuits. This thesis presents a SAT solver that
fulfills this requirement. We use this novel SAT solver to develop a digital circuit evolution
methodology based on the principles of Cartesian Genetic Programming (CGP). The
proposed methodology performs exceptionally well for circuits whose behavior can be expressed
compactly in terms of CNF (Conjunctive Normal Form) clauses. For illustration
purposes, the proposed methodology has been used to evolve digital circuits exhibiting the
behaviors of adders, multipliers, muxes, encoders, even parity circuits and a few LGSynth91
benchmarks.
