Logic Conformance Verification Of Asynchronous Circuits With EBES

Because of the lim itation of synchronous circuit,such as clock skew,jitter,noise and energy consumption,the asynchronous one has attracted more and more attentions.Asynchronous circuits have been used in real electronic systems,widely and deeply,so their correctness must be carefully validat ed.The description and verificat ion of the behavior of asynchronous circuits is a key issue to guarantee their functions.In recent years,most formal modelling and verification are based on state technology.Though,the event structures are rarely used in validat ion since of the much higher complexity of modelling procedure,but event structures are more direct and natural than finite state machines in modelling the behavior of digital circuit systems,especially the asynchronous one.In this thesis,the extended binding event structures(EBES)is selected to model and validate asynchronous circuits,and the process algebra semantics of EBES are described in detail.Event is the basic unit of the event structures,the event represents the occurrence of an action,and then how to obtain the action in the asynchronous circuit is very critical.Then the method of obtaining the action from the signal transmission waveform is given.Through the signal transmission waveform,each signal is divided into 4 actions,which contains two stable actions to represent the effective transmission of the signal.According to the definit ion of EBES,the denotional semantics of simple logic gates are presented.Because complex logic can be composed of basic logical units,it can be constructed as a combination of its EBES.The verification of asynchronous circuit is mainly to judge whether its EBES implement ation and specification are consistent.When using the bisimulation,to achieve the des ired results,the implementat ion must be added too many restrictions,but such a circuit is difficult to design.Therefore,the logic conformance is selected,and in order to ensure the accuracy of the asynchronous circuit,the relative t im ing constraints is added on the basis of the EBES implementation.At last,by taking the widely applied and important component CElement of asynchronous control unit as an example,and the EBES modelling of it is presented and the relative t im ing logic conformance is verified.In addition,two different implementat ions of CElement based on EBES and state machine are compared,and the former is more direct and natural than the latter in describing behavior.