// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //

// --------------------------------------------------------------------
// This file implements an Asynchronous Communications Interface
// Adapter (ACIA) similar to the 6850. An ACIA converts serial data to
// parallel data so that it can be used by a microprocessor. The serial
// data is a fixed number of bits that are transmitted at a known
// frequency, preceded by a start bit (0) and followed by one or two
// stop bits (1).
//
// The ACIA controller connects a peripherial with a microprocessor.
// ACIA has two boolean inputs on the peripherial side with the following
// meaning:
//  DATA : input stream of 5bit wide data packets
//  DCD  : data carrier detect signal (indicates that valid data
//         has been transmitted)
//
// On the microprocessor side there are three further boolean inputs
// with the following meaning:
//
//  COMMAND : tells ACIA that the microprocessor wants to perform
//                one of the possible commands
//  C1,C0   : these two bits encode one the four commands of the
//                microprocessor which are
//                RESET: enable/disable interrupt when byte
//                               has been received
//             READSTAT: read status register
//             READDATA: read data register
//          MASTERRESET: master reset of the controller
//
// The ACIA controller has four outputs:
//
//  SHIFT : if true, the incoming data is shifted into the data
//              register
//   RDRF : RDRF (read data register full) indicates whether a
//              complete data packet has been read into the data
//              register. RDRF should be cleared if the ACIA is reset,
//              the carrier is lost, or if the microprocessor reads
//              the data after reading the status and finding RDRF high.
//    IRQ : IRQ (interrupt request)is cancelled if the ACIA is reset,
//      or if the microprocessor reads the status and data
//              registers.
//   DCDO : DCDO(data carrier detect outstanding) is set high
//              whenever there has been a loss of carrier that hasn't
//              been handled by the microprocessor. It is set high as
//              soon as DCD input goes low. It remains high as long as
//              DCD remains low. If the microprocessor either reads the
//              status and data registers or resets the ACIA while DCD
//              is low. DCDO will go low as soon as the carrier is
//      restored. Otherwise, DCDO will remain high until the
//              status and data registers are read or the ACIA is reset.
//
// The example has been taken from the following reference:
// @inproceedings{BrCD86,
//   key         ={BrCD86},
//   author      ={M.C. Browne and E.M. Clarke and D.L. Dill},
//   title       ={Automatic Circuit Verification Using Temporal Logic:
//         Two New Examples},
//   booktitle   ={Formal Aspects of {VLSI} Design},
//   address     ={Amsterdam},
//   editor      ={G.J. Milne and P.A. Subrahmanyam},
//   publisher   ={North Holland},
//   pages       ={113-124},
//   year        ={1986}
// }
// ----------------------------------------------------------------------


macro MASTERRESET = (COMMAND &  C1 &  C0);
macro READSTAT = (COMMAND &  C1 & !C0);
macro READDATA = (COMMAND & !C1 &  C0);
macro RESET = (COMMAND & !C1 & !C0);

macro NORMAL = (DCD & DCDO & IRQ & !COMMAND);

module ACIA (bool ?C0,?C1,?COMMAND,?DCD,?DATA,!SHIFT,!RDRF,!IRQ,!DCDO,RIE) {
    bool NEWIRQ,        // is true when an interrupt has been generated, but the
                        // processor has not discovered why by reading the status
                        // register
        DCDST,          // is true when the carrier has been lost but the processor
                        // hasn't read the status register to discover the problem.
        DCDRD;          // is true when the carrier has been lost and the
                        // microprocessor has not handled this by reading the
                        // status register and then the data register
        //RIE;            // (receive interrupt table) is true if the microprocessor
                        // should be interrupted when a complete byte has been
                        // received


    // ----------------------------------------------------------------
    // the first thread handles the incoming data
    // ----------------------------------------------------------------
    loop {
        abort {
            immediate await (!DATA);    // wait for start bit
            next(SHIFT)=true;           // start shifting
            pause;
            pause; pause; pause; pause; // receive four further bits
            next(SHIFT)=false;          // stop shifting
            pause;
            if(RIE) {                   // generate interrupt for processor
                next(IRQ) = true;
                next(NEWIRQ) = true;
            }
            next(RDRF) = true;          // signal full data register
            pause;
        } when(!DCD or MASTERRESET);
        next(SHIFT) = false;            // clean up when carrier is lost
        next(RDRF) = false;             // or data register was full
        pause;
    }
    ||
    // ----------------------------------------------------------------
    // the second thread handles the loss of the carrier
    // ----------------------------------------------------------------
    loop {
        immediate await (!DCD);         // check is carrier is lost
        next(DCDO) = true;              // not yet handled by processor
        if(!MASTERRESET) {            // generate interrupt if not reset
            next(IRQ) = true;
            next(NEWIRQ) = true;
            next(DCDST) = true;
            next(DCDRD) = true;
        }
        pause;
        immediate await (DCD);          // wait until DCD holds again
        next(DCDO) = DCDRD;
        pause;
    }
    ||
    // ----------------------------------------------------------------
    // the third thread handles the commands of the processor
    // ----------------------------------------------------------------
    loop {
        immediate await (COMMAND);
        case
        (READSTAT) do {
            next(NEWIRQ) = false;
            next(DCDST) = false;
        }
        (READDATA) do {
            next(RDRF) = false;
            next(IRQ) = NEWIRQ;
            next(DCDRD) = DCDST;
            next(DCDO) = DCDST | !DCD;
        }
        (MASTERRESET) do {
            next(IRQ) = false;
            next(NEWIRQ) = false;
            next(DCDST) = false;
            next(DCDRD) = false;
        }
        default {
            next(RIE) = !RIE;
        }
        pause;
    }
}

satisfies {
    Set_DCDO : assert A G (!DCD -> X DCDO);
    ReSet_DCDO : assert A G (DCDO & DCD -> X !DCDO);
    s1: assert A G (!DCD & !COMMAND & !DCDO & !RIE
            -> X [(DCD & READSTAT -> DCDO & IRQ & X [(DCD & READDATA ->
                    DCDO & IRQ & X (!DCDO & !IRQ)) WW !NORMAL]) WW !NORMAL]
        );
}