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