FORMALSEMANTICS FORVHDL THE KLUWER INTERNATIONAL SERIES IN ENGINEERING AND COMPUTER SCIENCE VLSI, COMPUTER ARCHITECTURE AND DIGITAL SIGNAL PROCESSING Consulting Editor Jonathan Allen Other books in the series: ONOPTIMALINTERCONNECTIONSFORVLSI, AndrewB. Kahng, Gabriel Robins ISBN: 0-7923-9483-6 SIMULATION TECHNIQUES AND SOLUTIONS FOR MIXED-SIGNAL COUPLING IN INTEGRATEDCmCUITS, Nishath K. Verghese, TimothyJ. Schmerbeck, DavidJ. Allstot ISBN: 0-7923-9544-1 MIXED-MODE SIMULATION AND ANALOG MULTILEVEL SIMULATION, Resve Saleh, Shyh-JyeJou, A. Richard Newton ISBN: 0-7923-9473-9 CADFRAMEWORKS: Principles and Architectures, PietervanderWolf ISBN: 0-7923-9501-8 PIPELINEDADAPTIVEDIGITALFILTERS, Naresh R. Shanbhag, Keshab K. Parhi ISBN: 0-7923-9463-1 TIMEDBOOLEANFUNCTIONS: AUnified Formalismfor ExactTimingAnalysis, William K.C. Lam, RobertK. Brayton ISBN: 0-7923-9454-2 ANANALOGVLSISYSTEM FORSTEREOSCIPIC VISION, MishaMahowald ISBN: 0-7923-944-5 ANALOGDEVICE-LEVELLAYOUTAUTOMATION, JohnM. Cohn, DavidJ. Garrod, RobA. Rutenbar, L. Richard Carley ISBN: 0-7923-9431-3 VLSIDESIGNMETIlOOOLOGIESFORDIGITALSIGNALPROCESSING ARCHITECTURES, Magdy A. Bayoumi ISBN: 0-7923-9428-3 CmCUITSYNTIIESIS WITIIVHDL, RolandAiriau, Jean-Michel Berge, VincentOlive ISBN: 0-7923-9429-1 ASYMPTOTIC WAVEFORMEVALUATION, EliChiprout, MichelS. Nakhla ISBN: 0-7923-9413-5 WAVEPIPELINING:THEORYANDCMQSIMPLEMENTATION, C. ThomasGray, Wentai Liu, RalphK. Cavin, DI ISBN: 0-7923-9398-8 CONNECTIONISTSPEECHRECOGNITION: AHybrid Appoach, H. Bourlard, N. Morgan ISBN: 0-7923-9396-1 BiCMOSTECHNOLOGYANDAPPLICATIONS, SECONDEDITION, A.R. Alvarez ISBN: 0-7923-9384-8 TECHNOLOGYCAD-COMPUTERSIMULATIONOFIC PROCESSES ANDDEVICES, R. Dutton, Z. Yu ISBN: 0-7923-9379 VHDL '92, THE NEW FEATURES OF THE VHDL HARDWARE DESCRIPTION LANGUAGE,J. Berge, A. Fonkoua, S. Maginot, 1. Rouillard ISBN: 0-7923-9356-2 APPLICATIONDRIVENSYNTHESIS, F. Catthoor, L. Svenson ISBN:0-7923-9355-4 FORMAL SEMANTICS FORVHDL Edited by Carlos Delgado Kloos and Peter T. Breuer Universidad Politecnica de Madrid, Madrid, Spain SPRINGER-SCIENCE+BUSINESS MEDIA, B.V. Library of Congress Cataloging-in-Publication Data Formal semantlcs for VHDL / edlted by Carlos Delgado Kloos. Peter T. Breuer. p. c •. Includes blbllographlcal references. ISBN 978-1-4613-5941-8 ISBN 978-1-4615-2237-9 (eBook) DOI 10.1007/978-1-4615-2237-9 1. VHDL (Computer hardware descrlptlon lanaguage) 2. Programmlng languages (Electronic computersl--Semantics. r. Kloos. Carlos Delgado. II. Breuer. Peter T. TK885.7.F67 1995 621.39'2--dc20 94-46912 ISBN 978-1-4613-5941-8 Printed on acid-free paper AH Rights Reserved © 1995 Springer Science+Business Media Dordrecht Originally published by Kluwer Academic Publishers in 1995 Softcover reprint ofthe hardcover Ist edition 1995 No part of the material protected by this copyright notice may be reproduced or utilized in any form or by any means, electronic or mechanical. inc1uding photocopying. recording or by any information storage and retrieval system, without written permission from the copyright owner. CONTENTS FOREWORD ix PREFACE xi CONTRIBUTORS Xlll o GIVING SEMANTICS TO VHDL: AN INTRODUCTION Carlos Delgado Kloos, Peter T. Breuer 1 1 VHDL 1 2 Semantics 2 3 A Running Example 5 4 Contents ofthis book 6 1 A FUNCTIONAL SEMANTICS FOR DELTA-DELAY VHDL BASED ON FOCUS Max Fuchs, Michael Mendler 9 1 Introduction 10 2 A Motivating Example 11 3 Assumptions 14 4 Formal Semantics for 6-VHDL 22 5 Conclusion 40 APPENDIX A Syntax of6-VHDL 41 2 A FUNCTIONAL SEMANTICS FOR UNIT-DELAY VHDL Peter T. Breuer, Luis Sanchez Fernandez, Carlos Delgado Kloos 43 1 Introduction 43 2 The VHDL Subset 46 v vi 3 Functional Semantics 49 4 Summary and Future Work 68 APPENDIX A Auxiliary Function Definitions 70 3 AN OPERATIONAL SEMANTICS FOR A SUBSET OF VHDL John P. Van Tassel 71 1 Introduction 71 2 Related Research 73 3 Syntax 76 4 Operational Semantics 80 5 Information Organization 82 6 Rules ofthe Semantics 85 7 Equivalence 96 8 A NAND Gate 97 9 Conclusions 104 4 A FORMAL DEFINITION OF AN ABSTRACT VHDL'93 SIMULATOR BY EA-MACHINES Egon Borger, Uwe Glasser, Wolfgang Muller 107 1 Introduction 108 2 Related Work 109 3 EA-Machines 111 4 The Formal Model 114 5 Example 131 6 Conclusion & Future Directions 138 APPENDIX A Elaborated Example 139 5 A FORMAL MODEL OF VHDL USING COLOURED PETRI NETS Serafin Olcoz 140 1 Introduction 140 2 VHDL Event-Driven Simulation 141 3 The VHDL Execution Model 145 4 Variables, Types and Expressions 148 5 Statements, Subprograms and Processes 159 Contents vii 6 Implementation ofa CPN Model Generator 166 7 Conclusions 167 6 A DETERMINISTIC FINITE-STATE MODEL FORVHDL Gert Dohmen, Ronald Herrmann 170 1 Introduction 170 2 Generation ofthe Finite-State Model 173 3 Conclusion 200 APPENDIX A Elaborated Running Example 201 APPENDIX B Utility Functions 202 7 A FLOW GRAPH SEMANTICS OF VHDL: A BASIS FOR HARDWARE VERIFICATION WITHVHDL Ral!Reetz, Thomas Krap! 205 1 Introduction 206 2 Flow Graph Model 209 3 Semantics ofVHDL 215 4 The Example 231 5 Verification 234 6 Conclusion and Future Work 238 REFERENCES 239 FOREWORD It is recognized that formal design and verification methods are an impor tant requirement for the attainment of high quality system designs. The field has evolved enormously during the last few years, resulting in the fact that formal design and verification methods are nowadays supported by several commercially- and academically-based tools. A pan-European network, named EuroFORM, has been formed, bringing to gether European groups active in research on formal system design and verifi cationmethodologies. Thenetworkhas beensponsored bytheEuropeanUnion under the DGXII Human Capital and Mobility Program (HCM). EuroFORM currently consists of the following partners: Technical University of Denmark (Prof. J. Staunstrup), Universite Joseph Fourier (Prof. D. Borrione), Politec nico di Torino (Prof. P. Prinetto), Universite de Provence (Prof. L. Pierre), University of Frankfurt (Prof. H. Eveking), University of Passau (Prof. W. Grass), University of Manchester (Prof. H. Barringer), University of Olden burg (Prof. W. Damm), Fraunhofer G. Dresden (Dr. B. Straube), Technical University of Madrid (Prof. C. Delgado Kloos), University ofRome (Prof. R. de Nicola), Bull Paris (Prof. F. Anceau), University of Cambridge (Prof. M. Gordon) and IMEC. VHDL has become widely accepted as a standard hardware description lan guage. The languageis currently supported by different kinds oftools: simula tors, synthesisers, verifiers, performance analysers, etc., provided by a variety ofdifferent vendors. Having different tools and users generating and reading the same language requires that the same semantics is assigned by them to all constructs and elementsofthelanguage. Thecurrent IEEE standard VHDLlanguagereference manual (LRM) tries to define VHDL as well as possible in a descriptive way, explaining the semantics in English. But rigor and clarity is very hard to maintain in a semantics defined in this way, and that has already given rise to many misconceptions and contradictory interpretations. ix Foreword x Severalgroupshavebeen activein workingonmethodsfor theformal definition ofthe VHDL semantics. Most ofthose methods were presented and discussed during a workshop organized by Prof. Carlos Delgado Kloos, within the scope ofthe EuroFORM network, in Las Navas del Marques near Madrid in January 1994, and a representativeset are described extensively in this book. The fun damentals ofan overlappingand partially alternative set ofapproaches will be collectedina specialissue, companiontothisbook,oftheInternationalJournal on Formal Methods in System Design, edited by Prof. Dominique Borrione. We hereby thank the European Union which has enabled us, in the framework ofthe Human Capital and Mobility program, to bringseveralviews togetherin the EuroFORM network. The results presented in this book are now available to the global community interested in the semantics of VHDL. The efforts of the authors and editors in proposing solutions and approaches for the formal definition ofthe semantics ofthe VHDL languagewill definitely contribute to the better understanding and formulation ofthis important lan guage. It will contribute to a more universal use and definition of VHDL and other future system description languages. Prof. Luc Claesen EuroFORM network coordinator PREFACE This book presents a number ofapproaches each giving a formal semantics to the hardware description language VHDL. Who should read this book? To whom is it directed? One can envisageseveral groupsofpeopleas beinginterested in it. On theonehand, peoplewhoalready know VHDL and would like to look at it from a different perspective. Some of thecontributionsinthis bookfollow thesimulation cycleapproachdescribed in the LanguageReference Manual (LRM), but someofthemdescribe VHDLfrom a totally different point of view. Although the LRM describes the semantics of the language from the perspective of an abstract simulation program, one can abstract beyond simulation concepts and describe the languageconstructs directly. Another group ofpeople who could be interested are people who have worked with formal semantics and the formal characterizationoflanguages. For them, it might be easier to understand the language by reading this book than by reading the LRM or hardware-oriented textbooks. Finally, people concerned with applications ofVHDL might find this book in teresting. Here they canfind out how VHDL may be treated by model checking techniques, how generic properties about VHDL models may be proved, or how VHDL may be embedded in a theorem prover. The collection of papers presented in this book has its origins in a workshop organizedinLasNavasdelMarquesnearMadrid (Spain) in January1994. This workshop wasorganizedin thecontext ofthe project EuroFORM, sponsored by the Commission of the European Union, in which 14 institutions are partici pants. Someofthe chaptersofthis bookare written by partnersin the project and some are authored by outside experts. The existence of the EuroFORM project, and its funding body, the European Commission, is gratefully acknowledged. Not only because it made the work shop possible. Boththe postsofPeterT. Breuerat the UniversidadPolitecnica xi