Name
Abstract | ||
|---|---|---|
We propose a formal framework based on higher order logic theorem proving as a support for high level synthesis. We suppose that the design process starts from a behavioural or functional specification in terms of a VHDL description. It produces a structural description at the register transfer level. We propose a method for proving the correctness of synthesis results combining the advantages of presynthesis and postsynthesis verification. To perform the postsynthesis task automatically and efficiently correctness-implying properties of an intermediate synthesis result are checked. |
Year | DOI | Venue |
|---|---|---|
1998 | 10.1007/3-540-49519-3_16 | FMCAD |
Keywords | Field | DocType |
postsynthesis task,correctness-implying property,intermediate synthesis result,design process,combined formal post,high level synthesis,structural description,vhdl description,presynthesis verification,synthesis result,register transfer level,postsynthesis verification,higher order logic,theorem proving | Specification language,Computer science,High-level synthesis,Correctness,Automated theorem proving,Formal specification,Theoretical computer science,Register-transfer level,High-level verification,Functional specification | Conference |
ISBN | Citations | PageRank |
3-540-65191-8 | 1 | 0.40 |
References | Authors | |
15 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Thomas Lock | 1 | 1 | 1.08 |
| Michael Mendler | 2 | 314 | 34.60 |
| Matthias Mutz | 3 | 5 | 3.38 |