Research Paper #557
|Synthesizing Hardware: Configuration Via Proof
|Submitted to CADE-92
|Configuring large computer hardware systems is a complex task and efforts to automate it have spawned knowledge based systems which have proved difficult to maintain. This paper describes a logical formalism for configuration and the use of a proofs as configurations approach analogous to program synthesis via proofs as programs. Meta-level control is achieved through proof plans, which embody common strategies for guiding inference. As well as ensuring soundness, in that only legal configurations can be synthesized, the system also facilitates maintenance because of its clean separation of object-level knowledge, heuristics, and control strategies.
|NO ONLINE COPY