Translation Validation of High-Level Synthesis

The growing complexity of systems and their implementation into silicon encourages designers to look for model designs at higher levels of abstraction and then incrementally build portions of these designs--automatically or manually--from these high-level specifications. Unfortunately, this translation process itself can be buggy, which can create a mismatch between what a designer intends and what is actually implemented in the circuit. Therefore, checking if the implementation is a refinement or equivalent to its initial specification is of tremendous value. In this paper, we present an approach to automatically validate the implementation against its initial high-level specification using insights from translation validation, automated theorem proving, and relational approaches to reasoning about programs. In our experiments, we first focus on concurrent systems modeled as communicating sequential processes and show that their refinements can be validated using our approach. Next, w...

• Type: Journal
• Year: 2010
• Where: TCAD
• Authors: Sudipta Kundu, Sorin Lerner, Rajesh K. Gupta
• Keywords: Implementation, Initial Specification, Software Engineering, TCAD 2010, Validation Approach