Checking for combinational equivalence in circuits

摘要

A binary system has a facility to check for equivalence between a pair of combinational circuits. The process is based upon the use of binary decision diagrams (BDD) with integrated satisfiability (SAT) checking. The switching system is divided (20) into input (30) and an output section (40). Independent claims are provided for a computer system and computer program product.