PROVING THE CORRECTNESS OF DIGITAL HARDWARE DESIGNS USING PROLOG INFORMATICA i/88 UDK 681.3:325.6.08 Z. Brezočnik B. Horvat University of Maribor ABSTRACT. An approach Is presented for automatic formal verlfication of dlgltal harduare deslgns using Prolog. Prolog is used both as a representatlonal language for specifying the structure and the behavlour of a design and also as an Inference nechanlsin for proving its functional correctness. A design in this model is composed of hierarchicaly organlzed modules. Each module is represented as a flnite state nachine. Validation of design correctness is made by formal proof as an alternative to the traditional approach which utilises simulatlon. The verlfi­ cation proceeds as follows: a) vriting a design specifIcatlon and a description of Its realizatlon in Prolog, b) derivlng a design behavlour from the Interconnectlons of its components and their behavlours, c) shovrlng eguivalence betveen the specifled and the derived behavlour. The syBtem has enough domaln speclfic and general mathenatical knowledge to perform the proofs largely automatically. Designa can be handled from the lovest translstor level up to the architectual levels. Some large deslgns includlng a simple computer haVe already been verlfied. 1. INTRODUCTION A hardvare or softvare deslgner must be able to decide vihether the design meets its functional specificatlon. Currently three different approaches exlst for answering this guestion. The first approach to enshure functional correctness is to develop the design from the specifIcatlon by such a methodology that ensures it can't be incorrect. In softtrare design It is exempllfled in research of automatic programming. In hardvare design automated technlgues eKlst for dealing with elements of deslgns that are most tedious and prone to human error (such as wire routlng or PAL generatlon). Silicon compllation technlgues for automatic generatlon of complete deslgns from specifIcatlons are under development. This approach is perhaps the most attractive, but it is also the most difficult to achleve, because It faces an eventual astronomically large search space of design alternatives. A problem of automatic synthesiB is so difficult, that useful general purpose systems for automatic Bynthesis are not expected in the near future. The second and the most common validate a design is an accurate it and trying it' on test cases. simulatlon every posslble comblnat should be trled for every poss State. The number of ali posslble can be extremely large even for si Amultiplier for two 16-blt intege four bllllon different inputs. It exhaustlve simulatlon is no longer can only select a subset of input hope to extrapolate from them to correctness or fallure of the approach to simulatlon of In exhaustive ion of inputs Ible internal input patterns mple devices. rs faces over s clear that feaslble. We patterns and determine the design. The selectlon of an adeguate subset of test cases is very difficult. Such partial simulatlon can detect the existence of an error, but can never guarantee that there are no nore errors in the design. There is an a formal verlfi mathenatical pro succeds, the des for ali input verlfication in technlgues. It representing the dlgltal systems whlch wlll exper search spaces. depends much on knovledge base. simulatlon and automatic synth the nost promlsi iternative thlrd approach - a catlon of a design with of. If the fornal verlfication ign vili natch its specificatlon patterns. Research in formal volves artificial intelllgence reguires a fornalisn for structure and the behavlour of and also an inference nechanism, tly manage astronomlcally large A success of the verlfication a bullt-ln general mathematical Because of uncompleteness of the a bad prognosis for the soon esls this approach seens to be ng in the nearer tern. Wagner vas a pioneer vith his research in this field. He has used a nonprocedural functional language for dlgltal design description and a theorem prover in a first order predlcate logic. The proof must be guided manually. Because of the description language the use is llmited to lov levels of a design. After that, Gordon has developed his methods for hardvare modellng and verlfication based on different hierarchical levels vith an Interactive theorem prover (1). Inltially., proofs vere made manually, but more recently vith an Interactive theorem prover. In this paper ve present our verlfication system, named VERDIS (2) for formal verlfication of dlgltal hardvare deslgns using Prolog. VERDIS represents an automatlzed version of a 14 variant of Gordon's approach. In Falrchlld Laboratory for Artificial Intelligence the VERIFV svstem was developed based on the slnllar prlnclples (3). VERDIS has successfully verlfled some experlmental deslgns wlth . an Interestlng degree of complexity. some; predefined modules fron the sjrsten llbrary. Let's illustrate some constructs mentioned so far ' by consldering an example of a one-bit multlpller. It's constructed from a collectlon of 2rto-l multlplexors, each of whlch has Inputs inx,\ iny, control Input ctrl and output out. 2. DESIGN REPRESENTATION IN VERDIS % Definition of a one-bit multiplier % terms of 2-to-l auItiplexsors A dlgltal system In VERDIS is represented as a collectlon of hierarchlcally organized modules and thelr Interconnectlons. A module Is consldered as a finite state machlne (FSM) A =1X,Y,Z,5,;»} (1) nodule(bitauIt(N)) . I port(bitmult, ctrl(Bitmult),input, boole). port(bitmult(H),out(BitMult),output, i integer(H)}. It has a finite set of input (X) and output (Z) ports and a finite set of internal state variables (V). VERDIS supports FSM of types Mealy and Moore and also ordinary decision circuits, if y={}- constant(Bitiiiult(H) , i nulKBitmult) ,0,integer(N)) . j part'(bitBult(H), »plx(Bitmult, I), mux2) s- Iindex(0,I,H). A module is either a primitive with no internal structure (basic building block of the design) or composition of the form I I(Ni,..,Nu), where the components N The input (output) po are the input (output) Compound modules are output ports of some ports of other compone module are those ports port has an associ specifies the domain f it. Signals in dl differently according which they are conside logic values ,as bit higher-level objects. folloving types: are themselves modules. rts of a compound module ports of its components. formed t3y linking some components to some input nts. External ports of the that are not linked. Each ated signal type which or signals passing through gital By8tem are vieved to the conceptual level in red: as voltage levels, as , as numbers or even as Signals in VERDIS may have -booole (Boolean truth values true or false) -bit (binary dlgits 0 and 1 ), -integer(N) (integers in the range 0-2 •^•*»-l ), -integer ( natural numbers), -booleZ, bitZ, integerZfN) and integerZ (high impedance signal types). Structural and signal hierarchy allow more succint description. Signals on a higher hierarchical level don't show unneces&ary details of lover-level signals, but cary the same Information. Por conciseness the behaviour of described by two sets of eguations an exhaustive table: D^y = 5(x,y) z = A(x,y) xex, yeY xsX, ysY, zsz Eguation (2) gives Internal states a of inputs and current state. Eguati output signals as functlons of current state. A dictionary of functlons that can be used in expr describlng module behaviour current of arithmetlc {*,-,*,"> , logic (not and branchlng functlons (if,case) an special functlons for such operation signals on a bus and work wlth memor bushfn, rfetch, fetch,store,...). the FSM is , rather than (2) (3) s functlons on (3) gives inputs and available essions for ly consists ,and,or,xor) d also some s as wlring les (joinfn, Module definition consists of Prolog facts and rules. In addition to constructs for specifying type of the module, ports, states, components, Internal connectlons and behavioural eguations the description language supports seversl useful constructs: constants, parameters, arrays, bit- wise connectlons and egu operator for calling linked(bitBult(H),bit(I,in), • inx(aplx(Bit»ult,l)))s- index(0,I,H>. linkedCbitmult(N), ctrKBimuIt, I), ctrl(mplx(Bitault, I))) t-index(0,I,H). linked(bitvtult(H), out (mplx(BitmuIt, D), bita,out (Bitmult))) s- index(0,I ,H) . output_eguation(bit»ult(N), out(Bit»ult) t" if(ctrl(Bitault), in(BitmuIt), nulKBitmult))) . In this example, N is a parameter speclfying the |bit vide of the multiplicand (i.*., the most I significant bit represents 2*^). Due to declarative pover of Prolog a suitable indexing of part and connectlons can be usad. The construct index(0,I,N) means simply that I can take |any value from O to A/ . givan the and thelr 3. THE VERIFICATION PROCESS The jkey princlple of VERDIS is that behaviour of components of a system lnter;connBctions, it is possible to derlve a deEcr|lption of the behaviour of the vhole system. The derived behaviour can then be compa.red with a specification of the intcnded behaviour of the system. If a design contalns an error, a discrepancy betveen both behaviours can be detected and the design corrected. i Before of the verification some basic checks are made to enshure that nontristate outputs ara not Hired, that connected signals have eguivalent types, that every output and state variable has an eguation ... . These checks have proved to be very | useful in finding typing and logical mistakes in design specification. On reguest for checks, if the has been already proofj is not n succeeds immed primitive, its the correctness ušes a depth flr each pt its part verification correctness proved, in ecessary an iately. If correctness of a module st search to and then The next derlve a module fr with thei module ha eguations. in fact an module. I at parts of compone informatio substituti step in verifyin behavioural descrl om the behaviours r interconnectlon s a set of output The unlon of ali impllcitly speci t contalns interna inside the module nt modules). The n should be hidden ons of interna of a module VERDIS of this module type vhich časa anothar d the verification a modula la a can be assumad. If is unknown, VERDIS racurBivaly varify module as a uhole. g a module is to ptlon of a coapoBlte of its components s. Each component and a set of state these eguations is fied behaviour of a 1 variables (algnals and state variables unnecessary internal With subseguent 1 variables with 15 behaviour equations of conponent inodules ali internal variables are eliminated. If any frequently used Internal variable has a very compllcated eguatlon it niay be better not to eliinlnate it to avoid even larger eguatlons. In such cases VERDIS first derives and evaluates the expression for the imnediate variable and refers to it In behaviour eguatlons of the module where needed. The final result of this step is a set of derived output equations and a set of state eguatlons. At this point we can' try to prove that the derived behaviour description of the module is eguivalent to the behavioural specification. In most cases a mapping betveen them is an exact eguivalence - isomorphism. We have to show that corresponding eguatlons in both automata are Identical. The proof of identity is generally a hard problem. It regulres much mathematlcal knowledge about functlons, which can be used in eguatlons. In more complex cases the correspondence betveen automata is a homomorphism rather than exact eguivalence. A may have a structural or a form or both. Structural occurs, when automata are identical but different in structural description. Behavioural or temporal homomorphism occurs, vhen the same automata is vieued with different time-scales. VERDIS currently vorks only for isomorphic machines. The derived and the specifled behaviour are compared for each output and each state. Proof of design correctness regulres the ability to prove that a given . eguatlon (specified behaviour as a left side and derived behaviour as a right side )is an identlty. The eguatlon is first checked to see vhether it is recognized as a trivial ldentity or vrhether it is a'' trivial non-ldentlty. If the eguatlon is not trivial, VERDIS trles to choose the best strategy for proving the lndentlty. A strategy selectlon depends on a form of left and right side of the eguatlon and on function, operators and types of the variables involved. The repertoire of strategies contalns: algebraic simplification, Boolean canonlcalization and enumeration. homomorphism behavioural homomorphism functionally Algebraic simplif strategy, which t left and right simplificatlon, Simplification is recursive Prolog simplifies a simplificatlon ru and functlons. Exp is observed on on The definitlon substituted for expreBsion is simp to deal with comb commutatlvity an functlons (*,*,and ication is the mo ries to prove the side of the egua xpansion and canoni Implemented ulth procedure that given expreBsi les for the involve ansion is used when ly one side of the of the function its call and the lified. Canonicallz Inatorial problems d associativity or...) . st general identity of tion with calIzation. a general recursively on using d operators a function eguatlon. is then resulting ation trles because of of some If only Boolean variables occur in the eguatlon a more straightforuard strategy of Boolean canonicallzation Is chosen. During six subseguent steps the left and the right side of eguatlon are transformed to a lexically ordered complete dlsjunctive normal forms and then compared. It's faster than algebraic simplificatlon. Sometimes no other strategy but enumeration may be applied. An enumeration is made over a minimal necessary number of variables. For a selected set of variables each possible combination of thelr values is generated and substituted into the eguatlon, whlch is then slmplified to 'true' or 'false'. In some special cases it's not necessary to generate ali possible combinatlons but.only some of then. Partial enumeration may save much computatlon. VERDIS avoids the use of enumeration, because it's usually very space and tirne consuning. If VERDIS doesn't have enough knotiledge to select a strategy, an Interactive mode is entered. Currently a user can Inslst in the algebraic simplificatlon, in the enumeration on ali or just some of the variables and can also slroply asBume the eguatlon to be true or false. It's always possible to enlarge VERDIS's knovledge base and automatlze the 'strategy selectlon for such cases. Proving ldentlty of an eguatlon is the maln and the most difficult problem in the verificatlon process. The use of any procedural programming language with deterministic organlzatlon vould not be a natural way for solvlng this problem. This fact is one of the most signlflcant arguments for realizatlon of VERDIS wlth the nonprocedural language Prolog. A Prolog program is a pattern dlrected system. The proof proceeds wlth an activatlon of that verificatlon rule which is currently appliable to the left and to the right side of the eguatlon. Such realizatlon has a high degree of modularity. The knowledge base can simply be enlarged by adding new rules uithout any other changes. 4. TUO COnPLEX EKAMPLES VERDIS has tackled some complex designs includlng modules d74 and hosi. d74 Is an arithmetlc unit( inputs inA, inB, ii>C and outputs outl and out2), vhich is intendend to compute sums of products. outl = inA»inB •*• inA»inC out2 = inA*inC -^ inB«inC At the top level and two adders. slices, each of multiplier, a shi are bulIt from ful invertors and 2-to are bullt from log themselves describ algebra level and tristate signala parameterlzed in b that has a^-bit i types of module w hierarchy. The d parts, includlng llstlng of the pr lines. it contalns thre The multiplier which contaln fter and an adde ladders, vhlch -1 multiplexors. ic gates. The 1 ed at two levels at loHer transis and stored cha lt-wide of input nputs involves Ith nine levels esign contalns 1 1016 translstors oof trace occupl e multlpliers consist of a one-bit r. The adders are built from Multiplexors ogle gates are at Boolean tor level vith rge. d74 is s. An instance 21 different of structural 902 primltive The entire es about 1300 The next example is a reglster-transfer level description of a simple computer host ulth eight operations: HALT, JMP, JZRO, ADD, SUB, LD, ST and NOP. The computer is divided into a control sectlon and a data section. The data section is built upon a single 16 bit data bus. Slx register ( the program counter, the accumulator, the instruction register, the argument register, the buffer register and the memory register) and also an arlthmetic-logic unit and RAM are connected to the bus. The control section contalns a mlcroprogram ROM, a microprogram counter and a microinstruction decoder. VERDIS has proved the correctness of this computer at the microinstruction level. S. DISCUSSION OF THE RESULTS VERDIS is a large Prolog program that occuples about 61 kbytes of code for interpretation. It currently runs on a VAX 8800 under ISJ Prolog interpreter (4). 16 The maln restriction on the coinplexlty of esanples which currently can be tackled is the (3^ amount of vorkspace reguired by Prolog. To deal with large systems, it is nece5sary to verify them a pleče at a tlme or to restart verlfication uhen it aborts due to lack of (4) space. Slnce VERDIS promptly records the progress of verlfication in the database, restartlng does not result In dupllcatlon of (5) work. Due to the hlerarchlcal decompositlon of design description the work done in provlng the correctness of a complete systein Is llnear in terms of the number of types of module in Its design, rather than llnear In terms of the number of prlmltive components. For complex designs wlth Dany thousands of prlmltive coaponents, the computatlonal savlng can be very great. At present, the program performs only functional verlfication, wlth no consideratlon of tlmlng. It appears relatively straightforvard to introduce the notatlon of tlme in our description, but addlng the approprlate inferentlal machlnery wlll probably regulre more effort. Hovever, dealing with truly asynchronous systems regulres a rather different approach with revision of the representatlon and proof mechanism, perhaps In dlrectlon of a temporal loglc (5). The verlfication in VERDIS runs largely automatically, what Is an advantage in comparison with the Gordon's approach, where the proof has to be guided by a user. VERDIS can be compared with a sinilar syBtem VERIFV which has been developed In the Falrchild Laboratory for Artificial Intelllgence. VERDIS Introduces some useful new elemente; posslbility of macro calls for predefined modules in the system library; retaining of Internal variables with over- complex expresslons (l.e. bus output ), new verlfication strategies of Boolean canonlcallzation and partly enumeration, more heuristics in varlable selection for the enumeration etc. 6.C0NCLUSI0N VERDIS is our first attempt of formal verlfication uhlch has already shovn that dlgital designs with an Interesting degree of complexity can be handied. It should be trled on many other real designs and it's knowledge base should be enlarged to become a real design tool, but ablllties of this approach are yet evldent. The decislon for Prolog as a description and an Implementatlon language seems to be correct. Pattern matchlng and backtracklng in Prolog are very poverful tools in the verlfication process. VERDIS is currently Interpreted on a VAX 8800 under IJS Prolog Interpreter(4). If we have any Prolog compller, the speed of execution of the compiled code wlll increase ten tlmes at least. VERDIS should be only one component of larger system supportlng hardware designs. This would integrate programs for design entry, slmulation, verlfication, dlagnostlcs etc. Maribor, November 1986 H. G. Barrow, VERIFV: A Program for Provlng Correctness of Digital Hardvare Designs, Artificial Intelllgence, Vol. 24, No. 1-3, December 1984, 437-491 jj. Stojanovskl, IJS Prolog Reference Manual, Institut Jožef Štefan, LJubljana, 1986 i3.C.MoszkowGkl, A temporal loglc for reasonlng about hardware, Procedlngs isixth International Symposium on Computer Hardvare Description Languages, Carnegle- Mellon Unlverslty, Plttsburgh, 1983, 79-90 REFERENCES (1) H. Gordon , J. Herbert, Formal hardvare verlfication methodology and its application to a netvork interface chip, lEE Proceedlngs, Vol. 133, Pt. E, No. 5, September 1986, 255-270 (2) Z. Brezocnlk , Hardvare verlfication, Master thesis. Tehniška fakulteta.