Title :
Verified high-level synthesis in BEDROC
Author :
Chapman, Richard ; Brown, Geoffrey ; Leeser, Miriam
Author_Institution :
Dept. of Comput. Sci., Cornell Univ., Ithaca, NY, USA
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;
Conference_Titel :
Design Automation, 1992. Proceedings., [3rd] European Conference on
Conference_Location :
Brussels
Print_ISBN :
0-8186-2645-3
DOI :
10.1109/EDAC.1992.205894
