// ************************************************************************** // // // // eses eses // // eses eses // // eses eseses esesese eses Embedded Systems Group // // ese ese ese ese ese // // ese eseseses eseseses ese Department of Computer Science // // eses eses ese eses // // eses eseses eseseses eses University of Kaiserslautern // // eses eses // // // // ************************************************************************** // // The module below describes a RS-Flipflop constructed with NOR-gates // // that have the same delay. This delay is modeled as a macro step of // // Quartz. We then prove some facts about the stability of the circuits. // // ************************************************************************** // macro InputChange = ((s<->!X s) | (r<->!X r)); module RSFlipFlop(bool ?r,?s,p,q){ loop { next(p) = !(s | q); next(q) = !(r | p); pause; } } satisfies { // ------------------------------------------------------ // The following specs state that once a certain input // is given, then a stable output is obtained after some // delay time. To allow arbitrary delays, we have to fix // the input forever. // ------------------------------------------------------ Set : assert A G ( G( s & !r) -> F G (!p & q) ); Reset : assert A G ( G(!s & r) -> F G ( p & !q) ); Forbidden : assert A G ( G( s & r) -> F G (!p & !q) ); // ------------------------------------------------------ // The spec below states that the outputs oscillate when // the inputs s and r are both false at a point of time // where the outputs p and q are different. // ------------------------------------------------------ Oscillate : assert A G ( G (!s & !r & (p <-> q)) -> G ((X p <-> !p) & (X q <-> !q)) ); // ------------------------------------------------------ // The spec below states that the outputs oscillate when // the inputs s and r are both false at a point of time // where the outputs p and q are different. // ------------------------------------------------------ NoOscilla : assert A G ( G (!s & !r & (p <-> !q)) -> G ((X p <-> p) & (X q <-> q)) ); // ------------------------------------------------------ // We conclude that all inputs are stable when p is not // equal to q. This is proved below // ------------------------------------------------------ StableOutputs1: assert A ( G(p <-> !q) & G(s <-> X s) & G(r <-> X r) -> F G ( (p <-> X p) & (q <-> X q))); // ------------------------------------------------------ // This suggests the following operation mode: we assume // that at some point of time, we have (r <-> !s). This // either sets or resets the flipflop, and in particular, // we then have p!=q. If after that point of time, the // input s=r=1 never occurs, then we always have stable // outputs. However, the property StableOutputs2 below // is not true. // ------------------------------------------------------ // StableOutputs2: // assert A G ((s <-> !r) & // G!(s & r) & // F G ((s <-> X s) & (r <-> X r)) // -> // F G ((p <-> X p) & (q <-> X q))); // ------------------------------------------------------ // The problem that appears with the above specification // is that the inputs change too fast. An stable input // like s&!r can lead to transient transitions. For example, // !r&s&p&!q -> X(!p&!q), and when the same input would // still be available, we would reach output !p&q next. // ------------------------------------------------------ StableOutputsWithSlowInputs: assert A ( F(s <-> !r) & G (InputChange -> X !InputChange) & G !(s & r) & F G ((s <-> X s) & (r <-> X r)) -> F G ((p <-> X p) & (q <-> X q))); // ------------------------------------------------------ // Finally, we list all transitions, which explains the // delay time we used above: There are transitient moves // of length 2. // ------------------------------------------------------ AllTransitions: assert A G ((!r & !s & !p & !q -> X( p & q)) & (!r & !s & !p & q -> X(!p & q)) & (!r & !s & p & !q -> X( p & !q)) & (!r & !s & p & q -> X(!p & !q)) & (!r & s & !p & !q -> X(!p & q)) & (!r & s & !p & q -> X(!p & q)) & (!r & s & p & !q -> X(!p & !q)) & (!r & s & p & q -> X(!p & !q)) & ( r & !s & !p & !q -> X( p & !q)) & ( r & !s & !p & q -> X(!p & !q)) & ( r & !s & p & !q -> X( p & !q)) & ( r & !s & p & q -> X(!p & !q)) & ( r & s & !p & !q -> X(!p & !q)) & ( r & s & !p & q -> X(!p & !q)) & ( r & s & p & !q -> X(!p & !q)) & ( r & s & p & q -> X(!p & !q))); }