Abstract | ||
---|---|---|
The paper investigates the problem of designing high level synthesizers which would guarantee correctness of the designs produced. No satisfactory solution to this problem had been available so far. The paper presents a formal framework in which the synthesis and verification processes can be modelled in a practical way. It is shown that the complexity of the verification process can be reduced by following the modularity usually present in a synthesizer design. To simplify the correctness proof of the individual synthesis steps, some easily verifiable templates are defined, in which the algorithms can be expressed. The methodology is embedded in HOL (Higher Order Logic) system. |
Year | DOI | Venue |
---|---|---|
1995 | 10.1109/ICVD.1995.512118 | VLSI Design |
Keywords | Field | DocType |
verifiable template,individual synthesis step,higher order logic,synthesizer design,high level synthesizers,correct high level synthesizers,verification process,satisfactory solution,formal framework,correctness proof,modularity,scheduling,logic circuits,high level synthesis,formal logic,hardware,formal verification,logic design,very large scale integration | Logic synthesis,HOL,Computer science,Correctness,High-level synthesis,Real-time computing,Very-large-scale integration,Modularity,Higher-order logic,Formal verification | Conference |
ISBN | Citations | PageRank |
0-8186-6905-5 | 0 | 0.34 |
References | Authors | |
3 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
B. M. Subraya | 1 | 32 | 3.06 |
A. Kumar | 2 | 67 | 16.56 |
S. Kumar | 3 | 257 | 28.32 |