Lecture Notes ni Computer Science Edited yb .G Goos and .J Hartmanis 582 I I I Carlos Delgado Kioos scitnameS of latigiD Circuits I I galreV-regnirpS nilreB Heidelberg kroYweN Paris London oykoT Editorial Board D. Barstow W, Brauer .P Brinch Hansen D. Gries D. Luckham C. Moler A. Pnueli G."Seegm(Jller .J Stoer N. Wirth rohtuA Dr. Carlos Delgado Kloos Superior Escuela T~cnica de Ingenieros de n6icacinumoceleT Universidad Polit6cnica de Madrid Ciudad Universitaria, E-28040 Madrid, Spain CR Subject Classification (1987): B.5.2, B.6.3, B.7.2, D.1.1, D.3.1 ISBN 3-540-18540-2 Berlin Springer-Verlag Heidelberg New York ISBN 0-387-18540-2 Springer-Verlag New Berlin Heidelberg York Library of Congress Cataloging-in-Publication Data. Kloos, Carlos DelgadoS.e mantics of digital circuits, (Lecture notes in computer science; 285) Bibliography: p, .1 STREAM (Computer hardware description language) 2. Digital integrated circuits. I, Title. .1I Series. TK7885,?.K56 1987 621,39 87-28629 ISBN 0-387-18540-2 (U.S,) This work is subject to copyright. All rights are reserved, whether the whole or part of the material is concerned, specifically the rights of translation, reprinting, re-use of illustrations, recitation, broadcasting, reproduction on microfilms or in otherw ays, and storage in data banks. Duplication of this publication or parts thereof is only permitted under the provisions of the German Copyright Law of September 9, 1965, in its version of June 24, 1985, and a copyright fee must always be paid. Violations fall under the prosecution act of the German Copyright Law, © Springer-Vedag Berlin Heidelberg 1987 Printed in Germany Printing and binding: Druckhaus Beltz, Hemsbach/Bergstr. 2145/3140-543210 oT orahC Preface ehT theory of formal scitnames for gnimmargorp segaugnal saw depoleved for precisely defining the function of retupmoc .smargorp This helped to construct better smargorp dna to verify meht with respect to a specification. It sah won emoceb evident that a similar treatment is yrassecen for digital circuits. In this koob ew want to vLal a formal foundation, desab no a single emehcs egaugnal for formally describing the behaviour of digital systems, nopu hcihw a ygolodohtem of ngised dna tnempoleved of digital circuits nac eb built. oT this dne ew present a ,egaugnal hcihw ew call ,I~AERTS for the description of concurrent systems. It allows to describe finite nets of stream gnissecorp functions. After giving the syntactic dna citnames definition of eht ,egaugnal with parametrised the underlying niamod of values, ew wohs woh larudecorp smargorp nac eb delledom with it. nehT ew focus ruo attention no different description levels in the process of the design of VLSI (Ve~ Large elacS Integrated) circuits, dna give the sniamod no which the MAERTS egaugnal sah to eb ,desab together with emos additional smsinahcem specifically dedeen for the different s. level gniwolleF a nwod-pot ,hcaorppa ew first study the register transfer level dna describe the ruoivaheb of suonorhcnys seludom dna registers in the MAERTS .egaugnal nehT ew consider eht gate level, at hcihw lanoitanibmoc dna sequential circuits nac eb constructed from gates. eW concentrate here no suonorhcnysa circuits, giving a formal foundation, based no fixpoint theory, of the ternary analysis seuqinhcet for drazah detection. ehT immediately lower level is eht switch level, modelling SOM (Metal Oxide )rotcudnocimeS circuits in terms of transistors, resistors, dna capacitors. nevE at this level, ew nac esu the MAERTS ,egaugnal but won it is desab no a richer niamod than the niamod of naeloob values. ehT koob closes with a review of related work, emos general observations no transformational ,tnempoleved dna emos hints for future research. It is a pleasure to thank ym former colleagues of the PIC group at the Institut for Informatik red nehcsinhceT Universit~t ,nehcnOM ohw have definitely dah a strong influence nopu this work. In particular, I wish to thank F.L. Bauer, .M Broy, .W ,hcsoD .B MBller, ,dna especially, .H renssBW for their constructive criticism dna valuable help. sknahT og also to .H Ehler, T. Tensi, dna to the students of a ranimes desinagro yb F.L. reuaB dna .W hcsoD for useful remarks. I la os want to express ym gratitude to ym present seugaelloc of the Depto. ed Ingenierla Telem~tica ed la Universidad Polit~cnica ed Madrid for their stnemmoc dna to galreV-regnirpS for their support. ,dirdaM/hcinuM tsuguA 7891 .C odagleD soolK Table of Contents 1. NOITCUDORTNI 1.1. deeN for a formal description of the behaviour of (integrated) circuits ......... I 1.2. Software dna design hardware .................................................... 1 1.3. dnAims a organisation of this book .............................................. 3 2. EHT M#ERIS EGAUGNAL 2.1. Introduction .................... ................................................ S 2.2. Syntax .......................................................................... 5 2.2.1. Streams .................................................................. 5 2.2.2. Primitive agents ......................................................... 6 2.2.2.1. gnidneppA a value ............................................... 6 2.2.2.2. Repeating a function ............................................ 7 2.2.2.3. Distributing values ............................................. 7 2.2.2.4. Selecting values ................................................ 8 2.2.3. Composition of agents .................................................... 9 2.2.3.1. selpmaxE ........................................................ 9 2.2.3.2. Applicative style ............................................... 11 2.2.3.3. Functional style ................................................ 21 2.2.3.4. nO the composition styles ....................................... 41 2.2.3.5. Syntactic definition ............................................ 51 2.3. Semantics ....................................................................... 61 2.3.1. domains Semantic ......................................................... 61 2.3.2. Semantic definition ...................................................... 02 2.3.3. Example .................................................................. 12 2.4. emoS useful composite agents .................................................... 22 2.4.1. Extensions of the forking agent .......................................... 22 2.4.2. Extensions of the permuting agent ........................................ 32 2.4.3. A synchronizing agent .................................................... 42 2.4.4. Double rail distribution ................................................. 52 2.4.5. rotatummoC ............................................................... 62 2.5. Transformation rules ............................................................ 62 2.6. Final remarks ................................................................... 82 3.L ARUDECORP LEVEL STNEGA 3.1. Introduction .................................................................... 92 3.2. A simple procedural language .................................................... 92 3.2.1. Syntax ................................................................... 92 3.2.2. Example .................................................................. 03 3.2.3. Semantics ................................................................ 03 3.3. Relating the procedural dna the q~ERTS language ................................. 33 3.4. Example ......................................................................... 24 3.5. Final remarks ................................................................... 34 VIII 4. RETSIGER REFSNART LEVEL STNEGA 4.1. Introduction .................................................................... 54 4.2. Mode]ling synchronicity ......................................................... 54 4.3. Modules ......................................................................... 84 4.3.1. Unconditional routing modules ............................................ 94 4.3.1.1. Shift modules ................................................... 49 4.3.1.2. Other modules with permutation .................................. 05 4.3.1.3. Divergence and convergence modules .............................. 15 4.3.2. Conditional routing modules .............................................. 35 4.3.2.1. Demultiplexor ................................................... 35 4.3.2.2. Multiplexor ..................................................... 55 4.3.3. Processing modules ....................................................... 55 4.3.3.1. Code transformers ................... ............................ 55 4.3.3.2. Logic dna arithmetic modules .................................... 75 4.4. Registers ....................................................................... 85 4.4.1. ehT D-flip-flop .......................................................... 85 4.4.2. ehT RS-flip-flop ......................................................... 95 4.4.3. ehT JK-flip-flop ......................................................... 16 4.5. Register transfer networks ...................................................... 26 4.6. Final remarks ................................................................... 36 5. ETAG LEVEL STNEGA 5.1. Introduction .................................................................... 56 5.2. Combinational circuits .......................................................... 66 5.2.1. Stationary behaviour ..................................................... 96 5.2.2. Transitory behaviour ..................................................... 96 5.2.2.1. Transitions ..................................................... 69 5.2.2.2. Hazards ......................................................... 17 5.2.2.3. Ternary extension of a boolean function ......................... 37 5.2.2.4. Fine modelling .................................................. 57 5.2.2.5. Coarse modelling ................................................ 77 5.3. Sequential circuits ............................................................. 97 5.3.1. Ternary functions ........................................................ 97 5.3.2. Transitions in sequential circuits ....................................... 28 5.4. Final remarks ................................................................... 78 6. HCTIWS LEVEL STNEGA 6.1. Introduction .................................................................... 98 6.2. ehT basic domain for the switch level ........................................... 98 6,2.1. Power supplies ........................................................... 89 6.2.2. Resistors ................................................................ 19 6.2.3. Switches ................................................................. 59 6.2.4, Capacitors ............................................................... 69 6.3. Modelling switch level elements with the MAERTS language ........................ 69 IX 6.3.1. Connectors ............................................................... 96 6.3.2. Power supplies ........................................................... 97 6.3.3. Resistors ................................................................ 97 6.3.4. Switches ................................................................. 104 6.3.5. Capacitors ............................................................... 901 6.4. Modelling switch level networks ................................................. 111 6.5. Non-regular situations .......................................................... 211 6.6. Final remarks ................................................................... 311 7. NOISULCNOC 7.1. Related work .................................................................... 511 7.2. Development by transformation ................................................... 611 7.3. Further research directions ..................................................... 711 7.4. Bibliography .................................................................... 811 I. Introduction 1.1. Need for a formal description of the behaviour of (integrated) circuits secnavdA in eht ygolonhcet of silicon gnissecorp evah edam it possible to fabricate silicon spihc with a ytixelpmoc of over a million active ,stnemele dna this rebmun is still .gnisaercni This gives rise to the possibility of integrating very xelpmoc circuit sngised no very llams saera (far smaller naht a erauqs centimeter). This potential cannot eb fully exploited if it is not deinapmocca yb na etauqeda ygolodohtem for formally gnipoleved these designs from functional specifications or at least a dohtem for formally verifying eht correctness of eht ngised with respect to eht original specification. htiW eht elbakramer work dedaeh yb .C daeM dna L. yawnoC (cf. especially ,daeM/ yawnoC )/0891 a gib step in this direction sah neeb edam yb separating eht snrecnoc of design dna fabrication dna yb gnisoporp a structured ngised .ygolodohtem tuB still eht lacitamehtam snoitadnuof of hcus a ygolodohtem have ton neeb denifed properly yet. Both smargorp dna circuits era snoitatnemelpmi of ,smhtirogla the first suitable being to eb nur no a lareneg esoprup retupmoc dna the dnoces to eb etched into silicon (for ,elpmaxe or realized with standard "off-the-shelf" ,stnenopmoc etc.). From this ygolana it is ton surprising that essentially eht emas seuqinhcet that evah neeb desu in the last twenty sraey to emocrevo eht "software crisis" for laitneuqes smargorp /Bauer 71/ era won starting to eb deilppa to retsam what dluoc eb called the erawdrah" crisis". fO this course requires gnitpada meht to eht wen ,muidem yb taking ,ycnerrucnoc ytilanoisnemidib (actually there is a finite rebmun of lanoisnemid-owt layers), cificeps-ygolonhcet issues, etc. into .tnuocca ,revoeroM it is of ton hcum esu to evah verified software if it is going to eb detucexe no non-verified .erawdrah woN that eht scitnames of laitneuqes smargorp is fully dootsrednu dna the scitnames of concurrent smargorp also semoceb ,dootsrednu eht time sah emoc to look at eht scitnames of digital circuits. 1.2. Software dna hardware design retupmoC science sah depoleved from the erawdrah to eht software side. It saw ton satisfactory to margorp sretupmoc in enihcam egaugnal dna os high-level segaugnal erew defined. euD to this historical origin, these segaugnal were strongly influenced yb eht nov nnamueN architecture: they were sequential dna imperative at the .gninnigeb Writing hcus a margorp saw dediug yb eht capabilities eht enihcam offered, instead of yb eht ideas no woh to evlos the particular .melborp nehW software dah to eb decudorp in great quantity, a deen arose for a ygolodohtem to ngised ,smargorp dna meht ngised correctly. A margorp saw then deredisnoc a product to eb ,depoleved dna engineering techniques, including rules of discipline dna structure, were applied. Afterwards lacitamehtam sdohtem were used, thus converting a margorp into a formal object tuoba hcihw smeroeht could eb .devorp ehT secnavda in integrated circuit fabrication led have to a situation in hcihw it is possible to ecudorp xelpmoc circuits with hcus positive features :sa sm~l size, wol rewop ,noitpmusnoc high ,deeps paehc materi~, etc. Therefore ew era won in a similar situation sa eht software sector was. At eht gninnigeb of this ,edaced the first seigo~dohtem ,deraeppa which for the first time less gave importance to efficiency dna tnenopmoc count dna stressed the ngised aspects, niaga including rules of discipline dna structuring, dna separation of .snrecnoc htiW eht experience deniag in software, a rebmun of sehcaorppa era gniraeppa which apply formal sdohtem to eht niamod of .erawdrah In doing ,os emos of eht doog gnireenigne practices that resulted from ecneirepxe will the have opportunity to emoceb mathematically justified. tuB the greatest epoh is that the design ssecorp of VLSI systems will emoceb better ,dootsrednu that ngised seuqinhcet will arise that preserve correctness dna that the precise ruoivaheb of circuits nac eb formally defined dna .deetnaraug ehT software life cycle contains eht different steps a design of a margorp seog through from its informal definition to its esu dna adaptation to wen requirements. emoS of these steps are: infor~l stnemeriuqer formal (pre-algorithmic) specification high-level algorithmic margorp versions (applicative, imperative, ...) low-level algorithmic margorp versions ,yl~Wnessa( enihcam code, ...) ecnanetniam roF assuring correct smargorp either a constructive dohtem hcus sa margorp transformation, or na a posteriori dohtem hcus sa margorp verification nac eb .detpoda In erawdrah ,ngised a rebmun of different levels to og through nac also eb identified. esehT levels era characterized yb different seerged of detail in several :stcepsa emos stnenopmoc era detoned yb their extensional behaviour or defined sa a noitisopmoc of stnenopmocbus (function abstraction or concretisation) the niamod desu in the interpretation is finer or coarser (abstraction or concretisation of the basic )niamod the gnicneuqes or neve timing issues era given in erom or less detail (timing abstraction or concretisation) roF historical dna practical snosaer eht following levels era ylnommoc distinguished (see, e.g. /Bell, lleweN 71/): the register transfer level, characterized yb words of binary values of fixed le ndgtnh a registers, seludom dna transfers; the gate level, characterized yb eht laws of naeloob algebra dna additional ;smsinahcem the switch level, in hcihw eno with deals a simplified ledom for rewop sources, transistors, resistors, dna capacitors, dna yam yolpme a multivalued logic. evobA the register transfer level ew dealw ith systems that n aecb described yb smargorp in the classical sense. woleB eht switch level ew nac on longer og into erom detail in function dna put must erom topological dna geometrical issues into eht design. eowS the have level of stick diagrams (symbolic layout or topological level) dna of sksam (geometric layout or cirtemoeg level). ehT erom a tnenopmoc is specified in terms of ,stnenopmocbus ew era htob gnivom nwod to erom primitive ;stnenopmoc including erom structural stcepsa into the .ngised oS no the yaw from a functional specification nwod to the sticks level, ew era putting in erom structure. If ew abstract at the sticks level from the gninaem of the primitive elements, ew only have structure, dna if ew abstract from the structure, ew only the have ruoivaheb of the circuit in the form of a function. gnisopmI a concrete metric to the structure converts it into a .yrtemoeg e heTsu of several levels of abstraction is a nommoc dohtem to epoc with xelpmoc systems, to analyse dna design them. Its limitations must also eb seen. ehT higher the level ew are gninosaer in, the less flexible ew are to esu wol level efficiency considerations. ,revewoH these aspects era sacrificed in favour of the ability to fully dnatsrednu a design at every tnemom of the .tnempoleved ehT tnempoleved through eht different levels should eb enod within eno single .krowemarf ehT tnempoleved will eb hierarchical with respect to the egaugnal levels, but also allowing eno to ekam transformations within each level. This hcaorppa is called almst hierarchical in ,namssuS/ Steele 80/. It allows eno to gain erom efficient ,snoitatnemelpmi esuaceb hguohtla ew might ton esu in eno level efficiency considerations from eht level ,woleb what ew can od is tnemelpmi a tnenopmoc yb wol level primitives dna then ekam transformations within the lower level leading to erom efficiency (in time and/or space). 1.3. Aims dna organisatton of this book In this ,koob ew present eht MAERTS ,egaugnal hcihw will serve sa a nommoc skeleton for the different levels of erawdrah description. Using eno single krowemarf is the best yaw to erapmoc the different erawdrah ngised levels dna put them into relation. This also allows to eventually transformations preserving perform correctness gnoma .meht