is to certify that the thesis entitled "A Practical Framework For Formal Verification

A PRACTICAL FRAMEWORK FOR FORMAL VERIFICATION OF HIGH LEVEL SYNTHESIZERS

by

B.M. SUBRAYA

DEPARTMENT OF COMPUTER SCIENCE AND ENGINEERING

A Thesis Submitted in partial fulfillment of the requirements for the Degree of

Doctor of Philosophy

to the

INDIAN INSTITUTE OF TECHNOLOGY, DELHI NEW DELHI-110 016

INDIA MARCH 1994

Certificate

is to certify that the thesis entitled "A Practical Framework For Formal Verification

Technology, Delhi, for the award of Degree of Doctor of Philosophy, is a bonafide research work carried out by him under our supervision and guidance. The results obtained in this thesis have not been submitted to any other university or Institute for the award of any other degree or diploma.

k(kolv

tuvw-A,_

Dr. Shashi Kumar Associate Professor,

Deptt. of Computer Science and Engineering,

Indian Institute of Technology, New Delhi 110 016

Dr. Anshul Kumar Professor,

Deptt. of Computer Science and Engineering,

Indian Institute of Technology,

New Delhi 110 016

To my parents and Gaurav

Acknowledgements

I am greatly indebted to my supervisors Prof. Anshul Kumar and Prof. Shashi Kumar for their invaluable technical guidance and moral support during course of my research. This work could never have taken shape without their continued guidance and support.

Without their active involvement, it wouldn't have been possible for me to complete this arduous task. Working with them has been a great pleasure and learning experience for me.

I would also like to thank Prof. M.H Dhananjaya, Director(T), J.S.S Mahavidyapeetha, Mysore, for allowing me to continue my research work. Without his moral support and constant encouragement, it would have been difficult to complete this work.

I am thankful to the Ministry Human Resource Development(MHRD), Govt. of India for sponsoring me under the Quality Improvement Scheme(QIP). My sincere thanks to the Principal, Si. College of Engineering, Mysore, for having deputed me for the research work.

I take this opportunity to thank Prof. P.C.P. Bhatt, Dr. Balakrishnan and Dr. Arun Kumar for their valuable suggestions. I also thank the chairman and members of the Departmental Review Committee for their help.

I am greatly indebted to Mr. Manoj Karunakaran and Mr. Naseer for providing all sorts of help during the final stages of this work.

I am also thankful to my colleagues at SJ College of Engineering, Mysore, particularly Prof. A.G Hariharan and Prof. K. Chidananda Gowda for their support during my research.

My thanks are due to several friends at IIT Delhi, Mr. Rustagi of network lab and members of CAD lab who contributed one way or the other during the preparation of this thesis.

My sincere thanks to Mr. and Mrs. Sriram Hegde for providing help in many ways during the completion stages of this work.

I am grateful to Mr. and Mrs. Narashimha Hegde and Ravindra Hegde who have provided moral support, encouragement and strength during my final stages of the work.

My parents have constantly encouraged and inspired me throughout my life. I cannot thank them enough for giving me the best education possible. Without their blessings, I wouldn't have been successful in my endeavours. I take this opportunity to acknowledge their love, affection and support. I respectfully and lovingly dedicate this thesis to them.

Finally, I sincerely accept the fact that this work wouldn't have been possible without the cooperation and innumerable sacrifices made by my wife, Yamuna.

ii

ABSTRACT

With the growing acceptability of high level synthesizers to design complex circuits in short time periods, there are also increasing expectations about correctness of the synthesized designs. This thesis investigates the problem of designing synthesizers which would guarantee correctness of the designs produced. No satisfactory solution to this problem had been available so far.

The thesis presents a formal framework in which the synthesis and verification processes can be modelled in a practical way. It is shown that the complexity of the verification process can be reduced by following the modularity usually present in a synthesizer design. The essential idea here is to identify the conditions under which the overall correctness of the synthesizer can be ensured by verifying only local correctness of the individual subsystems like scheduler, allocator, binder etc.

To simplify the correctness proof of the individual synthesis steps, some easily verifiable templates are defined, in which the algorithms can be expressed. The templates have a restrictive structure of control constructs, but are general enough to allow mapping of a variety of synthesis algorithms on to them. Two kinds of functions are used in the templates - a) synthesis functions, which build up the hardware structure, and b) computation functions, which compute parameters for the synthesis functions and also take care of the optimization issues. It has been shown that if computation functions satisfying

iii

certain properties are used to derive synthesis algorithms from these templates, then these algorithms are assured to be correct. A number of pre-proven templates along with the required properties of the associated computation functions are presented for various synthesis steps. This reduces the effort required for proving correctness of new synthesis algorithms.

The thesis demonstrates how this methodology can be embedded in HOL(Higher Order Logic) system, and in particular, how correctness of templates can be proved. In order to prove correctness of templates, a language in which the templates can be represented is defined in HOL. Interfaces of synthesis modules, correctness criteria, and properties of the computation functions are also expressed in the same framework. Details of the proof of a scheduling template are presented for illustration.

iv

TABLE OF CONTENTS

Acknowledgements Abstract

Table of Contents List of Figures List of Tables

CHAPTER 1 INTRODUCTION 1

1.1 Hardware Verification 1

1.2 High Level Synthesis and Verification 2 1.3 Classification of Hardware Verification Methodologies 4

1.4 Previous Work 5

1.4.1 Verifying Correctness of Individual Designs 8 1.4.2 Synthesis Coupled with Verification 10 1.4.3 Specific Synthesizers Which are Correct 10 1.4.4 General Approaches for Designing Correct Synthesizers 11

1.5 Motivation for Present Work 13

1.6 Our Synthesis Verification Approach 14 1.6.1 Flexibility and Ease of Verification 14

1.6.2 Managing the Complexity 15

1.6.3 A Practical Framework 16

1.7 Overview of the Thesis 17

v

CHAPTER 2 OVERVIEW OF THE PROPOSED APPROACH 18

2.1 Introduction 18

2.2 High Level Synthesis and its Partitioning 19 2.3 Verification of Synthesis in Terms of Synthesis Steps 21 2.4 Synthesis Templates and Their Verification 23 2.5 Synthesis Verification and HOL Proof System 25

CHAPTER 3 MODULARIZING VERIFICATION OF SYNTHESIS

PROCESS 28

3.1 Introduction 28

3.2 Relationship Between Local and Global Correctness 29 3.3 Formal Representation of Interfaces Between Synthesis Steps 31

3.3.1 Division of Synthesis Task into Subtasks 35 3.3.2 Input to the High Level Synthesizer 36 3.3.3 Representation of Scheduler Output 45 3.3.4 Representation of Allocator Output 46 3.3.5 Representation of Binder Output 47 3.3.6 Representation of Interconnections 47 3.3.7 Representation of Control Part Realization 48 3.4 Correctness of Data Part Synthesis Output 52 3.4.1 Formal Correctness Criteria for a Scheduler 53 3.4.2 Formal Correctness Criteria for Allocations 54 3.4.3 Formal Correctness Criteria for a Binder 59 3.5 Correctness Criteria for Control Part Synthesis Process 67

3.6 Conclusions 73

vi

CHAPTER 4 TEMPLATES BASED SYNTHESIS STEPS AND THEIR

VERIFICATION 74

4.1 Introduction 74

4.2 Synthesis Functions and Computation Functions 76 4.2.1 Synthesis Function for Scheduling 77 4.2.2 Synthesis Function for Allocation 78 4.2.3 Synthesis Function for Binding 78 4.2.4 Synthesis Function for Interconnection 80 4.3 Templates for Synthesizer Algorithms 81

4.3.1 Templates for Operator Scheduling 84 4.3.2 Modelling of Scheduling Algorithms 91 4.3.3 Templates for Allocation 94

4.3.4 Templates for Binding 96

4.3.5 Modelling Binding Algorithms 106 4.3.6 Templates for Interconnection 106

4.4 Verification of Templates 108

4.4.1 Proof of Scheduling Templates 109

4.5 Conclusions 123

CHAPTER 5 SYNTHESIS VERIFICATION AND THEOREM

PROVER: HOL 123

5.1 Introduction 123

5.2 HOL Proof Checker 124

5.3 Language for Representing Templates 126

5.3.1 Syntax 127

5.3.2 Semantics 128

vii

5.4 Template Examples 131 5.4.1 Input-Output Structures 131

5.4.2 Synthesis Functions 133

5.4.3 Computation Functions 134

5.4.4 Examples 134

5.5 Preparing for Verification 136

5.5.1 Representation of Correctness Criteria 138 5.5.2 Representing Properties of Computation Functions 139

5.6 Proof of Template tosl 143

5.6.1 Verification Goal 144

5.6.2 Proof of Dependency Preserving Property 145 5.6.3 Part B: Proof of Conflict Free Property 152 5.6.4 Part C: Proof of Completeness Property 156

5.6 Conclusions 160

CHAPTER 6 CONCLUSIONS 162

6.1 Summary of Results and Achievements 162 6.2 Guidelines for Writing a Correct Synthesizer 164

6.3 Directions of Future Work 166

REFERENCES 167

APPENDIX A 177

APPENDIX B 179

viii