Automated formal verification of scheduling with speculative code motions

ABSTRACT

We present a methodology for formal verification of scheduling phase of High-Level Synthesis (HLS) when speculative code motions are performed during this process. Verification relies on establishing functional equivalence between the result of scheduling and the behavioral specification of the design, using their FSMD models. We propose and formally define a relation between the two FSMDs that is less constrained than the strong equivalence, but stronger than weak equivalence. For verification of scheduling involving speculative code motions, we propose the notion of FSMD recomposition, a transformation that alters the state sequence and/or the operation of each state, while maintaining the functionality. The equivalence conditions are formulated in higher-order logic, and their correctness is verified in the theorem proving environment PVS. The entire verification flow, including formal model extraction and proof generation is fully automated.

REFERENCES

• 1: Pranav Ashar , Subhrajit Bhattacharya , Anand Raghunathan , Akira Mukaiyama, Verification of RTL generated from scheduled behavior in a high-level synthesis flow, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.517-524, November 08-12, 1998, San Jose, California, United States [doi>10.1145/288548.289080]
• 2: Dominique Borrione , Julia Dushina , Laurence Pierre, A compositional model for the functional verification of high-level synthesis results, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, v.8 n.5, p.526-530, Oct., 2000 [doi>10.1109/92.894157]
• 3: Chandan Karfa , Dipankar Sarkar , Chittaranjan Mandal , Chris Reade, Hand-in-hand verification of high-level synthesis, Proceedings of the 17th ACM Great Lakes symposium on VLSI, March 11-13, 2007, Stresa-Lago Maggiore, Italy [doi>10.1145/1228784.1228885]
• 4: Hans Eveking , Holger Hinrichsen , Gerd Ritter, Automatic verification of scheduling results in high-level synthesis, Proceedings of the conference on Design, automation and test in Europe, p.12-es, January 1999, Munich, Germany [doi>10.1145/307418.307449]
• 5: Daniel D. Gajski , Loganath Ramachandran, Introduction to High-Level Synthesis, IEEE Design & Test, v.11 n.4, p.44-54, October 1994 [doi>10.1109/54.329454]
• 6: Daniel D. Gajski , Nikil D. Dutt , Allen C.-H. Wu , Steve Y.-L. Lin, High-level synthesis: introduction to chip and system design, Kluwer Academic Publishers, Norwell, MA, 1992
• 7: S. Gupta, R. Gupta, N. Dutt, and A. Nicolau. SPARK. A Parallelizing Approach to the High-Level Synthesis of Digital Circuits. Kluwer Academic Publishers, 2004.
• 8: S. Gupta, N. Savoiu, S. Kim, N. Dutt, R. Gupta, and A. Nicolau. Speculation techniques for high level synthesis of control intensive designs. Technical Report 0040, University of California, Irvine, December 2000.
• 9: Youngsik Kim , Shekhar Kopuri , Nazanin Mansouri, Automated Formal Verification of Scheduling Process Using Finite State Machines with Datapath (FSMD), Proceedings of the 5th International Symposium on Quality Electronic Design, p.110-115, March 22-24, 2004
• 10: Nazanin Mansouri , Ranga Vemuri, Automated Correctness Condition Generation for Formal Verification ofSynthesized RTL Designs, Formal Methods in System Design, v.16 n.1, p.59-91, Jan 1,2000 [doi>10.1023/A:1008777509016]
• 11: N. Narasimhan, R. Kalyanaraman, and R. Vemuri. Validation of synthesized register-transfer level designs using simulation and formal verification. In Proc. High Level Design Validation and Test Workshop, Nov 1996.
• 12: S. Owre, N. Shankar, J. Rushby, and D.Stringer-Calvert. PVS Language Reference. SRI International, Sep. 1999.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION
      B.5.2 Design Aids
          Subjects: Verification

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages

  I. Computing Methodologies
  I.6 SIMULATION AND MODELING
      I.6.5 Model Development

General Terms:
Verification

Keywords:
automated theorem-proving, formal verification, high level synthesis, speculation