SYNTHESIS OF DIGITAL DESIGNS BY EQUIVALENCE TRANSFORMATIONS.

A method of design using automated logic and provably correct arithmetic transformations of inputs to arithmetically equivalent outputs is proposed. This approach starts with a functional-level description and produces a network interconnection list of macrocells at the gate and register level. The netlist output corresponds to the netlists used by various netlist comparison checkers or could serve as input to a silicon compiler. The novelty and importance of the approach is its use of logic, arithmetic rules, and logic programming to describe and document the synthesis process so that the design is provably correct.