Verified high-level synthesis in BEDROC

Author

Chapman, Richard ; Brown, Geoffrey ; Leeser, Miriam

Author_Institution

Dept. of Comput. Sci., Cornell Univ., Ithaca, NY, USA

fYear

1992

fDate

16-19 Mar 1992

Firstpage

59

Lastpage

63

Abstract

The authors present the HardwarePal hardware description language and formal operational and denotational semantics for it, briefly discussing their proof of the two semantics´ equivalence. They then discuss their intermediate representation, dependence flow graphs, and the operational semantics of DFG. They describe the translation from HardwarePal to dependence flow graphs and outline their proof that this translation preserves the meaning of the initial HardwarePal program. The authors discuss proving the correctness of the translation from behavioral specification to intermediate form, proving the correctness of optimizations, and plans for proving the correctness of scheduling. The authors conclude by discussing their plans for proofs that register-transfer level design produced by BEDROC implements the dependence flow graph

Keywords

circuit analysis computing; formal verification; logic CAD; logic testing; specification languages; BEDROC; HardwarePal; behavioral specification; correctness proving; denotational semantics; dependence flow graphs; hardware description language; high level synthesis verification; register-transfer level design; Algorithm design and analysis; Circuit synthesis; Computer science; Design optimization; Flow graphs; Hardware; High level synthesis; Silicon compiler; Specification languages; Tree graphs;

fLanguage

English

Publisher

ieee

Conference_Titel

Design Automation, 1992. Proceedings., [3rd] European Conference on

Conference_Location

Brussels

Print_ISBN

0-8186-2645-3

Type

conf

DOI

10.1109/EDAC.1992.205894

Filename

205894