Synthesis of digital designs by equivalence transformations (hardware, computer-aided design)
Shiu‐Kai Chin · 1986
Computer-aided design tools have progressed to the point where circuit and layout related mistakes will largely be eliminated when designing very large scale integrated (VLSI) circuits. Specifically, the use of network comparison checkers and design rule checkers will insure that layouts and logic schematics are consistent and that layouts are free of design rule errors. Consequently, many, if not all of the errors present in the design of VLSI systems will be introduced at the logic level or higher. Typically, simulation has been the primary tool used to validate logic designs. However, because of the increasing complexity of VLSI logic designs, in practice it is almost impossible to check every detail of every connection by exhaustive simulation. A method of design using automated logic and provably correct arithmetic transformations of inputs to arithmetically equivalent outputs is proposed. This method starts with an arithmetic specification and produces correct and practical designs. This design method is demonstrated by synthesizing several combinational array multipliers, several bit-serial multipliers, and two word-serial multipliers. A set of hardware corresponding to various arithmetic operations that preserve the arithmetic value of the input and output terms, and various logical rules to select each operation is defined. The logic programming language PROLOG is used to actually execute the rules. By applying the rules for each design, the existence of a design is deduced, and the network interconnection list (netlist) of hardware is produced as an artifact. The advantage of this approach is that since only equivalence-preserving transformations are used, and since the logical rules are logically selected as part of the PROLOG interpretter, only functionally correct designs will result.