Methodology and apparatus for modular partitioning for the machine design of asynchronous circuits

摘要

A machine methodology for designing asynchronous circuits utilizes a modular approach for the synthesis of asynchronous circuits from signal transition graphs, partitions the signal transition graph into a number of simpler and more manageable modules. Each modular graph is then individually solved. The results of the small graphs are then integrated together to provide a solution to the asynchronous circuit design problem as defined by a given asynchronous behavioral specification. A satisfiability solver for Boolean output function utilizing a binary decision diagram is incorporated in one embodiment which is comprised of a structural SAT formula preprocessor and a complete, incremental SAT processor which is specifically designed to find an optimal solution. The preprocessor compresses a large size SAT formula representing a circuit into a number of smaller SAT formulas. Each small size SAT formula is then solved by the BDD SAT processor. The results of these subsolutions are then integrated together to contribute to the solution of the original larger design problem.