// ************************************************************************** //
//                                                                            //
//    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)));
}