High-level Synthesis Integrated Verification
Abstract
It is widely known in the engineering community that more than 60% of the IC design project time is spent on verification. For the very complex contemporary chips, this may prove prohibitive for the IC to arrive at the correct time in the market and therefore, valuable sales share may be lost by the developing industry. This problem is deteriorated by the fact that most of conventional verification flows are highly repetitive and a great proportion of the project time is spent on last-moment simulations. In this paper we present an integrated approach to rapid, high-level verification, exploiting the advantages of a formal High-level Synthesis tool, developed by the author. Verification in this work is supported at 3 levels: high-level program code, RTL simulation and rapid, generated C testbench execution. This paper is supported by strong experimental work with 3-4 popular design synthesis and verification that proves the principles of our methodology.
Keywords:
High-level Synthesis, Formal verification, E-DADownloads
References
B. L. Gal, E. Casseau, S. Huet, “Dynamic Memory Access Management for High-Performance DSP Applications Using High-Level Synthesis”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 16, No. 11, pp.1454-1464, 2008 DOI: https://doi.org/10.1109/TVLSI.2008.2000821
S. Gupta, R. K. Gupta, N. D. Dutt, A. Nikolau, “Coordinated Parallelizing Compiler Optimizations and High-Level Synthesis”, ACM Transactions on Design Automation of Electronic Systems, Vol. 9, No. 4, pp. 441–470, 2004 DOI: https://doi.org/10.1145/1027084.1027087
R. A. Walker, S. Chaudhuri, “Introduction to the scheduling problem”, IEEE Design & Test of Computers, Vol. 12, No. 2, pp. 60–69, 1995 DOI: https://doi.org/10.1109/54.386007
M. F. Dossis, “A Formal Design Framework to Generate Coprocessors with Implementation Options”, International Journal of Research and Reviews in Computer Science, Vol. 2, No. 4, pp. 929-936, 2011
P. G. Paulin, J. P. Knight, “Force-directed scheduling for the behavioral synthesis of ASICs”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 8, No. 6, pp. 661–679, 1989 DOI: https://doi.org/10.1109/43.31522
A. A. Kountouris, C. Wolinski, “Efficient Scheduling of Conditional Behaviors for High-Level Synthesis”, ACM Transactions on Design Automation of Electronic Systems, Vol. 7, No. 3, pp. 380–412, 2002 DOI: https://doi.org/10.1145/567270.567272
U. Nilsson, J. Maluszynski, Logic Programming and Prolog, John Wiley & Sons Ltd., 2nd Edition, 1995
A. A. Del Barrio, R. Hermida, S. O. Memik, J. M. Mendias, M. C. Molina, “Multispeculative Addition Applied to Datapath Synthesis”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 31, No. 12, pp. 1817-1830, 2012 DOI: https://doi.org/10.1109/TCAD.2012.2208966
O. Sarbishei, K. Radecka, “On the Fixed-Point Accuracy Analysis and Optimization of Polynomial Specifications”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 32, No. 6, pp. 831-844, 2013 DOI: https://doi.org/10.1109/TCAD.2013.2238290
A. Morvan, S. Derrien, P. Quinton, “Polyhedral Bubble Insertion: A Method to Improve Nested Loop Pipelining for High-Level Synthesis”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 32, No. 3, pp. 339-352, 2013 DOI: https://doi.org/10.1109/TCAD.2012.2228270
K. Banerjee, C. Karfa, D. Sarkar, C. Mandal, “Verification of Code Motion Techniques Using Value Propagation”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 33, No. 8, pp. 1180-1193, 2014 DOI: https://doi.org/10.1109/TCAD.2014.2314392
R. Sierra, C. Carreras, G, Caffarena, C. A. López Barrio, “A Formal Method for Optimal High-Level Casting of Heterogeneous Fixed-Point Adders and Subtractors”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 34, No. 1, pp. 52-62, 2015. DOI: https://doi.org/10.1109/TCAD.2014.2365094
S. Xydis, G. Palermo, V. Zaccaria, C. Silvano, “SPIRIT: Spectral-Aware Pareto Iterative Refinement Optimization for Supervised High-Level Synthesis”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 34, No. 1, pp. 155-159, 2015 DOI: https://doi.org/10.1109/TCAD.2014.2363392
M. Dossis, "Intermediate Predicate Format for Design Automation Tools", Journal of Next Generation Information Technology, Vol. 1, No. 1, pp. 100-117, 2010 DOI: https://doi.org/10.4156/jnit.vol1.issue1.9
M. Dossis, Patent number 1005308, 5/10/2006 by the Greek Industrial Property Organisation, 2006
D. Amanatidis, M. Dossis, “High level synthesis of geometric active contours”, 2nd Global Virtual Conference, Slovakia, April 7-11, 2014
L. Wu, H. Huang, K. Su, S. Cai, X. Zhang, “An I/O Efficient Model Checking Algorithm for Large-Scale Systems”, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, Vol. 23, No. 5, pp. 905-915, 2015 DOI: https://doi.org/10.1109/TVLSI.2014.2330061
C. B. Harris, I. G. Harris, “Generating formal hardware verification properties from Natural Language documentation”, 2015 IEEE International Conference on Semantic Computing (ICSC), Anaheim, CA, pp. 49-56, February 7-9, 2015 DOI: https://doi.org/10.1109/ICOSC.2015.7050777
R. A. Hernandez, M. Strum, W. J. Chau, “Transformations on the FSMD of the RTL code with combinational logic statements for equivalence checking of HLS”, 16th Latin-American Test Symposium (LATS), Puerto Vallarta, Mexico, pp. 1-6, March 25-27, 2015 DOI: https://doi.org/10.1109/LATW.2015.7102518
V. Athavale, M. Sai, S. Hertz, S. Vasudevan, “Code coverage of assertions using RTL source code analysis”, 51st ACM/EDAC/IEEE Design Automation Conference (DAC), Moscone Center, San Francisco, CA, USA, pp. 1-6, June 1-5, 2014 DOI: https://doi.org/10.1145/2593069.2593108
Yang Shuo, R. Wille, R. Drechsler, “Improving Coverage of Simulation-Based Verification by Dedicated Stimuli Generation”, 17th Euromicro Conference on Digital System Design (DSD), Verona, Italy, pp. 599-606, August 27-29, 2014 DOI: https://doi.org/10.1109/DSD.2014.100
Downloads
How to Cite
License
Authors who publish with this journal agree to the following terms:
- Authors retain the copyright and grant the journal the right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.
- Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.
- Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) after its publication in ETASR with an acknowledgement of its initial publication in this journal.
