Efficient verification of scheduling, allocation and binding in high-level synthesis

This paper presents an efficient method to solve an important aspect of the high-level verification problem: the formal verification of RT-level implementations (datapath + controller), obtained from algorithmic-level specifications by high-level synthesis tools. The method consists in replicating external, and potentially incorrect, design processes within a mathematical framework, giving as a result the proof of correctness or the set of design decisions that led to errors. As the computational complexity is a major problem informal verification, the formal framework is based in an ad hoc formal theory. The moderate complexity achieved, has been confirmed by a detailed experimental study, which shows that our method can verify complex designs overloading the highlevel design-cycle only minimally.