High-level Synthesis Integrated Verification

M. Dossis

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-DA

Full Text:

PDF

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

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

R. A. Walker, S. Chaudhuri, “Introduction to the scheduling problem”, IEEE Design & Test of Computers, Vol. 12, No. 2, pp. 60–69, 1995

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

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

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

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

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

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

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.

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

M. Dossis, "Intermediate Predicate Format for Design Automation Tools", Journal of Next Generation Information Technology, Vol. 1, No. 1, pp. 100-117, 2010

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

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

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

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

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




eISSN: 1792-8036     pISSN: 2241-4487