Computing functional properties and network flexibilities for logic synthesis and verification
Malgorzata Chrzanowska-Jeske, Jin Song Zhang · 2006
Logic synthesis is a process of converting a given Register Transfer Level (RTL) description into an optimized gate-level netlist implemented using cells in a target technology library while meeting the area, speed and testability requirements. Logic verification ensures the correctness of the original design and that the transformations occurred during logic synthesis do not alter the design behavior. Properties of Boolean functions have long been exploited both in logic synthesis and verification to simplify the design representations, improve the quality of results, and reduce the runtime of these applications. The research in this area often have two orthogonal directions: (1) To discover new functional properties and demonstrate their applications in logic synthesis and verification; (2) To improve the computational efficiency of existing properties so that computational demands can keep pace with the ever increasing design sizes. Part I of this thesis includes research conducted in both directions: (1) A functional property called Linear cofactor relationship (LCR) is formalized and its usefulness is demonstrated through several applications. A recursive BDD-based procedure is proposed to compute LCRs efficiently. (2) Improved computations of several other properties often used in logic synthesis and verification are presented. The properties include classical symmetries, autosymmetry and unateness. The proposed algorithms advance the state-of-the-art of these computations, and therefore, making these functional properties more applicable in logic synthesis and verification applications. Flexibilities in a Boolean network are often exploited during logic synthesis and resynthesis to make local structural changes to the netlist, while maintaining the global functionality of the circuit. Several formalisms have been proposed to express the flexibilities of Boolean networks, most of which require extensive computing. In part II of the thesis, efficient algorithms to compute two forms of flexibilities, i.e. Sets of Pairs of Functions to Be Distinguished (SPFD) and node resubstitution, are proposed. The improvement in their computations will make them applicable in real design optimization.