Digital Circuit Evolution Using SAT Solver (Evolvable Hardware)

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.