VERIFIABLE HARDWARE SYNTHESIS

Authors
  1. Hammerlindl, J.B.
  2. Girczyc, E.F.
Corporate Authors
Audesyn Inc, Edmonton ALTA (CAN);Chief of Research and Development, Ottawa ONT (CAN) Director of Research and Development Communications and Space
Abstract
We have investigated two areas: (a) the analogies between production-based hardware synthesis and theorem proving; and (b) the analogies between production-based hardware synthesis and function preserving transformations on databases. Our objective was to identify methods for the verifiability of hardware synthesis. The report describes two analogies between a production-based synthesis system like Elf and a theorem-prover, namely the kernel analogy and the constructive analogy. The Kernel analogy is based on the resemblance of productions to theorems and the similarities between applying a production and rewriting with a theorem. We state the constructive analogy as follows: Using a production-based synthesis system to design hardware is like using a therorem-prover to develop a constructive proof of an existential conjecture. Specifically, by designing an implementation that realizes the given specification, Elf shows that such an implementation exists. TRUNCATED
Report Number
AUTR-89-06 — Technical Report; Contractor Report; See also AUTR-89-06 (DSIS 90-01276) which is a different descriptive report
Date of publication
15 Mar 1989
Number of Pages
65
DSTKIM No
90-01283
CANDIS No
63553
Format(s):
Hardcopy;Originator's fiche received by DSIS

Permanent link

Document 1 of 1

Date modified: