Paper Info
Title
A study about the efficiency of formal high-level synthesis applied to verification
Abstract
The use of a formal synthesis system is proposed as an efficient alternative for the formal verification of RT-level circuits obtained from algorithmic-level specifications by high-level synthesis (HLS) tools. The goal of the proposal is to recreate, within the formal synthesis system, any design process performed by an external HLS tool in order to check its correctness. The mean is the utilization of the post-synthesis reports given by HLS tools to guide the derivation process into the formal synthesis system. The paper places particular emphasis in two aspects: to give a comprehensive vision of the formal scenario, and to demonstrate its practical viability. In relation with the former aspect, the methodology is detailed and the architecture of the whole system is summarized (including specification mechanisms, derivation rules, HLS tasks formalization, automated derivation procedure, etc.). With respect to the latter one, a theoretical study (confirmed by a set of experiments) shows that the formal derivation process has quadratic and linear complexity in terms of time and memory consumption, respectively. Finally, the paper concludes that following the proposal, even commercial HLS processes can be verified with a reduced overhead (5% in average) without modifying the HLS tools.
Year
DOI
Venue
2002
10.1016/S0167-9260(02)00021-4
Integration
Keywords
Field
DocType
High-level synthesis,RT-level formal verification,Formal synthesis,Joint design and verification cycle,Formal verification overhead
Formal equivalence checking,Computer science,Correctness,High-level synthesis,Formal specification,Real-time computing,Program derivation,Formal methods,High-level verification,Formal verification
Journal
Volume
Issue
ISSN
31
2
0167-9260
Citations 
PageRank 
References 
0
0.34
6
Authors
3
Name
Order
Citations
PageRank
J. M. Mendias11219.25
Román Hermida28915.34
Olga Peñalba321.47