Binary Judgment Figure Bdd And Its Java Implementation, Application And Research

Many problems.in these fields such as digital control system,computer assistant design(CAD),computer assistant test(CAT),artificial intelligent(AI)and programmable logic controller can be expressed as a series of Boolean operations.These operations rely on the sumbol of Boolean function and validity of algorithm.Generally,the expression of Boolean function or truthtable is usually used to describe digital logic function.Boolean function is a method that can describe digital logic function accurately.But along with rapid development of large-scale integrate circuit and super large-scale integrate circuit,the operation of digital logic function becomes more and more complex.Some disadvantages are exposed gradually from the following traditional methods.For example,if Boolean function is used to express digital logic function, there will be huge and complex expressions and long processing time.If truthtable is chosen, plenty of memory will be used,it only can be applied to some special fields.Whereas,the researchers try to find out more sententious and convenient expressions.BDD(Binary Decision Diagram) was proposed to express boolean function by E.R.Bryant in 1986.The memory used by BDD is less than other methods.Therefore,the researchers import BDD to former detection to obtain a larger system size.BDD attach increasingly importance to its inherent computing methods of large digital system.Synthetically,BDD has advantages as follows:(1) Intuitionistic.It is easy to logic circuit analyzing.(2) The details of digital circuit's logic describing is reflected,this is important for circuits analyzing and testing.(3) It is convenient for computer's storage because of its shorter programme than boolean algebra.(4) It is convenient for using artificial intelligence to search answer space heuristic.(5) The higher executing speed will be obtained whatever based on hardware or software.(6) Parallel graph theory algorithm is applied for improving executing speed.Former detection mainly validates finite state system create by a former whether satisfy the property that requested.Former detection technology can be described abstractively:former M and property P described logostic are presented,check that if P is true in M.The main problem in former detection is the blast in state space.This problem roots in the interaction among different parts in system,or complex data structure which has a large scale.The size of system state will be huge in this way.Tense logic plays an important role in former detection.Former detection is based on tense logic which may be made up of several states.Tense logic expression maybe true in some states and false in other states.Therefore,the value of the expression changes by states.Tense logic can be divide into two classes according to the discribtion of system state's time paths:computing tree tense logic(CTL) and linear tense logic(LTL).CTL is presented by Clarke and Emerson.It has easy operators and it can compute an expression whether finite state former is satisfied in some state.It is a time former which adopts tree and formed by uncertain state paths of several offsets. The reasons of using BDD in former detection are as follows:two BDD paradigms equal logically if and only if they are equal in suntax when these two predicate expressions are used by BDD.Namely,two BDDparadigms equal logically if and only if these two BDD paradigms are the same one BDD paradigm.At present,the basic idea of solving layout problem by BDD is as following:denote sataes and movements of layout problem to BDD paradigms first,input the BDD paradigms to BDD solver,then translate the result into generic layout problem.JavaBDD is a suit of Java software bag which applies for the creation of BDD,execution of logic operation,eXpression of diversion between state machine and state.It also can empolder various of expression of CTL by this software bag to implement simple functions of former detection.The article describes the concept,property,creation and algorithms of BDD theoretically, analyzes interrelated theories in JavaBDD.Some problems such as how to implement the creation, storage and reduction of BDD,how to implement logic and quantifier operation in BDD,how to constitute state concourse and transfer of states are analyzed.Representative example is chosen to explain the applications of BDD.The article also describes the primary theory of CTL and former detection.A improves project is proposed and validated according to implementing CTL's EX and AX algorithm in reference books.Different operation is added to JavaBDD.The article gives a simple circuit and former detection based on the implemention of CTL's basic expressions.