当前位置：文档之家 › Creating a Formal Verification Platform for IBM CoreConnect-based SoC

Creating a Formal Verification Platform for IBM CoreConnect-based SoC

  • 格式：pdf
  • 大小：214.34 KB
  • 文档页数：12

Creating a Formal Verification Platform for IBMCoreConnect-based SoC∗Wen-Shiu Liao and Pao-Ann Hsiung†Department of Computer Science and Information EngineeringNational Chung Cheng University,Chiayi,Taiwan-621.†hpa@AbstractHow to ensure functionality correctness in an SoC chip is a troublesome issue.This is because SoC is so complex that it is difficult tofind errors in corner cases.Thus,bugs mayexist even after thorough simulation and emulation.In contrast,formal verification provides100%coverage with counterexamples and is expected to be a complementary solution.Hence,many researchers and designers are trying to apply formal verification to SoC design in ordertofind errors as early as possible.The current status-quo is that there are only isolated tools,but no integrated environment for the formal verification of VLSI designs.Here,a Formal Ver-ification Platform(FVP)is proposed,which allows designers to configure a formal verificationenvironment representing the SoC in which a user-designed Intellectual Property(IP)is to beintegrated.We illustrate how to create a formal verification platform for an IBM CoreConnect-based SoC in this work.1IntroductionSystem-on-a-Chip(SoC)design is getting more and more popular in the recent years.However,how to ensure an SoC product satisfies its specification is becoming a serious problem.Due to the design complexity in SoC,traditional verification methods must generate huge numbers of test patterns to test the functionality of an SoC design.With traditional verification,some bugs may still exist even if an SoC passes the tests.To get rid of the verification crisis in an SoC design,many researchers ∗This work was supported by project grants NSC91-2215-E-194-008,NSC92-2218-E-194-009,and NSC91-2213-E-194-008,NSC92-2213-E-194-003from the National Science Council,Taiwan.are trying to apply formal verification to SoC design.The advantages of formal verification are (1)it provides more confidences by exhaustively traversing whole system state spaces,and(2) when a system fails to satisfy a property,formal verification will produce a counterexample to indicate where the bug is.Several efforts on formally verifying hardware or SoC indicate that verifying a large system by using formal methods is feasible[1],[2],[3],[4],[5],even though formal verification has its own share of problems such as the famous state-space explosion issue.Often,in a platform-based SoC design,a system designer integrates some pre-designed and verified Intellectual Properties(IP)with one or more user-designed IP.In order to efficiently reuse IPs in an SoC,an on-chip bus(OCB)architecture such as AMBA[6]or CoreConnect[7]is essential. Often,a typical OCB architecture is composed by two buses:a processor local bus(PLB)and an on-chip peripheral bus(OPB).Each bus has some IPs attached and a bus arbiter to control the bus.The bus bridge enables data communication between the buses.For formally verifying a user-designed IP,a designer needs to also model the SoC environment in which the IP will be embedded.Thus,it is desirable that we have a platform in which formal verification can be done.To complement a system designer’s efforts in formally verifying an IP,a Formal Verification Platform(FVP)[8]is proposed,which provides cycle-accurate modeling and verification.The article is organized as follows.Section2introduces a formal verification platform for SoC. Section3describes the system model and the property definition that are used in our formal ver-ification platform.Then,we demonstrate how we model hardware systems with clock models. Section4discusses the issues encountered in the creation of a formal verification platform for IBM CoreConnect-based SoC and the corresponding solutions.Section5concludes with future work.2Formal Verification PlatformDue to the inefficiency of traditional hardware verification methods and the increase in design com-plexity,formal verification is getting more and more attention in recent years.As summarized below,there are some issues unresearched in the current state-of-art on formally verifying an SoC.(1)Some model checkers like SMV has only one implicit clock,a designer has to make some tricks when modeling an SoC with two or more bus frequencies or with gated clocks[3].(2)Currently, there is no utility for platform-based formal verification of SoC.(3)The state space explosion issue is still a major bottleneck in formal verification.To handle above issues,we choose State Graph Manipulators(SGM)[9]as the verification……...Figure1:FVP Architecturekernel for our FVP.SGM is a high-level compositional model checker with multiple state-space reduction techniques for the verification of real time systems.In SGM,a system is described by a set of communication Extended Timed Automata(ETA)[10]and a property is specified by Computation Tree Logic(CTL)[11].We can model hardware behavior with multiple clocks or a gated clock in the timed automata model.In SGM,the global system state-space is computed iteratively by composing one timed automaton at a time.Thus,it is natural to treat an IP as a timed automaton in SGM.Figure1illustrates the architecture of FVP consisting of three components:SoC environment configurator,SoC system integrator,and SGM kernel.The given order is the sequence in which they are used.A user sets up an SoC environment using the SoC environment configurator.After the userfinishes modeling a user-designed IP,the SoC system integrator integrates the user-designed IP model with all the formal IP models that were specified through the SoC environment configurator. As soon as the whole SoC model is integrated,the user can formally verify the SoC using the SGM kernel against user-specified properties.The detailed functionalities of the SoC environment configurator,SoC system integrator,and the SGM kernel are described as follows.•SoC environment configurator:Through the SoC environment configurator,an IP designer can setup all the IPs that constitute an SoC environment for the designer’s own IP model.This configured environment information is stored for later use during the SoC integration phase.For example,a user may select two buses:PLB and OPB,two PLB masters,one bridge,two PLB slaves,and3OPB slaves as an SoC environment for an image-processing IPto be attached on the IBM CoreConnect bus architecture.•SoC system integrator:According to the information saved by SoC environment configurator, the SoC system integrator composes an SoC consisting of the user-designed IP model and all the user-specified formal IP models.Because the ETA model is a closed one,an external environment model is required,for which a formal bench(a-kind-of testbench)is generated by the SoC system integrator.•SGM kernel:The formal model of each IP in SoC is expressed as an ETA.The SGM kernel reads these automata sequentially and merges them one by one to generate the global system behavior of the SoC.The user can use CTL to specify the properties that they are interested in.SGM then uses symbolic model checking technology to verify if the set of ETA satisfiesa given CTL property.If the ETA does not satisfy a CTL property,a counterexample isproduced by SGM.The user can then analyze the counterexample to locate design problems.The verificationflow of FVP is shown in Figure 2.There are three stages in the verification flow of FVP:configuration stage,modeling and integration stage,and verification stage.In the configuration stage,an FVP user begins by specifying his/her SoC environment.After an SoC environment is specified,the SoC environment configurator will check if there is any conflict among the IPs in the assigned SoC.Before integrating the SoC in the beginning of modeling and integration stage,lint checking is provided to avoid any syntax error in the user-designed IP model and to avoid any inappropriate interactions of the user IP model with the formal models.If lint checking fails because of syntax errors,the user must then modify his/her model.The user may also re-configure the SoC environment to correct any inappropriate use of the formal models.After lint checking is done,the SoC system integrator generates thefinal SoC models and a formal bench according to the configuration data,existing formal models,and the user-designed IP model.In the verification stage,the user can start verifying the whole SoC model using the SGM kernel.Either a wrong property specified in SGM,or a wrong configuration,or some bugs in the user-designed IP model may cause the formal verification to fail in SGM.If verification fails,the user must analyze counterexamples manually to decide how to re-formulate properties,to re-configure the SoC environment,or to modify the user-designed IP model.Figure2:Verification Flow in FVP3System Model,Property Definition,and Clock ModelsIn FVP,a system is described by a set of communication Extended Timed Automata(ETA)[10]and a property is specified by Computation Tree Logic(CTL)[11].The global system state-space is computed iteratively by composing one timed automaton at a time.3.1System ModelOur system model is a set of ETA,which have shared variables and synchronization labels and are formally defined as follows.Definition1Mode PredicateGiven a set C of clock variables and a set D of discrete variables,the syntax of a mode predicateηover C and D is defined as:η:=false|x∼c|x−y∼c|d∼c|η1∧η2|¬η1,where x,y∈C,∼∈{≤,<,=,≥,>},c∈N,the set of integers,d∈D,andη1,η2are mode predicates.2Let B(C,D)be the set of all mode predicates over C and D.Definition2Extended Timed AutomatonAn Extended Timed Automaton(ETA)is a tuple A i=(M i,m0i,C i,D i,L i,χi,E i,λi,τi,ρi)such that: M i is afinite set of modes,m0i∈M is the initial mode,C i is a set of clock variables,D i is a set of discrete variables,L i is a set of synchronization labels,χi:M i→B(C i,D i)is an invariance function that labels each mode with a condition true in that mode,E i⊆M i×M i is a set of transitions,λi:E i→L i associates a synchronization label with a transition,τi:E i→B(C i,D i)defines the transition triggering conditions,andρi:E i→2C i∪(D i×N)is an assignment function that maps each transition to a set of assignments such as resetting some clock variables and setting some discrete variables to specific integer values.2 Using the above ETA definition,our system model can be defined as follows.Definition3Hardware SystemA Hardware System is defined as a set of hardware and clock components.Each component is modeled by one or more timed automata.A system is modeled by a network of communicating timed automata.If a system S has a set of hardware components{H1,H2,...,H n}and a set of clock components{C1,C2,...,C m},then S=H1 H2 ... H n C1 C2 ... C m,where is a parallel composition operator resulting in the concurrent behavior of its two operands.If H i is modeled byan ETA A Hi ,1≤i≤n,and C j is modeled by an ETA A Cj,1≤j≤m,then the ETA defined byA S=A H1×...×A H n×A C1×...×A C m is an ETA model for system S,where×is the state-graph merge operation in SGM and concurrency semantics is defined as follows:•two concurrent transitions with the same synchronization label are represented by a single synchronized transition in the product automaton,and•two concurrent transitions without any synchronization label are represented by interleaving them,resulting in possibly two different paths(computations).23.2Property DefinitionProperties are the precise descriptions of the features or behaviors that we want to verify against a user designed system.In FVP,properties are specified in Computation Tree Logic(CTL),which is defined as follows.X = 5CLK_A := 0X:=0X = 5X:=0Y= 10CLK_B := 0Y :=0Y = 10Y := 0TimedAutomaton A Timed Automaton BFigure 3:Multi-rate Bus Clock ETA ModelsX = 5CLK_G := 0X:=0X = 5 && G = 1CLK_G := 1X:=0CLK_G :=0G := 1X := 0X = 5 && G = 0CLK_G := 0X:=0Figure 4:Gated Clock ETA ModelDe finition 4:Computation Tree Logic FormulaA computation tree logic formula has the following syntax:φ::=η|∃ φ |∃2φ |∃φ U φ |¬φ |φ ∨φ .(1)Here,ηis a mode predicate in B (∪n i =1C i ,∪n i =1D i ).∃ φ means there exists a computation such thatφ is true in the next mode.∃2φ means there exists a computation,from the current state,along which φ is always true.∃φ U φ means there exists a computation,from the current state,along which φ is true until φ becomes true,within the time constraint of ∼c .Traditional shorthands like ∃ ,∀ ,∃3,∀2,∀3,∀U ,∧,and →can all be de fined as in [11].23.3Clock ModelsThe details of modeling hardware systems with complex clock synchronization is given in [12].Here,we show how we handle system models with multiple bus clocks and a gated clock.Figure 3illustrates an example of modeling two bus clocks.We use clock variables X and Y to represent the progress of time in the two bus clocks,and register variables CLK A and CLK B to represent the signal outputs of the two bus clocks.In the timed automata A and B ,A0(B0)and A1(B1)represent the states of the bus clocks driven low and high,respectively.The transitions from A0(B0)to A1(B1)represent the change of bus clock level from low to high,which is the positive edge of the bus clock signal.Similarly,the transitions from A1(B1)to A0(B0)represent the negative edge of the bus clock.The different rates of multiple bus clocks in hardware system can be modeled by setting different values to the clock variables X and Y on the transitions.For example,the rate of clock CLK B is twice that of clock CLK A in Figure 3.The initialization of bus clocks can be modeled by setting the initial state of the automata.If transitions in some hardware component models need to be triggered at the positive edge of CLK A ,then the user can synchronize these transitions withthe clock transition from A0to A1in order to guarantee that these transitions will be triggered at the same time.Figure4is a gated clock model.Gated clock is a common technique for low power design in hardware.Register variable G is a control signal that enables/disables the clock.When G is one, the clock operates normally.When G becomes zero,the timed automata will eventually stay in Low-power mode until G becomes one,which represents the gated condition of a clock.4Formal Verification Platform for IBM CoreConnectCoreConnect[7]is an on-chip bus architecture proposed by IBM.It defines a standard for on-chip communications in an SoC design.There are three buses that are defined in the CoreConnect speci-fication:Processor Local Bus(PLB),On-Chip Peripheral Bus(OPB),and Device Control Register Bus(DCR).The PLB is designed for high-performance,high clock frequency system modules.The OPB is designed for high-performance system modules.The DCR is designed for data transfer between CPU’s registers and control/statue registers in the devices.In our current work only PLB and OPB are modeled in our platform.4.1Modeling CoreConnect PlatformTo ensure that the CoreConnect-based formal verification platform is correct,we model it gradually. Thus,thefirst of our CoreConnect platform supports only single bus transactions in PLB and in OPB.Currently,we modeled six CoreConnect components in thefirst version of the platform, including a generic PLB master,a generic PLB slave,a simple PLB arbiter,a PLB bridge,a simple OPB arbiter,and a generic OPB slave.Two bus clock models,PCLK and OCLK,are used to provide synchronizations in the PLB and in the OPB,respectively.Some abstractions are used to reduce the number of states in the CoreConnect component models,without compensating verification correctness or capability.These abstractions are listed as follows.1.Address abstraction:We use a register variable instead of a set of bits in address bus so thataddress decoding is abstracted.When a PLB master decides to access a PLB slave or an OPB slave,it will assign address to let slaves(including PLB bridge)know which slave is chosen by the PLB master.2.Data abstraction:Our focus in verification is on a the intercommunications among IPs onPLB_M1Err = 1M1_rqeuest := 0Figure5:Read Transfer in PLB Master ETA ModelCoreConnect rather than data accuracy.Thus,we do not model data bus in thefirst version of our CoreConnect platform.Figure5is a formal model for a read transfer in a generic PLB master.The timing diagram for a single read transfer is shown in Figure6.The PLB address cycle consists of three phases:request, transfer,and termination.A PLB master will assert Mn request,Mn priority,and Mn busLock signals to get the ownership of the bus in the request phase.A PLB slave will receive address and transfer qualifier in the transfer phase once the PLB arbiter grants the bus to the PLB master by asserting PLB PAValid signal.The maximum length of the transfer phase is controlled by the slave’s SI wait signal and by the PLB arbiter address cycle time-out mechanism.The conditions of the termination phase are either a bus slave asserts SI addrAck,or SI rearbitrate,or a bus master asserts Mn abort,or a bus arbiter deletes a transaction time-out.A normal read transfer will end with receiving the PLB MnrDAck signal.If there is time-out in the read transfer,the PLB master will also receive PLB MnErr in the terminate phase.If the PLB master decides to abort transfer,it can assert Mn abort asynchronously.Thus,we do not synchronize the transition from M1to M21with PCLK,in our model.Figure6:Timing Diagram of Read Transfer in PLB4.2Verifying ourfirst CoreConnect PlatformWe have created a CoreConnect-based SoC environment manually such that the behaviors repre-sented by our models are consistent with the CoreConnect specification[7].The SoC environment is composed by two generic PLB masters,two generic PLB slaves,a PLB bus arbiter,a PLB bridge, an OPB arbiter,and two OPB slaves.For convenience,we assign each PLB slave and each OPB slave a unique address.PLB slaves are assigned to address1or2.OPB slaves are assigned to address3or4.The verificationflow for the platform is shown in Figure7.We begin the verification process by verifying interactions in PLB formal models and in OPB formal models individually.Then, we verify the integration of the whole SoC environment.Some CTL properties checked in our verification process are listed below.•∀2((M1ABus=1∩M1request=1)→∃3(PLB M1rDAck=1)):This property checksthat the PLB slave1willfinish a bus transfer whenever an PLB master wants to access it.TheFigure7:Verification Flow of thefirst CoreConnect Platformformula means as long as PLB slave1is selected,the PLB M1rDAck signal will be asserted eventually if there is no time-out.•∀2((M1request1=1∩M2request=1)→∀ ((PLB PAValid=1)∩(PLB masterID=1))):This property is to verify the priorities in the PLB arbiter.The formula means if PLBmaster1and PLB master2both request a bus transfer at the same time,then the PLB arbiter will grant access to PLB master1in the next clock cycle.•∀2(O M2request=0→∀2O M1Grant=1):This property is to verify the park mecha-nism in the OPB.The bus is parking in OPB master1.Thus,if OPB master2does not makea request,the OPB arbiter will always grant the bus to OPB master1.5ConclusionThrough our experiences in modeling and verifying a formal verification platform for SoC design, we have shown how abstractions can be employed,how properties can be used to validate a platform, and how multi-rate clocks can be modeled and used for verification in an SoC formal verification platform.Our future work will include the design of a second version for our platform that considers burst transaction and other enhancements.Another future work will be the extension to other on-chip bus architectures.References[1]B.Chen,M.Yamazaki,and M.Fujita.Bug identification of a real chip design by symbolic model check-ing.In Proceedings of European Conference on Design Automation,pages132–136,February/March 1994.[2]T.A.Henzinger,X.Liu,S.Qadeer,and S.K.Rajamani.Formal specification and verification of adataflow processor array.In Proceedings of the IEEE/ACM International Conference on Computer-Aided Design(ICCAD’99),pages494–499,November1999.[3]H.Choi,B.Yun,Y.Lee,and H.Roh.Model checking of S3C2400X industrial embedded SoC product.In Proceedings of the38th Design Automation Conference,pages611–616,June2001.[4]P.Chauhan,E.M.Clarke,Y.Lu,and D.Wang.Verifying IP-core based system-on-chip designs.InProceedings of the12th IEEE International ASIC/SOC Conference,pages27–31,September1999. [5]B.Wang and Z.H.Lin.Formal verification of embedded SoC.In Proceedings of the4th InternationalASIC Conference,pages769–772,October2001.[6]ARM Company.AMBA Specification2.0.1999./arm/Tech Specs?OpenDocument.[7]IBM Company.CoreConnect Bus Architecture.2002./chips/techlib/techlib.nsf/productfamilies/CoreConnect Bus Architecture. [8]W.-S.Liao and P.-A.Hsiung.FVP:A formal verification platform for SoC.In Proceedings of the16thIEEE International SoC Conference,pages21–24,(Oregon,USA),September2003.IEEE CS Press. [9]F.Wang and P.-A.Hsiung.Efficient and user-friendly verification.IEEE Transactions on Computers,51(1):61–83,January2002.[10]R.Alur and D.L.Dill.A theory of timed automata.Theoretical Computer Science,126:183–235,April1994.[11]E.M.Clarke,O.Grumberg,and D.A.Peled.Model Checking.MIT Press,1999.[12]W.-S.Liao and P.-A.Hsiung.Modeling hardware systems with complex clock synchronizations inthe SGM formal verifier.In Proceedings of the14th VLSI Design/CAD Symposium,pages177–180, (Hwalien,Taiwan,ROC),August2003.。

合集下载

Formal Verification of MIX Programs

Formal Verification of MIX Programs

Formal Verification of MIX ProgramsJean-Christophe Filliˆa treCNRSLRI,Univ Paris-Sud,Orsay F-91405INRIA Futurs,ProVal,Orsay F-91893AbstractWe introduce a methodology to formally verify MIX programs.It consists in annotatinga MIX program with logical annotations and then to turn it into a set of purely sequentialprograms on which classical techniques can be applied.Contrary to other approaches ofverification of unstructured programs,we do not impose the location of annotations but onlythe existence of at least one invariant on each cycle in the controlflow graph.A prototypehas been implemented and used to verify several programs from The Art of ComputerProgramming.1IntroductionMIX is a machine introduced by D.Knuth in The Art of Computer Programming[5]and equipped with an assembly language.If it looks outdated compared to today’s computers,it is nonetheless a language with a clearly exposed semantics and the vehicle of many algorithms described in this set of books.It is thus quite natural to consider proving such programs in a formal way. Moreover,the techniques involved in the verification of assembly-like programs have direct applications in domains such as Proof Carrying Code[8]or safety of low-level C programs.Our approach to formally verifying MIX programs is built on previous works on the veri-fication of C and Java programs[3].The general idea is to specify a program using logical annotations inserted in its source code,and then to translate the program into an intermedi-ate language suitable for Hoare logic[4].The output is a set of verification conditions,that is a set of logical formulae whose validity implies the correctness of the program.Discharg-ing the verification conditions can be done using existing theorem provers,either automatic or interactive.The formal specification of structured programs is naturally done using pre-and postcon-ditions for functions and loop invariants.Assembly programs,on the contrary,do not favor any particular program point for logical assertions.Recent work has identified the entry points of natural loops as obvious candidates for such assertions[1],but ourfirst experiments show that it can be a constraint.This is why we choose an approach where assertions can be freely inserted at any program point.We only impose that any cycle in the controlflow graph contains at least one assertion.Then it is possible to turn a MIX program into a set of purely sequential programs without jumps(either conditional or unconditional).In a second step,these programs are interpreted in a model where it is possible to apply the usual techniques of Hoare logic.Section2introduces our methodology.Section3describes a prototype and ourfirst experi-ments.We conclude with possible future work.X EQU1000ORIG3000MAXIMUM STJ EXIT←−PreINIT ENT30,1JMP CHANGEMLOOP CMPA X,3JGE*+3CHANGEM ENT20,3LDA X,3DEC31←−InvJ3P LOOP←−PostEXIT JUMP*Figure1:Program M(TAOCP,vol.1,page145).2MethodologyWefirst show how to annotate a MIX program using logical assertions(section2.1).Then we give an algorithm to turn this program into a set of purely sequential programs(section2.2).Finally we explain how to get verification conditions from these sequential programs(section2.3)and we prove the soundness of our method(section2.4).2.1SpecificationLet us consider thefirst program illustrating MIX,namely program Mfinding the maximum of the elements of an array[5,page145].This program is given Figure1.It assumes that the size of the array is in register I1,that the array contains at least one element,and that the elements are stored in memory at addresses X+1,...,X+I1.When the program return,accumulator A contains the maximum element and register I2an index where it appears.Thefirst step consists in specifying this behavior by inserting logical annotations in program M.There are three such annotations:•a precondition indicating the assumption at the program entry point,namelyPre≡I1≥1inserted at program point MAXIMUM;•a postcondition indicating the expected property at the end of execution,namely the annotationPost≡1≤I2≤I1∧A=X[I2]∧∀i,1≤i≤I1⇒A≥X[i] inserted a program point EXIT;•and an invariant indicating the property maintained by the program,namely the anno-tationInv≡0≤I3≤I1∧1≤I2≤I1∧A=X[I2]∧∀i,I3<i≤I1⇒A≥X[i] inserted right before instruction J3P.These three annotations are indicated on Figure1.The meaning of an annotation is clear:each time execution reaches an annotation,it must be verified.Figure2:Controlflow graph for program M.traverse(n)=if n is currently visited then fail(we found a cycle with no invariant)if n has not yet been visited thenfor each transition n s→mcall traverse(m)if m is an invariant I thenassociate to n the code s;assert Ielseassociate to n the code s;s for each code s associated to mif n is an invariant J the prefix each code of m by assume JFigure3:Sequentialization algorithm.2.2SequentializationThe next step is to turn the MIX program into a set of purely sequential programs which do not contain jumps anymore,and whose correctness imply the correctness of the initial program. To do so,wefirst build the controlflow graph,where nodes correspond to program points and transitions to sequences of instructions and test results.Such a controlflow graph for program M is given Figure2.The key idea is to impose the presence of(at least)one annotation on each cycle in the controlflow graph.Annotations are considered as invariants here:they must be verified when reached initially and maintained by any path used to come back.(In the remainder of this section we will refer to annotations as invariants instead of assertions to make it clearer.) Our sequentialization algorithm simply performs a depth-first traversal of the graph from the entry point,associating to each node a set of purely sequential programs.Pseudo-code for this algorithm is given Figure3.The result of sequentialization is the set of programs associated to the entry point and to each invariant encountered during the traversal.The result for program M is the set of four codes,given Figure4.Keyword assume introduces an assumption and keyword assert a property to be verified.These programs are naturally interpreted as follows:seq1is the initial validity of the invariant Inv;seq2and seq3express the preservation of Inv on the two possible paths;finally seq4expresses the validity of the postcondition.It is important to notice that this algorithm is not related to MIX but could be used with any assembly-like language.seq1≡assume Pre ENT30,1 ENT20,3 LDA X,3 DEC31 assert Inv seq2≡assume Invassume I3>0CMPA X,3assume CMP≥0DEC31assert Invseq3≡assume Invassume I3>0CMPA X,3assume CMP<0ENT20,3LDA X,3DEC31assert Invseq4≡assume Invassume I3≤0assert Post Figure4:Sequentializing program M.2.3Generating the Verification ConditionsThe last step consists in generating verification conditions from the sequential programs i.e.log-ical formulae whose validity implies the correctness of the initial program.For this purpose,we can use traditional Hoare logic[4],or more conveniently a calculus of weakest preconditions[2], provided some logical model of MIX programs:•registers A,X,I1,...I6are modeled as global integer variables;•the memory is modeled as a global array of integers;•flags E,G and L are interpreted as the sign of a unique global variable CMP. Furthermore,we make the following assumptions:•direct use of register J is not supported(only the co-routine pattern is recognized and handled separately);•input-output instructions are not modeled:they can be used in programs but the user has to state assumptions about data which is read.2.4SoundnessIn this section we prove the soundness of our method.Let us write S={seq1,...,seq k}the set of purely sequential programs resulting from the sequentialization.Each seq i has the following shapeassume P is iassert Q iwhere P i and Q i are user invariants and s i is a purely sequential program which does not contain any invariant(but with possible assume declarations corresponding to test results).Let us assume an operational semantics for purely sequential MIX programs,as a set of states and a transition relation between states written S1s−→S2which means“execution of program s in state S1leads to state S2”.We note S|=I if invariant I holds in state S.The correctness of each program seq i means that in any state S1such that S1|=P i and for any state S2such that S1s i−→S2we have S2|=Q i.Note that we are only considering partial correctness.Soundness can be stated as follows:Theorem1(soundness)Let S be a state satisfying the invariant I at entry point,i.e.S|=I, and let us consider an execution reaching a program point with an invariant J in state S .Then S |=J.Proof.Let us consider all the intermediate states where the execution reaches an invariant. By definition of the sequentialization algorithm,there is afinite number of steps between two such states(otherwise we would have a cycle in the controlflow graph without any invariant). Therefore the execution looks like−→S n=S−→S2...s nS=S0s1−→S1s2where each state S i is associated to an invariant I i,with I0=I and I n=J.Each triple (I i−1,s i,I i)exactly corresponds to one sequential program in S,since invariant I i−1can be reached in the controlflow graph from the entry point,and since there is path from I i−1to I i in this graph which does not cross any other invariant.Then proving S i|=I i is a straightforward induction,since S0|=I0by assumption and since the correctness of the sequential programs implies that if S i−1|=I i−1and S i−1s i−→S i then S i|=I i.3Implementation3.1PrototypeWe implemented our method as a prototype tool,called demixify,taking annotated MIX programs as input and generating verification conditions in the native syntax of several theorem provers. Our tool uses the back-end of the Why platform[3],which provides an intermediate language dedicated to program verification.Thus our prototype is simply a front-end which parses annotated MIX programs,performs the sequentialization and then prints the resulting programs in the syntax of the Why tool.Then we rely on the Why tool to compute the verification conditions and to dispatch them to interactive provers(such as Coq,PVS,Isabelle/HOL,etc.) or automatic provers(Simplify,Ergo,Yices,etc.).In practice,demixify is run on afile file.mix to produce a Whyfile file.why.Then it is possible to use tools from the Why platform on thisfile(to compute the verification conditions,display them,launch provers,display the results,etc.).Inside file.mix annotations are inserted between brackets.One pair of brackets{P}stands for an assertion to be verified at the corresponding program point and double brackets{{P}}stands for an invariant.A quotation mechanism allows to insert pure Why code inside the inputfile,using the syntax{{{ why code}}}.This is typically used to insert a prelude containing parameters for the program or logical declarations for its specification.Within annotations,the current values of registers is referred to using the names A,I1,I2, etc.The current value at address p in memory is denoted by mem[p].3.2Case StudiesUp to now,we only verified very simple MIX programs,such as program M above(which is verified fully automatically).We briefly describe some of these case studies in this section.3.2.1Sequential SearchingWe consider here three implementations of sequential searching from Section6.1of The Art of Computer Programming[7,page397].The goal is to check whether a given value stored at address K appears in an array of N values stored at addresses KEY+1,...,KEY+N.First,we introduce KEY,K and N as parameters,using the quotation for Why code: {{{logic KEY,K,N:int}}}Thefirst implementation(Program S page397)simply scans the array from index1to index N.It can be annotated as follows:start:{{N≥1}}lda Kent11-N2H:{{1≤N+I1≤N∧A=mem[K]∧∀i,1≤i<N+I1⇒mem[K]=mem[KEY+i]}}cmpa KEY+N,1je successinc11j1np2Bfailure:{∀i,1≤i≤N⇒mem[K]=mem[KEY+i]}hltsuccess:{mem[K]=mem[KEY+N+I1]}The postcondition is split into two assertions at labels failure and success,respectively.The loop invariant is here located at the loop entry point(label2H).It may seem unnecessary to add A=mem[K]in the loop invariant,since A and K are not modified in the loop body,but there is currently no mechanism to get such invariant for free.When demixify is run on this program,it generates10verification conditions(when splitting conjunctions),all discharged automatically using an automatic theorem prover such as Simplify or Ergo.The next implementation(Program Q page397)improves on the previous one by setting a sentinel at address KEY+N+1,namely the value to be searched for.The annotated code is as follows:start:{{N≥1}}lda Ksta KEY+N+1ent1-Ninc11{{1≤N+I1≤N+1∧A=mem[K]∧mem[KEY+N+1]=A∧∀i,1≤i<N+I1⇒mem[K]=mem[KEY+i]}}cmpa KEY+N,1jne*-2j1np successfailure:{∀i,1≤i≤N⇒mem[K]=mem[KEY+i]}hltsuccess:{mem[K]=mem[KEY+N+I1]}The specification is exactly the same,apart from the addition of a specification for the sentinel in the loop invariant,namely mem[KEY+N+1]=A.Note that the loop invariant is placed one instruction after the loop entry point(which is located here right before instruction inc11). As we already did with program M,we notice that it is convenient to have freedom in invariant locations.For this second implementation,12verification conditions are generated and all are automatically discharged.The last improvement consists in unrolling the loop once,in order to save one increment (Program Q’page398).The specification is exactly the same as for program Q:start:{{N≥1}}lda Ksta KEY+N+1ent1-1-N3H:inc12{{1≤N+I1≤N+1∧A=mem[K]∧mem[KEY+N+1]=A∧∀i,1≤i<N+I1⇒mem[K]=mem[KEY+i]}}cmpa KEY+N,1je4Fcmpa KEY+N+1,1jne3Binc114H:j1np successfailure:{∀i,1≤i≤N⇒mem[K]=mem[KEY+i]}hltsuccess:{mem[K]=mem[KEY+N+I1]}Again the loop invariant is not placed at the loop entry point but immediately after the in-crement instruction(inc12here).Running demixify on program Q’results in14verification conditions.All are automatically discharged,but one.Not surprisingly,this is the preservation of the property∀i,1≤i<N+I1⇒mem[K]=mem[KEY+i]when I1is incremented by2,i.e.after two successive negative tests.Thus the proof requires two case analyzes to distinguish between1≤i<N+I1,i=N+I1and i=N+I1+1.It seems to be out of reach of the heuristics involved in the automatic theorem provers we are using. 3.2.2Selection SortOur last case study is a proof of straight selection sort[7,Program S page140].The purpose of this program is to sort in place the values stored at locations INPUT+1,...,INPUT+N,in increasing order.We start a Why prelude with the declaration of parameters N and INPUT:{{{logic N,INPUT:intNext we introduce predicate definitions to simplify annotations.Thefirst such predicate is the main invariant of selection sort,which states that the upper part of the array INPUT+ i,...,INPUT+N is already sorted and that all values in the lower part are smaller than values in the upper part:predicate Inv(a:int array,i:int)=sorted_array(a,INPUT+i,INPUT+N)andforall k,l:int.1<=k<=i-1->i<=l<=N->a[INPUT+k]<=a[INPUT+l]Here we use a predefined predicate sorted array from Why’s standard library.The second predicate is the permutation property.Indeed,we not only need to prove that thefinal array is sorted but also that it is a permutation of the initial.For this purpose we introduce an auxiliary variable mem0representing the initial contents of the memory and we use a predefined predicate sub permut from Why’s standard library:logic mem0:int farraypredicate Perm(m:int array)=sub_permut(INPUT+1,INPUT+N,m,mem0)}}}We are now in position to annotate the MIX code for selection sort:init:{{N≥2∧Perm(mem)}}ent1N-12H:{{1≤I1≤N−1∧Inv(mem,I1+2)∧Perm(mem)}}ent20,1ent31,1lda INPUT,38H:{{1≤I1≤N−1∧Inv(mem,I1+2)∧Perm(mem)∧1≤I2<I3≤I1+1∧A=mem[INPUT+I3]∧∀k,I2+1≤k≤I1+1⇒mem[INPUT+k]≤mem[INPUT+I3]}} cmpa INPUT,2jge*+3ent30,2lda INPUT,3dec21j2p8Bldx INPUT+1,1stx INPUT,3sta INPUT+1,1dec11j1p2B{sorted array(mem,INPUT+1,INPUT+N)∧Perm(mem)}This annotated code generates42verification conditions,all discharged automatically.3.2.3Other Case StudiesA proof of algorithm I(inversion of a permutation in place)is already engaged.We could also consider the formal proof of Knuth’s algorithm for thefirst N prime numbers performed by L.Th´e ry a few years ago[9]:the proof was done using Why and Coq directly and we could turn it into a proof of the original MIX code.4Conclusion and Future WorkWe have presented a methodology for the formal verification of MIX programs.A prototype has been implemented and thefirst experiments are encouraging.There are many possible extensions for this work.One improvement would be the ability to prove the termination of MIX programs,by addition of variants on each cycle of the controlflow graph,as we did for invariants. Another interesting extension would be formal reasonings regarding the complexity of MIX programs,since one of MIX’s main interests is precisely to allow a detailed complexity analysis. For this purpose,we could automatically associate counters to program lines in our model of MIX programs,and make it possible for the user to refer to these counters in annotations. Acknowledgements.I am sincerely grateful to L.Th´e ry for his suggestion to consider the formal proof of MIX programs.References[1]Mike Barnett and K.Rustan M.Leino.Weakest-Precondition of Unstructured Programs.In6th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering(PASTE),Lisbon Portugal,September2005.[2]Edsger W.Dijkstra.A discipline of programming.Series in Automatic Computation.Pren-tice Hall Int.,1976.[3]Jean-Christophe Filliˆa tre and Claude March´e.The Why/Krakatoa/Caduceus Platform forDeductive Program Verification.In19th International Conference on Computer Aided Ver-ification,2007.[4]C.A.R.Hoare.An axiomatic basis for computer munications of theACM,12(10):576–580,583,1969.[5]D.E.Knuth.The Art of Computer Programming.Volume1:Fundamental Algorithms.Addison-Wesley,1968.[6]D.E.Knuth.The Art of Computer Programming.Volume2:Seminumerical Algorithms.Addison-Wesley,1969.[7]D.E.Knuth.The Art of Computer Programming.Volume3:Sorting and Searching.Addison-Wesley,1973.[8]George C.Necula.Proof-carrying code.In Conference Record of POPL’97:The24th ACMSIGPLAN-SIGACT Symposium on Principles of Programming Languages,pages106–119, Paris,France,jan1997.[9]Laurent Th´e ry.Proving Pearl:Knuth’s algorithm for prime numbers.In Proceedings ofthe16th International Conference on Theorem Proving in Higher Order Logics(TPHOLs 2003),2003.。

Synopsys Formality EC Solution说明书

Synopsys Formality EC Solution说明书

DATASHEETOverview Formality ® is an equivalence-checking (EC) solution that uses formal, static techniques to determine if two versions of a design are functionally equivalent.Formality delivers capabilities for ECO assistance and advanced debugging to help guide the user in implementing and verifying ECOs. These capabilities significantly shorten the ECO implementation cycle.The size and complexity of today’s designs, coupled with the challenges of meeting timing, area, power and schedule, requires that the newest, most advanced synthesis optimizations be fully verifiable.Formality supports all of the out-of- the-box Design Compiler ® and Fusion Compiler™ optimizations and so provides the highest quality of results that are fully verifiable.Formality supports verification of power-up and power-down states, multi-voltage, multi- supply and clock gated designs.Formality’s easy-to-use, flow-based graphical user interface and auto-setup mode helps even new users successfully complete verification in the shortest possible time.Figure 1: Formality equivalence checking solutionIndependent formalverification of DesignCompiler and FusionCompiler synthesisresults, with built-in intelligencedelivering the highestverifiable QoRFormality Equivalence Checking and Interactive ECOKey Benefits• Perfect companion to Design Compiler and Fusion Compiler—supports all default optimizations• Intuitive flow-based graphical user interface• Verifies low-power designs including power-up and power-down states• ECO implementation assistance, fast verification of the ECO, and advanced debugging• Auto setup mode reduces “false failures” caused by incorrect or missing setup information• Multicore verification boosts performance• Automated guidance boosts completion with Design Compiler and Fusion Compiler• Verifies full-custom and memory designs when including ESP technologyFormalityThe Most Comprehensive Equivalence Checking SolutionFormality delivers superior completion on designs compiled with Design Compiler or Fusion Compiler. Design Compiler is the industry leading family of RTL Synthesis solutions. Fusion Compiler is the next generation RTL-to-GDSII implementation system architected to address the complexities of advanced process node design. Designers no longer need to disable the powerful optimizations available with Design Compiler or Fusion Compiler to get equivalence checking to pass. Design Compiler/Fusion Compiler combined with Formality delivers maximum quality of results (QoR) that are fully verifiable.Easy to Use with Auto-setup modeFormality’s auto-setup mode simplifies verification by reducing false failures caused by incorrect or missing setup information. Auto-setup applies setup information in Formality to match the assumptions made by Design Compiler or Fusion Compiler, including naming styles, unused pins, test inputs and clock gating.Critical files such as RTL, netlists and libraries are automatically located. All auto-setup information is listed in a summary report.Guided SetupFormality can account for synthesis optimizations using a guided setup file automatically generated by Design Compiler or Fusion Compiler. Guided setup includes information about name changes, register optimizations, multiplier architectures and many other transformations that may occur during synthesis. This correct-by-construction information improves performance and first-pass completion by utilizing the most efficient algorithms during matching and verification.Formality-guided setup is a standard, documented format that removes unpredictability found in tools relying on log file parsing.Independent VerificationEvery aspect of a guided setup flow is either implicitly or explicitly verified, and all content is available for inspection in an ASCII file.Figure 2: Automatic cone pruning improves schematic readability when debuggingHier-IQ TechnologyPatented Hier-IQ technology provides the performance benefits of hierarchical verification with flat verification’s out-of- the-box usability.Error-ID TechnologyError-ID identifies the exact logic causing real functional differences between two design representations. Error-ID can isolate and report several logic differences when multiple discrepancies exist. Error-ID will also present alternative logic that can be changed to correct a given functional difference; this flexibility allows the designer to select the change that is easiest to implement.Failing Pattern Display WindowAll failing input patterns can be viewed in a familiar spreadsheet-like format. The failing pattern window is an ideal way to quickly identify trends indicating the cause of a failing verification or improper setup.Figure 3: Problem areas can be easy identified by visual inspection of the Failing Pattern WindowPower-aware VerificationFormality is fully compatible with Power Compiler™ and verifies power-up and power-down states, multi-voltage, multi-supply and clock gated designs.When a reference design block is powered up, Formality verifies functionality. If the implementation design powers up differently, failing points will occur.Formality functionally verifies that the implementation powers down when the reference powers down and will detectfunctional states where the implementation does not power down as expected. The valid power states are defined in the power state table (PST).Power intent is supplied to Formality through IEEE 1801 Unified Power Format (UPF).Figure 4: Power connectivity is easy to see and debug from the schematic viewAccelerated Time to ResultsFormality’s performance is enhanced with multicore verification. This Formality capability allows verification of the design using up to four cores simultaneously to reduce verification time.Other Time-Saving FeaturesFormality’s Hierarchical Scripting provides a method to investigate sub-blocks without additional setup and is ideal for isolating problems and verifying fixes.The Source Browser opens RTL and netlist source files to highlight occurrences of a selected instance. This can help users correlate between the RTL and gate-level design versions.Error Region Correlation provides a quick, visual identification of the logic from one design that correspond to the errors isolated by Error-ID within the other.Command Line Editing allows you to take advantage of history and common text editor commands when working from Formality’s command line.Interactive ECOKey BenefitsProvides GUI-driven ECO implementation assistance, fast ECO verification, and advanced debugging. Formality guides the user through the implementation of ECOs, and then quickly verifies only the changed logic.Formality Interactive ECO FlowFormality uses the ECO RTL and an unmodified netlist. Guided GUI driven changes are made to the netlist. Once the ECO has been implemented, a quick verification is run on only the affected logic cones, eliminating the need for a full verification run on the design to verify that the ECO was implemented correctly.Once all ECO’s are implemented and fully verified, a list of IC Compiler™ commands is generated to assist in implementing the physical changes to the design.ECO GuidanceFormality highlights equivalent nets between the reference and implementation designs, and nets that have lost their equivalence due to the ECO changes in the reference. This helps the designer quickly identify where the change should be made in the implementation.Implementing the ECOEditing commands in Formality are used to modify the netlist in-place using the GUI.Rapid ECO VerificationFormality can identify and verify just the portion of the design affected by the ECO. This ensures that the ECO was implemented correctly. If the ECO verification fails, the ECO can be interactively “undone” and new edits can be made again. Once the partial verification passes, the changes are committed. This partial verification eliminates having to verify the entire design to assure that the ECO was implemented correctly, dramatically reducing the total time required to implement and verify the ECO.Figure 5: Equivalent net is highlighted between Reference design (left) and Implementation design (right)Figure 6: On a completed ECO, the schematic shows the nets affected by ECO in yellow, and the new component and net in orangeFigure 7: Formality transcript shows a successful partial verification of the portion of the design that was affected by the ECOInterface with IC Compiler IIOnce the ECO’s are implemented and verified, a final complete verification run is performed to assure that the ECO RTL and the ECO netlist are functionally equivalent.Formality produces IC Compiler II compatible ECO command file, easing the implementation in the physical design.Advanced DebuggingFormality incorporates advanced debugging capabilities that help the designer identify and debug verifications that do not pass. The designer can find compare points, equivalences (and inverted-equivalences) between reference and implementation designs, perform “what if” analysis by interactively modifying the designs, and verify equivalence between two (or multiple) points.Transistor VerificationESP combines with Formality to offer fast verification of custom circuits, embedded memories and complex I/Os. ESP technology directly reads existing SPICE and behavioral RTL models and does not require restrictive mapping or translation.Input Formats• Synopsys DC, DDC, Milkyway™• IEEE 1800 SystemVerilog• Verilog-95, Verilog-2001• VHDL-87, VHDL-93• IEEE 1801 Unified Power Format (UPF)Guided Setup Formats• Synopsys V-SDC• Formality Guide Files (SVF)Platform Support• Linux Suse, Red Hat and Enterprise• SPARC SolarisFor more information about Synopsys products, support services or training, visit us on the web at: , contact your local sales representative or call 650.584.5000.©2019 Synopsys, Inc. All rights reserved. Synopsys is a trademark of Synopsys, Inc. in the United States and other countries. A list of Synopsys trademarks isavailable at /copyright.html . All other names mentioned herein are trademarks or registered trademarks of their respective owners.。

Formal verification of a public-domain DDR2 controller design

Formal verification of a public-domain DDR2 controller design

Formal verification of a public-domain DDR2 controller designAbhishek DattaOski TechnologyNew Delhi, India abhishek@Vigyan Singhal Oski Technology Fremont, CA, USA vigyan@AbstractThis paper demonstrates a formal verification-planning process and presents associated verification strategy that we believe is an essential (yet often neglected) step in an ASIC or SoC functional formal verification flow. Our contribution is to present a way to apply the verification planning process and a set of abstraction techniques on a non-trivial open-source example (the Sun OpenSPARC™ DDR2 controller). The process and verification strategy can be applied to DDR2 controllers in particular and generalized for other designs.1. IntroductionModel checking (referred to as Formal verification elsewhere in this paper) usage has been increasing in recent times. This is partly due to the increase in performance and capacity of formal engines and partly due to the standardization of property specification languages. However, formal verification can still not lay claim to mainstream acceptance as a necessary part of verification sign-off. This can be attributed to a dearth of published material on three key aspects of effective formal verification - structured verification planning, re-usable verification IP and good verification strategy.Recently, there have been several attempts made to address the verification-planning aspects (Foster et al [1]). Formal verification IP re-use has also been reasonably well-documented [6]. However, there remains a need to disseminate effective verification strategies and methods to simplify complexity without necessarily compromising the completeness of the desired proof. Without good strategy most formal verification projects will be overwhelmed by complexity issues [7]. This paper is intended to address this perceived need.We use the open-source OpenSPARC T1 DDR2 controller design [2] as a context to demonstrate formal verification planning and implementation. The design is of comparable complexity to many modern memory controllers which, it is hoped, renders the presented ideas immediately applicable to the verification of similar designs.We discuss the re-use of formal verification IP to shorten schedules, use of interesting design abstractions and explain how cut-points can be a powerful compositional reasoning technique. The verification strategy employed to handle the design complexity is described in detail. Most memory controllers have common design strategies, even though they have been designed independently. This is partly because common design techniques permeate the industry over time and partly because of the requirements imposed by the standard specifications [4]. Therefore, we believe that the complexity issues described in this paper are pertinent to most DDR controller implementations. By extension, the techniques used to tackle the complexity are applicable to the whole class of memory controller designs and can be leveraged for other design types.The design and verification material discussed in this paper has been made freely available and published on a public website. Readers can download the material for further experimentation and jump-starting their own verification efforts.2. Review of the OpenSPARC designThe OpenSPARC-T1 processor is a highly integrated processor that implements the 64-bit SPARC V9 architecture. The processor, codenamed “Niagara” has been made publicly available [2] by Sun to promote participation in SPARC processor architecture and application design. The design is representative of cutting edge processor architecture with multi-threading, multi-CPU and other advanced features.Our focus area comprises the four on-chip dynamic random access memory (DRAM) controllers directlyinterfacing to the double data rate-synchronous DRAM (DDR2 SDRAM) modules. The controllers implement 144-bit interface per channel with 25 GB/sec peak total bandwidth. The downloadable package for the chip contains the Verilog RTL source, documentation and a comprehensive simulation-based regression environment. 3. OpenSPARC DDR2 Controller The functional block diagram of the DDR2 controller is shown below.Figure 1. DDR2 Controller Functional DiagramThe shaded region in the figure (sourced from [3]) above shows the address and control logic block inside the controller. There exists high concurrency in the control path due to the multiple independent sources of command words to the DDR2 DIMMs. In order of arbitration priority, these sources are – o Periodic Refresh requests. o Pending CAS Requests.o Scrub Row-Address-Strobe (RAS) requests. o Incoming Read RAS requests. o Incoming Write RAS requests.The read-write priority can change depending upon per-bank write-starvation counters and handling of write-before-read hazards.This concurrency in the design makes the control logic in the shaded box a good candidate for formal verification. Also, the control logic is encapsulated as a separate verilog module which means that we need make no effort to isolate the target logic.The data-path contains elements like ECC-based error correction which due to the arithmetic operations involving large data-paths is not ideal for formalanalysis. Suitable abstractions, such as black-boxing the ECC module and applying data-tagging patterns would make the data-path more amenable to analysis. However, for the purposes of this paper, we shall restrict the discussion to the control logic in the shaded area in Fig. 1. 4. Formal Verification-planning Review The initial planning stages of a 7-step verification plan [1] are shown in Fig. 2.Figure 2. Initial stages of a structured planThe intuitive steps impose a structure upon the planning effort. We briefly outline the preliminary steps for the DDR2 controller verification.Identification involves determination of design components that are in the formal verification “sweet-spot”. Blocks that have concurrency with limited sequential depth are good candidates. We have already identified the DDR2 control path logic as our target for the reasons mentioned in Section 3.Description involves a high-level functional specification of the target block. This can be derived from internal implementation specifications as well as the standard protocols that the target implements. In our case, the JEDEC DDR2 protocol specification [4] serves as the interface description.Interface description refers to the documentation of the inputs and outputs of the target block. The DRAM section of the OpenSPARC micro-architecture document [3] describes the interface in detail. The point of the interface listing is to identify missing constraints (are all my inputs constrained appropriately?) and missing assertions (do I have assertions on all my outputs, wherever applicable?). Generating requirements refers to the creation of a set of English language properties derived from the high-level design description. Typically, these are classified as interface and end-to-end requirements. We shall restrict our verification scope to the DDR2 interface. A set of English requirements for the control logic might read as follows –1. Activate cannot be issued to a non-Idle bank.2. Read and write commands can only be issued toactive banks.3. Check that the minimum Write to Read turnaroundtime is (CL-1) + (BL/2) + T_WTR …The next step is to translate the requirements to a formal description i.e. a formal property specification language. We use a pre-verified set of DDR2 properties, packaged as verification IP, in this effort.5. Review of DDR2 Formal VIPThe DDR2 protocol is an industry standard specification for SDRAM memory modules [4]. Compliant interface implementations must obey the protocol rules in the specification. A set of DDR2 properties must therefore be re-usable in all DDR2 verification. The re-use of proven, canned sets of properties is an important element of formal verification planning and re-use. It can significantly shorten verification schedules with better ROI since less time is spent implementing properties and verifying correctness.The DDR2 Formal VIP is articulated into module-level and per-bank properties with minimum auxiliary code sharing between different properties. There are two approaches to implementing property sets for non-trivial protocols that require supporting RTL logic to track design states. One approach is to code one or more monolithic FSMs and then writing properties that are derived from the states (or state transitions) in the large FSMs. The other approach is to minimize the shared logic between the different properties. The former approach is considered better for implementing constraints and the latter for assertions.Since the DDR2 control path has only outputs, all our properties are assertions. The approach was to come up with a set of properties that each target distinct design attributes, but together cover all of the protocol. This minimizes code sharing and duplication. It keeps the logic cone of the assertions pared down to the minimum relevant state elements.6. Verification OverviewSome points need to be made about the verification effort.We had no access to the designers of the block and an element of guesswork was involved in constraining the internal interfaces. Further, we had to spend more time looking through the RTL than normally required. The functional specification of the block [4] and the simulation-based regression infrastructure were well-documented. We restricted our efforts to the control path in the controller block. Also, we focused solely on the DDR2 interface properties of the block.The total effort comprises about three weeks of single person activity. The shortened schedule owes a great deal to the availability of DDR2 verification IP and reasonably good documentation.7. Verification StrategyIn this section we present a step-by-step discussion of the verification strategy. Note that while some of the elements, like initialization and exploiting symmetry, were anticipated a priori, the other implementation-specific abstractions were refined as we gained familiarity with the target design. This is fairly typical of the verification process.7.1. CSR Value Selection and InitializationThe DDR2 protocol specifies a large set of timing parameters. These parameters are typically stored in Controller Core CSRs accessible through a register programming interface. These (and other) CSRs need to be initialized by software before normal operation can commence. The programming of the registers is well-defined and typically done during boot-up. This highly sequential operation of significant depth is best done in simulation. We use the OpenSPARC simulation environment to take the design through initialization to an initial “normal” operation state from which point the formal engines take over.Figure 3. Simulation-based Design InitializationOnce initialized, it is important to block off the register write interface so that the CSRs do not change during formal analysis. Suitable constraints are written on the design inputs to disable register writes.Further, the DDR2 protocol defines an enumeration sequence of command words to initialize the DDR2 SDRAM module. A DDR2 controller cycles through this sequence after boot-up. Once again, this sequential“hump” needs to be crossed before we can begin formal analysis of the controller design. We again turn to simulation to take the design over the enumeration sequence. The initial state for our formal analysis is the state of the design after CSR initialization and DDR2 enumeration sequence is complete.7.2. Identifying Formal Sweet-spotsFig. 4 shows the DDR2 protocol state-diagram. The states and transitions outside the shaded area involve significant sequential depth that can compromise formal analysis. The design inputs were constrained such that these state transitions are avoided.Figure 4. DDR2 Formal Sweet-spotsSimulation-based techniques are very good at exercising well-defined state transitions with high sequential depth that are avoided in formal analysis. This demonstrates how the two verification techniques are complimentary to each other.7.3. Exploiting Design SymmetryDesign symmetry can be used to reduce analysis complexity. For instance, a 32-bit data-path can be reduced to a single bit if the data-path is manipulated atomically (no bit-slice manipulation). In this case, the symmetry of the data-path allows us to consider a single bit in lieu of the 32 bits.The DDR2 controller is capable of accessing four DDR2 modules concurrently with a 4-bit chip-select. The symmetry of the implementation means that if we verify the correctness for a single module (one bit of chip-select) while allowing the other modules to be accessed (but not monitored) then we have reasonable confidence in the completeness of the proof.Further, the DDR2 controller implements eight banks. Similar to the chip-selects, there is symmetry in the per-bank queue management logic. Verifying the operation for a single bank would be equivalent to verifying each bank separately. Note that to exploit this symmetry the formal VIP must have corresponding symmetry in its implementation of per-bank properties.7.4. Abstracting Large CountersCounters can add significant sequential depth to formal analysis. The DDR2 controller has a surfeit of counters. Most of these are small but the following are large enough to significantly impact performance – Refresh Interval – The DDR2 controller issues periodic Refresh commands to the DDR2 modules. The period is established by a 13-bit counter.Scrub Interval – The controller issues internal scrub commands at periodic intervals. The period is established by a 12-bit counter (see elaboration below).Write Starvation Counters – The controller gives higher priority to Read as opposed to Write. To prevent write starvation, a 6-bit counter begins counting after the Write Queue is full. A pending Write has priority over Read when the counter is full.CAS Latency Counters – Each bank has an 8-bit CAS latency counter that blocks further RAS picks if a CAS has been pending for more than 64 clock cycles.These counters can add substantial amount of sequential depth (diameter) to the analysis. As a result, the analysis might not converge. We show how cut-points can serve as equivalent abstractions.Consider the scrub-interval decision logic –The listing shows how the decision about the scrub timing interval is dependent on the value of the “que_scrb_time” net. This net is driven by an equation involving the comparison of the interval counter with a programmed interval in a CSR. If we place a cut-point on this net i.e. we direct the formal engines to treat this net as if it were a primary input, then we remove the interval counter from the logic cone of (relevant) assertions on the controller outputs. This increases the likelihood of analysis convergence.We have replaced the counter-driven logic by a simpler abstraction (an arbitrary un-driven net) that eliminates the sequential depth imposed by the counter. An analysis failure might arise due to the cut-point, which is easy to debug. On the other hand, a proof obtained with the cut-point is applicable to the original design as well. This is because we have replaced the specific counter logic that drives (constrains) the net, with an abstraction that under-constrains the analysis.For each of the counters listed earlier, a similar cut-pointing was done to eliminate them from the analysis.7.5. Handling Address ComparisonsThe controller assigns higher priority to Read over Write unless there is a Read after Write (RAW) hazard. It handles RAW hazards by comparing an incoming Read address with all the write addresses currently pending in the write queue. The corresponding decision logic is shown below –The net “que_b0_wr_index_pend” is asserted when a RAW hazard is detected. The 32-bit address comparison pulls in all the 32-bits of the address space, not to mention the recorded address bits in the Write queues. Consider the modified equation -We have removed the address comparison terms from the equation driving the net. Instead we introduce a free variable that can be arbitrarily asserted by the formal analysis to introduce a hazard condition. This simpler abstraction does not rule out any hazard condition that is admitted by the original equation. Therefore, a proof with the simpler equation is applicable to the original design. We have accomplished two things with this abstraction – First, we have eliminated the 32-bit address words stored in the write queue from the logic cone of relevant assertions. Second, we have reduced the need to monitor the 32-bit incoming read address. The free net removes the address logic from the simplified hazard equation.Figure 5. Eliminating Address-bits from COIAddress comparisons of this type are common. For instance, code that checks whether an address falls within an acceptable range. This technique can be judiciously used in these situations to eliminate complexity without compromising the quality of the proof.7.6. Applying Verification PatternsPatterns can be defined as generalized solutions in a given engineering domain that find recurring application to the problems of that domain. We illustrate the use of one such verification pattern, the Floating Pulse [5], which was used to implement a DDR2 SVA property that uncovered a potential bug in the control-path. The pattern expresses intent to – Specify that a single bit value can be asserted for only one cycle in any cycle of an infinite sequence.We use the pattern to implement the following DDR2 property –No more than 4 ACTIVATE commands may be issued to the DDR2 SDRAM within a window of T_FAW clock cycles.We can use the Floating Pulse pattern here to fix the lower bound of our sampling window of width T_FAW clock cycles. Then a counter that counts off the T_FAW cycles is used to define the sampling window within which we check if more than 4 ACTIVATE were issued.We first setup a pulse element through the following assumption. This is an SVA implementation of the Floating Pulse pattern.We bind the pulse to (any and all) occurrence of an ACTIVATE command. The pulse assertion marks the start of our sampling window. We then load a counter at the start of the window and begin counting down.The following assertion ties everything together.This property failed for the OpenSPARC DDR2 controller design. The controller issued five ACTIVATE commands within a T_FAW window violating the protocol. It is possible that some element outside the design controls the ACTIVATE commands but purely in the context of the controller design this can be construed as an error of omission. Fig. 6 shows the property violation on the last clock cycle.Figure 6. T_FAW Window Violation8. ConclusionIn this paper we presented elements of verification strategy for a DDR2 controller design. We showed how simulation-assisted initialization, exploiting design symmetry, using cut-points, design abstractions and verification patterns can be used to reduce complexity. The techniques and abstractions presented have been found to be equally effective in the verification of other classes of designs. The work presented is in the public domain. The design and verification material can be downloaded from the Formal Verification Patterns repository [5].9. References[1] Harry Foster, Lawrence Loh, Bahman Rabii, Vigyan Singhal, “Guidelines for creating a formal verification testplan”, DVCON , 2006.[2] OpenSparc Initiative - [3] Sun Microsystems - OpenSPARC T1 Micro-Architecture Specification Document.[4] JEDEC DDR2 SDRAM Specification – JESD79-2B, /download/search/JESD79-2B.pdf , Jan 2005.[5] The Formal Verification Pattern Repository (Wiki) - /wiki[6] Andrea Fedeli, Matteo Moriotti, Umberto Rossi, Franco Toto, “Addressing IP Reuse with Formal Verification and Assertion Based Verification”, D&R Article - /articles/article9511.html[7] Adnan Aziz, Vigyan Singhal, Robert K. Brayton, “Verifying Interacting Finite State Machines: Complexity Issues”, Technical Report UCB/ERL M93/52. Electronics Research Lab, Univ. California, Berkeley, CA 94720.。

principles of model checking

principles of model checking

principles of model checkingModel checking is a formal verification technique used to check whether a model of a system meets a desired property or specification. The principles of model checking include:1. Formal specification: The desired property or behavior of the system is formally specified using a temporal logic language, such as linear temporal logic (LTL) or computational tree logic (CTL). This specification serves as the basis for model checking.2. Finite-state model: The system is modeled as a finite-state model, which consists of a set of states and transitions between states. This model captures the behavior of the system's components and their interactions.3. State space exploration: The state space of the model is systematically explored to check whether the desired property holds for all possible system executions. This involves generating and evaluating the possible execution paths of the system.4. Verification algorithm: A verification algorithm is used to traverse the state space and check the specified property at each state. Model checking algorithms, such as depth-first search or breadth-first search, are typically used for this purpose.5. Counterexample generation: If the desired property does not hold, the model checking process can generate a counterexample, which is a specific sequence of system states and transitions that violates the property. This provides insights into the specific causes of the violation and helps in debugging and refinement.6. Scalability: Model checking can be applied to both small-scale and large-scale systems. To handle complex systems, various techniques such as abstraction, symmetry reduction, and partial order reduction are used to reduce the size of the state space and make the verification process more efficient.7. Automation: Model checking is largely an automated process, where computer tools are used to systematically explore the state space and check the specified property. This helps in reducing human error and makes the verification process more reproducible and reliable.8. Soundness and completeness: Model checking aims to provide sound and complete results. Soundness means that if the model checker reports that the property holds, then it indeed holds in all possible executions of the system. Completeness means that if the property does not hold, the model checker will eventually find a counterexample.By following these principles, model checking provides a systematic and rigorous approach to verify the correctness of system models, which has applications in various domains such as software engineering, hardware design, and protocol verification.。