Modeling and Verification of Circuit with Stable-Event

In recent years, the state based method has been common employed in formal verification. However, the event structures hardly adopted which is more direct and natural than finite state machines when describing the behavior of a circuit or system. In this paper, to describe the circuit accurately, stable event is proposed when the model extended bundle event structures, EBES in short, is equipped. From the signal transition waveform four actions can be obtained, two of them are used to express the stable signal, stable up and stable down. The stable event denotes the occured stable action. The EBES of primitive logic gates well be presented, and then the complex logic cell's EBES well be built in a compositional way.