Abstract
The growing design-productivity gap has made designers shift toward using high-level languages like C, C++ and Java to do system-level design. High-Level Synthesis (HLS) is the process of generating Register Transfer Level (RTL) design from these initial high-level programs. 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. In this paper, we present an approach to validate the result of HLS against the initial high-level program using insights from translation validation, automated theorem proving and relational approaches to reasoning about programs. We have implemented our validating technique and have applied it to a highly parallelizing HLS framework called SPARK. We present the details of our algorithm and experimental results.
This research was supported in part by NSF CAREER Grant 0644306.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Ashar, P., Bhattacharya, S., Raghunathan, A., Mukaiyama, A.: Verification of RTL generated from scheduled behavior in a high-level synthesis flow. In: ICCAD, pp. 517–524 (1998)
Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: POPL 2004 (January 2004)
Bustan, D., Grumberg, O.: Simulation based minimization. In: McAllester, D.A. (ed.) CADE 2000. LNCS, vol. 1831. Springer, Heidelberg (2000)
Chandy, K.M.: Parallel program design: a foundation. Addison-Wesley Longman Publishing Co. Inc., Boston, MA, USA (1988)
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Journal of Association Computing Machinery 52(3), 365–473 (2005)
Eveking, H., Hinrichsen, H., Ritter, G.: Automatic verification of scheduling results in high-level synthesis. In: DATE 1999, NY, USA (1999)
Fisler, K., Vardi, M.Y.: Bisimulation and model checking. Correct Hardware Design and Verification Methods (September 1999)
Goldberg, B., Zuck, L., Barrett, C.: Into the loops: Practical issues in translation validation for optimizing compilers. Electronic Notes in Theoretical Computer Science 132(1), 53–71 (2005)
Grötker, T.: System Design with SystemC. Kluwer Academic Publishers, Dordrecht (2002)
Gupta, S., Dutt, N., Gupta, R., Nicolau, A.: Spark: A high-level synthesis framework for applying parallelizing compiler transformations. In: VLSI Design 2003 (2003)
Josephs, M.B.: A state-based approach to communicating processes. Distributed Computing 3(1), 9–18 (1988)
Karfa, C., Mandal, C., Sarkar, D., Pentakota, S.R., Reade, C.: A formal verification method of scheduling in high-level synthesis. In: ISQED, pp. 71–78 (2006)
Kim, Y., Kopuri, S., Mansouri, N.: Automated formal verification of scheduling process using finite state machines with datapath (fsmd). In: ISQED 2004 (2004)
Kundu, S., Lerner, S., Gupta, R.: Automated refinement checking of concurrent systems. In: ICCAD 2007 (2007)
Lacey, D., Jones, N.D., Wyk, E.V., Frederiksen, C.C.: Proving correctness of compiler optimizations by temporal logic. In: POPL 2002 (January 2002)
Lam, M.: Software pipelining: an effective scheduling technique for VLIW machines. In: PLDI 1988 (June 1988)
Lin, Y.-L.: Recent developments in high-level synthesis. ACM Transactions on Design Automation of Electronic Systems 2(1), 2–21 (1997)
Narasimhan, N., Teica, E., Radhakrishnan, R., Govindarajan, S., Vemuri, R.: Theorem proving guided development of formal assertions in a resource-constrained scheduler for high-level synthesis. Form. Methods Syst. Des. 19(3), 237–273 (2001)
Necula, G.C.: Translation validation for an optimizing compiler. In: PLDI 2000 (June 2000)
Pnueli, A., Siegel, M., Singerman, E.: Translation Validation. In: Steffen, B. (ed.) ETAPS 1998 and TACAS 1998. LNCS, vol. 1384, pp. 151–166. Springer, Heidelberg (1998)
Rinard, M., Marinov, D.: Credible compilation. In: Proceedings of the FLoC Workshop Run-Time Result Verification (July 1999)
Walker, R., Camposano, R.: A Survey of High-Level Synthesis Systems. Kluwer Academic Publishers, Boston, MA, USA (1991)
Zuck, L., Pnueli, A., Fang, Y., Goldberg, B.: VOC: A methodology for the translation validation of optimizing compilers. Journal of Universal Computer Science 9(3), 223–247 (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kundu, S., Lerner, S., Gupta, R. (2008). Validating High-Level Synthesis. In: Gupta, A., Malik, S. (eds) Computer Aided Verification. CAV 2008. Lecture Notes in Computer Science, vol 5123. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70545-1_44
Download citation
DOI: https://doi.org/10.1007/978-3-540-70545-1_44
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70543-7
Online ISBN: 978-3-540-70545-1
eBook Packages: Computer ScienceComputer Science (R0)