Algebraic Systems And Formal And DS Theory Of Complex Encoder Verification Applications

With the rapid development of microelectronics technology, the complexity ofthe hardware and software system design is rapidly growing and the demand forreliability of system in harsh environment is increasing, all of those put forwardhigher requirement for the system on the correctness of design verification. Theformal verification overcomes the incompleteness of traditional verificationmethods, which is widely acknowledged as the major bottleneck in design methodology.It uses mathematical reasoning strictly and deductive method to prove whether thedesign specifications faithfully reflect the needs of users and whether the systemimplementations faithfully reflect system design standard. It is also used toverify whether the realization of product satisfies the critical performanceswhich the user needs.Theorem proving, one of the formal verification method, is extremely popularbecause it is free from the scale of the system, while high order logic theoremproving system is adopted widely because of its expressive flexibility. The morethe mathematic theorem libraries are, the wider the scope of application of thetheorem provers becomes.Based on higher order logical theorem prover, i.e. HOL4, this paper carriedout the research into the formalization of algebraic system and complex numbers,and then conducted the formal verification for SpaceWire, a highly reliablecommunication wire, on core encoder through theorem proving. The main innovationembodies in three following respects:(1)Formalizing the algebraic systemFirst, the properties of algebraic operations were formalized, and then thedefinitions and properties of common algebraic system including semigroup, monoid,group, ring and field were researched and analyzed. Started with the definitionof the operation, the logic descriptions of these structures were given, and theimportant properties were proved. At the same time the logic description of the homomorphism and isomorphism were given.(2) Formalizing the complex numbersThe data types of complex numbers were created firstly, and then the basicoperations were defined. After that, the basic theorems were proved. In addition,the modulus and argument were defined, and then the geometric meanings of complexnumbers in the form of polar coordinates were discussed. The exponential form ofcomplex number is commonly used in electronics; so many important properties ofthis form were researched and proved in detail. The achievement was collected byCambridge University in HOL4, which was listed as the highest achievement of HOL4in2011.(3)Formally verifying the DS encoding circuitTo verify whether the DS encoder circuit faithfully implemented thespecification in SpaceWire standard, the logic description of specification andimplementation about circuit were given first, and then equivalence checking wasapplied. With the aid of HOL tool, this equivalence checking was carried out ina formal verification method, i.e. theorem proving. This contribution wasdemonstrated in the3rdinternational SpaceWire conference.