HIERARCHICAL ANNOTATED ACTION DIAGRAMS An Interface-Oriented Specification and Verification Method HIERARCHICAL ANNOTATED ACTION DIAGRAMS An Interface-Oriented Specification and Verification Method E. Cerny Universite de Montreal B. Berkane Nortel Semiconductors P. Girodias Universite de Montreal K. Khordoc McGill University .... " SPRINGER SCIENCE+BUSINESS MEDIA, LLC Library of Congress Cataloging-in-Publication Data A c.I.P. Catalogue record for this book is available from the Library of Congress. ISBN 978-1-4613-7569-2 ISBN 978-1-4615-5615-2 (eBook) DOI 10.1007/978-1-4615-5615-2 Copyright © 1998 Springer Science+Business Media New York Originally published by Kluwer Academic Publishers, New York in 1998 Softcover reprint ofthe hardcover 1st edition 1998 All rights reserved. No part of this publication may be reproduced, stored in a retrieval system or transmitted in any form or by any means, mechanical, photo copying, recording, or otherwise, without the prior written perrnission of the publisher, Springer Science+Business Media, LLC. Printed on acid-free paper. Contents List of Figures ...................................................................... ix List of Tables ......................................................................x iii Preface ................................................................................. xv 1 Introduction .•................................................................. 1 1.1 Digital System Design and Verification ........................................................ .1 1.2 Interface-Oriented Models ............................................................................ .5 1.3 Purpose and Organization of the Book ...........................................................7 2 Overview of HAAD Method ......................................... 9 2.1 Leaf Action Diagrams .................................................................................. 10 2.2 Annotations in Leaf Action Diagrams ........................................................ .16 2.3 Hierarchical Action Diagrams ...................................................................... 17 2.4 Annotations in HAAD Hierarchy ................................................................. 19 3 Formal Characterization of HAAD ........................... 23 3.1 Leaf-Level Action Diagram Algebra ............................................................2 4 3.1.1 Basic Concepts and Notations .......................................................................... 24 3.1.2 Syntax and Intuitive Semantics ......................................................................... 25 Hierarchical Annotated Action Diagrams 3.1.3 Operational Semantics ..................................................................................... 27 3.104 Equivalence ...................................................................................................... 31 3.2 Verification .................................................................................................. .33 3.2.1 Basic theorems and intermediateform ............................................................. 33 3.2.2 Reactivity .......................................................................................................... 34 3.2.3 Equivalence verification ................................................................................... 37 3.3 Language of Hierarchical Action Diagrams .................................................4 1 3.3.1 Syntax and intuitive semantic .......................................................................... 041 3.3.2 Operational semantics ...................................................................................... 42 3.4 Related work ................................................................................................ .46 4 HAAD VHDL Model .................................................. 49 4.1 Execution ofHAAD VHDL Models ........................................................... .50 4.1.1 Status of an Action Diagram ........................................................................... .51 4.1.2 Operations in a Leaf Action Diagram .............................................................. 52 4.1.3 Occurrence intervals of input specified actions ............................................... 53 4.104 Occurrence time of specified DON'T CARE inputs ......................................... 54 4.1.5 VAUD or CONSTANT inputs after DON'T CARE .......................................... 54 4.1.6 Occurrence time of VALID or CONSTANT inputs ........................................... 56 4.1.7 Execution rules for specified input actions ...................................................... 58 4.1.8 Execution rulesfor end actions ........................................................................ 59 4.2 Execution of Hierarchical Action Diagrams ................................................ 60 4.3 Occurrence Time Enumeration of Output Actions ....................................... 61 4.4 Enumeration and Delay Correlation ............................................................. 64 4.5 Organization of a HAAD Model in VHDL .................................................. 64 5 Consistency, Causality and Compatibility ................ 69 5.1 Introduction .................................................................................................. 70 5.2 Basic Concepts ............................................................................................. 71 5.3 Problems ....................................................................................................... 75 5.3.1 Causality ........................................................................................................... 76 5.3.2 Compatibility .................................................................................................... 77 5.4 Block Machines ............................................................................................ 79 5.5 Derived Block Machines .............................................................................. 84 5.6 Causal Action Diagrams ............................................................................... 87 5.7 Compatibility of Action Diagrams ............................................................... 91 vi Table of Contents 5.8 Conclusions .................................................................................................. 95 6 Interface Verification using CLP ............................... 99 6.1 Interface Tuning Verification ....................................................................... 99 6.2 Constraint Logic Programnling .................................................................. 100 6.3 The Event Separation Problem .................................................................. .102 6.4 Delay Correlation ....................................................................................... 103 6.5 CSP and CLP Based on RIA ..................................................................... .106 6.5.1 Constraint saJisfaction problems .................................................................... 106 6.5.2 Consistency techniques ................................................................................... 107 6.5.3 Interval Arithmetic ......................................................................................... 108 6.5.4 Relational arithmetic versus functional aritlunetic ........................................ 109 6.5.5 CLP (BNR) Prolog and interval propagation ................................................ 110 6.5.6 Partial consistency in CLP (BNR) Prolog ...................................................... 111 6.6 Solving lTV with CLP Based on RIA ....................................................... .113 6.6.1 Consistency ...................................................................................................... 114 6.6.2 Global consistency issues in the presence of delay correlation ..................... 117 6.7 Examples .................................................................................................... 123 6.7.1 Causality Test ................................................................................................. 123 6.7.2 Satisjiability Test ............................................................................................. 125 6.8 Experimental Results .................................................................................. 127 6.9 Concluding Remarks .................................................................................. 131 7 Example: Interfacing ARM7 and a Static RAM ••.. 133 7.1 Problem Definition ..................................................................................... 134 7.2 Bus Functional Model of ARM7 Subset. ................................................... 139 7.3 Bus Functional Model ofRAM .................................................................. 143 7.3.1 Explicit HAAD model ofRAM. ....................................................................... 144 7.3.2 An implicit HAAD model ofR AM .................................................................. 149 7.4 VHDL Model of interface transducer ....................................................... .153 7.5 Putting it all together ................................................................................. .153 7.6 Static Interface Tuning Verification .......................................................... .155 7.6.1 nv Modeling ofA RM7 READ-WRrtE Scenario .......................................... 157 7.6.2 !IV Modeling ofR AM READ-WRITE Scenario ............................................. 158 7.6.3 !IV Modeling of Clock Generator and Interface Logic ................................. 159 7.6.4 Debugging the Interface Logic with nv. ....................................................... 159 vii Hierarchical Annotated Action Diagrams 7.6.5 Closing Remarks on IrV ................................................................................ 165 8 Summary and Recent Developments ••••••••••••••••••••••• 167 8.1 Summary .................................................................................................... 167 8.2 Recent Developments ................................................................................. 168 8.2.1 Port-based begin and end actions .................................................................. 168 8.2.2 Static timing verification ................................................................................ 171 8.3 Future Directions ........................................................................................ 171 References ........................................................................ 173 A Grammar of the HAAD Language ......................... 183 A.1 Conventions ................................................................................................ 183 A.2 Semantic Notes ........................................................................................... 185 A.2.1 Generics ......................................................................................................... 185 A.2.2 Name Spaces .................................................................................................. 185 A.2.3 Default Constraint Bounds ............................................................................. 185 A.3 Grammar Definition ................................................................................... 186 B Proofs for Chapter 3 ................................................. 189 B.1 Proof of Theorem 3.1 ................................................................................. 189 B.2 Proof of Theorem 3.2,3.3,3.4, and 3.5 .................................................... .191 B.3 Proof of Theorem 3.6 ................................................................................. 193 B.4 Proof of Theorem 3.7 ................................................................................. 198 B.5 Proof of Theorem 8 .................................................................................... 201 B.6 Proof of Theorem 3.9 .................................................................................2 05 B.7 Proof of Theorem 3.10 ............................................................................... 207 INDEX .............................................................................. 209 viii List ofF igures 2.1 Leaf Action Diagram: beginning of Write of ARM 7 ................ 10 2.2 Equivalent description in HAAD language of Figure 2.1.. ......... 11 2.3 Hierarchy for READ I WRITE cycles of ARM 7 ....................... 17 2.4 HAAD language encoding of Figure 2.3 .................................... 20 3.1 The ADAb term of the Action Diagram in Figure 2.1 ................ 27 4.1 Occurrence time of DON'T CARE specified action .................. 54 4.2 VALID or CONSTANT after DON'T CARE ............................ 55 4.3 Occurrence time of V ALID or CONSTANT inputs ................... 56 4.4 Hierarchical composition operators ............................................ 60 4.5 Output action occurrence time enumeration ............................... 62 4.6 Global structure of a HAAD VHDL process .............................. 66 5.1 Anon-causal specification .......................................................... 76 5.2 Assume in AD2 does not cover commit from 03 to 04 in AD! ................................................................... 77 5.3 Simple composition of commits does not work here .................. 78 5.4 A causal Action Diagram ............................................................ 88 5.5 AD for READ cycle of MC68360 .............................................. 96 Hierarchical Annotated Action Diagrams 5.6 Action Diagram for READ cycle of slave device ....................... 97 5.7 Composition P12 resulting from Figures 5.5 and 5.6 ................. 97 6.1 Excerpt of Figure 6.11 illustrating delay correlation ................ 103 6.2 Network of operators for delay correlation ............................... 105 6.3 The problem, exact and approximate solution spaces .............. 112 6.4 Delay correlation as a source of inconsistency ......................... 118 6.5 An inconsistent system with 100% correlated delays ............... 119 6.6 A specification and a possible block partition .......................... 124 6.7 Partial specification of Device 1 ............................................... 126 6.8 Partial specification of Device 2 ............................................... 126 6.9 AD of a RAM memory ............................................................. 128 6.10 AD of a RAM memory ............................................................. 128 6.11 Action Diagram specification of a memory controller. (End of read cycle -write cycle - beginning of read cycle) ...... 128 7.1 ARM7 - Static RAM interface .................................................. 134 7.2 ARM7 specification for Address, nRW, and ALE ................... 135 7.3 ARM7 specification for MCLK, Data in, and Data out ............ 136 7.4 Memory timing for DATA out (READ) ................................... 137 7.5 Memory timing for DATA in (WRITE) ................................... 137 7.6 RAM READ cycle with combined timing constraints ............. 138 7.7 ARM7 READ template with ALE active ................................. 139 7.8 ARM7 WRITE cycle template with ALE active ...................... 140 7.9 End-of-WRITE-Beginning-of-READ AD of ARM7 ............... 141 7.12 VHDL procedure to increment MCLK cycle count ................. 141 x List of Figures 7.10 AD of Figure 7.9 in HAAD language ....................................... 142 7.11 AD to verify min. pulse width of MCLK ................................. 143 7.13 HAAD hierarchy of explicit memory model ............................ I44 7.14 RAM End-of-WRITE followed by beginning of a cycle .......... 145 7.15 RAM End-of-deselected-READ followed by a cycle ............... 146 7.16 RAM End-of-selected-READ followed by another cycle ........ 147 7.17 RAM End-of-selected-READ followed by a deselection ......... 147 7.18 A deselected cycle followed by a deselected cycle .................. 147 7.19 RAM WRITE with Abort_Read and DATA out disable .......... 148 7.20 Exception Condition AD sensing Abort_ltead ......................... 148 7.21 Structure ofimplicitHAAD model ofRAM ............................ 149 7.22 Update of DATA out due to ADDR ......................................... 150 7.23 Update of DATA out due to nCS .............................................. 151 7.24 RAM WRITE and update of DATA out by nWE. .................... 152 7.25 VHDL entity declaration of interface transducer ...................... 153 7.26 VHDL architecture of interface transducer ............................... 154 7.27 Composition of ARM7 and RAM, with delay enumeration ............................................................. 155 7.28 ARM7 READ action graph ....................................................... 158 7.29 ARM7 WRITE action graph ..................................................... 160 7.30 ARM7 READ-WRITE action graph ......................................... 161 7.31 RAM READ action graph ......................................................... 162 7.32 RAM WRITE action graph ....................................................... 162 7.33 RAM READ-WRITE action graph ........................................... 163 xi