// ************************************************************************** // // // // 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 // // // // ************************************************************************** // // filename: ./ComputerArchitecture/AsynchronousCircuits/Cogar.qrz // // author: Manuel Gesell // // // // description: // // The following describes an asynchronous queue cell patented by // // Cogar in 1965. The circuits is implemented by a dual rail encoding, // // i.e. the input and output data that is forwarded through the queue // // is encoded by two boolean wires (in1,in0) and (out1,out0), respectively. // // Moreover, there is a "transfer and hold" (TH) wire and a "transfer // // and clear" (TC) wire running in opposite direction to the data wires. // // A high value on TC signals that the cell is actually empty and may // // receive data from the cell on its left when TH goes low again. // // 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 InputStable1 = ((in0 <-> X in0) & (in1 <-> X in1)); macro InputStable2 = ((thr <-> X thr) & (tcr <-> X tcr)); macro InputStable = (InputStable1 & InputStable2); macro WiresStable1 = ((X a <-> a) & (X b <-> b) & (X c <-> c)); macro WiresStable2 = ((X d <-> d) & (X e <-> e) & (X f <-> f)); macro WiresStable = ((X g <-> g) & WiresStable1 & WiresStable2); macro DATA_ONE = ( a & !b & !c); macro DATA_ZERO = (!a & b & !c); macro DATA_NONE = (!a & !b & c); macro DATA_UNDEF = (!a & !b & !c); macro SIGNAL_ONE = ( out1 & !out0); macro SIGNAL_ZERO = (!out1 & out0); macro SIGNAL_NONE = (!out1 & !out0); macro DATA_OSCILLATE1 = (!a & !b & !c -> X( a & b & c)); macro DATA_OSCILLATE2 = ( a & b & c -> X(!a & !b & !c)); macro DATA_OSCILLATE = (DATA_OSCILLATE1 & DATA_OSCILLATE2); macro SIGNAL_OSCILLATE1 = (!d & !e -> X( d & e)); macro SIGNAL_OSCILLATE2 = ( d & e -> X(!d & !e)); macro SIGNAL_OSCILLATE = (SIGNAL_OSCILLATE1 & SIGNAL_OSCILLATE2); macro HOLD1(phi) = (phi); macro HOLD2(phi) = (phi & X HOLD1(phi)); macro HOLD3(phi) = (phi & X HOLD2(phi)); macro HOLD4(phi) = (phi & X HOLD3(phi)); macro HOLD5(phi) = (phi & X HOLD4(phi)); macro HOLD6(phi) = (phi & X HOLD5(phi)); module Cogar (bool ?in0,?in1,?thr,?tcr, !out0,!out1,!thl,!tcl, a,b,c,d,e,f,g) { // bool a,b,c,d,e,f,g; choose a=true; else a=false; choose b=true; else b=false; choose c=true; else c=false; choose d=true; else d=false; choose e=true; else e=false; choose f=true; else f=false; choose g=true; else g=false; loop { next(a) = !(in0 | b | c | g); next(b) = !(in1 | a | c | g); next(c) = !(in0 | in1 | a | b); next(d) = !(in0 | in1 | b | c | e | f | thr); next(e) = !(in0 | in1 | a | c | d | f | thr); next(f) = !(d | e | tcr); next(g) = !(f | tcr); out0 = e; out1 = d; thl = g; tcl = c; pause; } } satisfies { // ---------------------------------------------------- // determine all stable states // ---------------------------------------------------- StableStates : assert A (F G WiresStable -> F G (DATA_ONE & SIGNAL_ONE) | F G (DATA_ZERO & SIGNAL_ZERO) | F G (DATA_ONE & SIGNAL_NONE) | F G (DATA_ZERO & SIGNAL_NONE) | F G (DATA_NONE & SIGNAL_NONE) | F G (DATA_UNDEF & SIGNAL_NONE) ); // ---------------------------------------------------- // verify the length of the critical path // ---------------------------------------------------- critical_path : assert A G(G InputStable -> (F G WiresStable <-> X X X X X X G WiresStable)); // ---------------------------------------------------- // inhibit output data when new input arrives // ---------------------------------------------------- InhibitOutputWhenNewInput : assert A G (in0 | in1 -> X SIGNAL_NONE); // ---------------------------------------------------- // inhibit output when right neighbor sends clear command // ---------------------------------------------------- InhibitOutputWhenClearCommand : assert A G (thr -> X SIGNAL_NONE); // ---------------------------------------------------- // receive new data and inhibit output signals // ---------------------------------------------------- NewDataOneWhenNewInput : assert A (F G (!in0 & in1 & (X tcr <-> tcr)) -> F G (SIGNAL_NONE & DATA_ONE & !thl & !tcl)); NewDataZeroWhenNewInput : assert A (F G (in0 & !in1 & (X tcr <-> tcr)) -> F G (SIGNAL_NONE & DATA_ZERO & !thl & !tcl)); NewDataUndefWhenNewInput : assert A (F G (in0 & in1 & (X tcr <-> tcr)) -> F G (SIGNAL_NONE & DATA_UNDEF & !thl & !tcl)); NewDataNoneWhenNewInput : assert A (F G (!in0 & !in1 & (X tcr <-> tcr) & (X thr <-> thr)) -> F G (SIGNAL_OSCILLATE & DATA_OSCILLATE) | F G (SIGNAL_NONE & DATA_OSCILLATE) | F G (SIGNAL_NONE & DATA_NONE)); // ---------------------------------------------------- // we repeat the above specs with quantitative time // ---------------------------------------------------- NewDataOneWhenNewInput4Cycles : assert A G( G (!in0 & in1 & (X tcr <-> tcr)) -> X X X X G (SIGNAL_NONE & DATA_ONE & !thl & !tcl)); NewDataZeroWhenNewInput4Cycles : assert A G( G ( in0 & !in1 & (X tcr <-> tcr)) -> X X X X G (SIGNAL_NONE & DATA_ZERO & !thl & !tcl)); NewDataUndefWhenNewInput4Cycles : assert A G( G ( in0 & in1 & (X tcr <-> tcr)) -> X X X X G (SIGNAL_NONE & DATA_UNDEF & !thl & !tcl)); // ---------------------------------------------------- // store existing data // ---------------------------------------------------- StoreDataOne : assert A G (!in0 & !in1 & !thl & DATA_ONE -> X DATA_ONE); StoreDataZero : assert A G (!in0 & !in1 & !thl & DATA_ZERO -> X DATA_ZERO); StoreDataNone : assert A G (!in0 & !in1 & !thl & DATA_NONE -> X DATA_NONE); StoreWhenNoNewData : assert A (F G (!in0 & !in1) -> F G ((DATA_ONE -> X DATA_ONE) & (DATA_ZERO -> X DATA_ZERO) & (DATA_NONE -> X DATA_NONE))); // ---------------------------------------------------- // send local data to output signals // ---------------------------------------------------- // ExposeDataOne: // assert A ( SIGNAL_NONE & DATA_ONE & // F G(!in0 & !in1 & !thr & tcr) // -> [(SIGNAL_NONE & DATA_ONE) SU (SIGNAL_ONE & DATA_ONE)]); // ExposeDataZero: // assert A ( SIGNAL_NONE & DATA_ZERO & // F G(!in0 & !in1 & !thr & tcr) // -> [(SIGNAL_NONE & DATA_ZERO) SU (SIGNAL_ZERO & DATA_ZERO)]); }