Automated representation changing for problem solving and electronic CAD

摘要

Structured top-down design can be viewed as a process of iterative step-wise representation changes wherein an initial specification passes through several levels of increasingly concrete representations. When viewed this way, many of the goals and difficulties of hardware CAD are strikingly similar to those addressed by the branch of AI problem solving known as `Problem Reformulation.' Our principal aim is to provide a common mathematical setting to the two disciplines and then to exploit problem reformulation results in the design and implementation of a CAD system that can reason about VLSI design as representational change. The CAD system builds on one that has a proof assistant at its core, so that circuits designed in the system are pre-verified. High-level design knowledge is captured by algebraic models; refinement transformations between levels and optimizing and partitioning functions within a level are algebraic homomorphisms. The use of algebra throughout allows us to add different kinds and levels of reasoning to the theorem prover without a loss of mathematical soundness. The formalization of the `design as representation change' idea involves bringing together various strands in abstract algebra, artificial intelligence, and formal methods for system design. In this paper we describe the algebraic background and give examples and results of this kind of analysis in artificial intelligence and multi-layered hardware description.