Hand-in-hand verification of high-level synthesis

This paper describes a formal verification methodology of highnthesis (HLS) process. The abstraction level of the input to HLS is so high compared to that of the output that the verification has to proceed hand-in-hand with the synthesis process. The HLS verification is performed in three phases in this work. The verification method is based on equivalence checking of two finite state machines with data-paths (FSMDs). Unlike most reported works that targets the individual phases independently, the proposed method applies to all these three phases. The method is strong enough to accommodate control structure modification of the original behaviour, application of several code motion techniques during scheduling and register optimization during register allocation. It can also verify the correctness of the controller. A hand-in-hand synthesis and verification tool SAST has been developed and tested for effectiveness on several HLS benchmark circuits. Categories and Subject Descriptors B....

• Type: Conference
• Year: 2007
• Where: GLVLSI
• Authors: Chandan Karfa, Dipankar Sarkar, Chittaranjan A. Mandal, Chris Reade
• Keywords: Formal Verification, Formal Verification Methodology, GLVLSI 2007, HLS Verification, VLSI