VERIFIABLE HARDWARE SYNTHESIS
- Authors
- 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
Document 1 of 1
- Date modified: