Automated Design of Circuits from Recursion Equations Using Theorem‐Proving Technique

AbstractThis paper aims at establishing the automated design for a circuit by the theorem‐proving technique, by formulating the circuit design as a transformation from the specification description (recursion equation) to the circuit model FN (functional network based on dataflow operation).First, rules for circuit construction and transformation rules are formulated, which are used as the inference knowledge in the theorem‐proving system. Then the circuit realization language is designed based on the modal logic, where the syntax corresponds to the FN structure, and the computation corresponds to the circuit operation. It is shown that the processing system for such a language can be realized by a technique similar to the derivation principle for the first‐order predicate logic.The theorem‐proving system for automated circuit design can be realized as a program on the circuit realization language, where the element composing the circuit is used as the declarative knowledge, and the transformation rule is used as the inference knowledge.When the design specification (recursion equation) is given as the goal clause, the automated circuit design system decides on the possibility of design, and the circuit structure information is extracted from the proof process. The behavior of the circuit can be simulated also in the process.