and2series.cta

很好的一本书

// Series AND2series, AND4series, AND8series, AND16series
//   of equivalent models for measurement of "polynomial growth".
// Variables ordered manually.

/* 
 * project: implementation of an 8-bit AND-Gate in CTA
 * modules: pMOSTransistorHigh, pMOSTransistorLow, nMOSTransistorHigh,
 *          nMOSTransistorLow, NANDGateHigh, NORGateLow, System
 * version: 05.05.2000
 * author:  Michael Vogel - ([e-mail])
 *
 * Based on paper "Some Progress in the Symbolic Verification of Timed 
 *                 Automata" pages 8 - 9 (MOS Circuits).
 *
 * This module uses five instances of NAND-gates and two instances of
 * NOR-gates to build an AND-gate with eight inputs. (28 transistors)
 * Boolean equation:
 * !( !( !(A && B) || !(C && D) ) && !( !(E && F) || !(G && H) ) ) 
 * == !(A && B && C && D && E && F && G && H)
 *
 * !!! There is no negator with two transistors to invert the "wrong" output.
 */

// instance of pMOSTransistorHigh is initialized to high
MODULE pMOSTransistorHigh
{
  INPUT
    // gate is value at gate input of pMOS transistor.
    gate         : DISCRETE;
    l            : CONST;
    u            : CONST;

  OUTPUT
    // outerVal = 1 if transistor is... and 0 if transistor is... 
    outerVal     : DISCRETE;
  
  // Initial gate input of pMOS transistor is zero -> outerVal = 1. 
  INITIAL   STATE(pMOS) = stable1
                   AND c = u AND outerVal = 1;  
    
  AUTOMATON pMOS
  {
    STATE stable0   { INV   gate = 1;  
                        TRANS { GUARD   gate = 0;  
                                DO   c' = 0;  
                                GOTO unstable1;
                              }
                    }
    
    STATE unstable1 { INV   gate = 0 AND c+1 <= u;  
                        TRANS { GUARD   gate = 1;  
                                DO   c' = u;  
                                GOTO stable0;
                              }
                        TRANS { GUARD   gate = 0 AND l <= c;  
                                DO   outerVal' = 1 AND c' = u;  
                                GOTO stable1;
                              }
                    }

    STATE unstable0 { INV   gate = 1 AND c+1 <= u;  
                        TRANS { GUARD   gate = 1 AND l <= c;  
                                DO   outerVal' = 0 AND c' = u;  
                                GOTO stable0;
                              }
                        TRANS { GUARD   gate = 0;  
                                DO   c' = u;  
                                GOTO stable1; 
                              }
                    }

    STATE stable1   { INV   gate = 0;  
                        TRANS { GUARD   gate = 1;  
                                DO   c' = 0;  
                                GOTO unstable0; 
                              }
                    }
  }
 
  LOCAL
    c            : CLOCK(5); // up
}

// instance of nMOSTransistorLow is initialized to low
MODULE nMOSTransistorLow
{
  INPUT
    // gate is value at gate input of nMOS transistor.
    gate         : DISCRETE;
    l            : CONST;
    u            : CONST;
 
  OUTPUT
    // outerVal = 1 if transistor is... and 0 if transistor is...
    outerVal     : DISCRETE;
  
  // Initial gate input of nMOS transistor is 0 -> outerVal = 0.
  INITIAL   STATE(nMOS) = stable0
                   AND c = u AND outerVal = 0;  
    
  AUTOMATON nMOS
  {
    STATE stable0   { INV   gate = 0;  
                        TRANS { GUARD   gate = 1;  
                                DO   c' = 0;  
                                GOTO unstable1;
                              }
                    }
    
    STATE unstable1 { INV   gate = 1 AND c+1 <= u;  
                        TRANS { GUARD   gate = 0;  
                                DO   c' = u;  
                                GOTO stable0;
                              }
                        TRANS { GUARD   gate = 1 AND l <= c;  
                                DO   outerVal' = 1 AND c' = u;  
                                GOTO stable1;
                              }
                    }

    STATE unstable0 { INV   gate = 0 AND c+1 <= u;  
                        TRANS { GUARD   gate = 0 AND l <= c;  
                                DO   outerVal' = 0 AND c' = u;  
                                GOTO stable0;
                              }
                        TRANS { GUARD   gate = 1;  
                                DO   c' = u;  
                                GOTO stable1; 
                              }
                    }

    STATE stable1   { INV   gate = 1;  
                        TRANS { GUARD   gate = 0;  
                                DO   c' = 0;  
                                GOTO unstable0; 
                              }
                    }
  }
 
  LOCAL
    c            : CLOCK(4); // un
}

// This module uses two instances of pMOS transistors and two instances of
// nMOS transistors to build a NAND gate with two inputs.
MODULE NANDGateHigh
{
  INPUT
    lp           : CONST;
    ln           : CONST;
    up           : CONST;
    un           : CONST;

    input1       : DISCRETE;
    input2       : DISCRETE;
    
  OUTPUT
    output1      : DISCRETE;

  LOCAL
    outputPMOS1  : DISCRETE(1);
   
  INST pMOS1 FROM pMOSTransistorHigh WITH
  {
    l            AS lp;
    u            AS up;
    gate         AS input1;  
    outerVal     AS outputPMOS1;
  }

  LOCAL
    outputNMOS1  : DISCRETE(1);

  INST nMOS1 FROM nMOSTransistorLow WITH
  {
    l            AS ln;
    u            AS un;
    gate         AS input1;  
    outerVal     AS outputNMOS1;
  }

  LOCAL
    outputPMOS2  : DISCRETE(1);

  INST pMOS2 FROM pMOSTransistorHigh WITH
  {
    l            AS lp;
    u            AS up;
    gate         AS input2;  
    outerVal     AS outputPMOS2;
  }

  LOCAL
    outputNMOS2  : DISCRETE(1);

  INST nMOS2 FROM nMOSTransistorLow WITH
  {
    l            AS ln;
    u            AS un;
    gate         AS input2;  
    outerVal     AS outputNMOS2;
  }

  // Initial inputs are 0 so initial output of NAND-gate is 1.
  INITIAL   STATE(zNAND) = high
                   AND output1 = 1;  

  AUTOMATON zNAND
  {
    STATE high  { INV   NOT ((outputPMOS1 = 0 AND outputPMOS2 = 0)
                             AND (outputNMOS1 = 1 AND outputNMOS2 = 1));
                       
                    TRANS { GUARD   (outputPMOS1 = 0 AND outputPMOS2 = 0)
                                    AND (outputNMOS1 = 1 AND outputNMOS2 = 1); 
                            DO   output1' = 0; 
                            GOTO low;
                          }
                }
    STATE low   { INV   NOT ((outputPMOS1 = 1 OR outputPMOS2 = 1)
                         AND (outputNMOS1 = 0 OR outputNMOS2 = 0));
                       
                    TRANS { GUARD   (outputPMOS1 = 1 OR outputPMOS2 = 1)
                                    AND (outputNMOS1 = 0 OR outputNMOS2 = 0); 
                            DO   output1' = 1; 
                            GOTO high;
                          }
                }
  }
}


// This module switches inputs once to random values if 0 <= clock < lx and
// keeps value if lx <= clock < ux. Initial value is 0.
MODULE inputLow
{
  INPUT
    lx           : CONST;
    ux           : CONST;
    c            : CLOCK;    

  OUTPUT
    outerVal     : DISCRETE;

  INITIAL   STATE(inp) = unstable
                   AND outerVal = 0;   

  AUTOMATON inp
  {
    STATE unstable { TRANS { GUARD   c + 1 <= lx;  
                             DO   outerVal' = 0 OR outerVal' = 1;   
                             GOTO stable;
                           }
                   }

    STATE stable   { INV   c <= lx;  
                       TRANS { GUARD   c = lx;  
                               GOTO unstable;
                             }
                   }
  }
}


// This module uses five instances of NAND-gates and two instances of
// NOR-gates to build an AND-gate with eight inputs. (28 transistors)
// Boolean equation:
// !( !( !(A && B) || !(C && D) ) && !( !(E && F) || !(G && H) ) ) 
// == !(A && B && C && D && E && F && G && H)
//
// !!! There is no negator with two transistors to invert the "wrong" output.
MODULE System
{
  // All constants have been divided by greatest common 
  // divisor of them.
  // See paper: "Some Progress in the Symbolic Verification 
  // of Timed Automata"
  // pages 8 - 9 (MOS Circuits).
  
  // l? minimal needed time to change output after change of 
  // input.
  // u? maximal needed time... .
  // ?p is time for pMOS transistor,
  // ?n for nMOS transistor.
  
  // Inputs can change if 0 <= clock < lx 
  // and inputs are stable if lx <= clock < ux.  

  INITIAL   STATE(aresetClock) = reset
                   AND c = 0;  

  LOCAL
    lx = 6       : CONST; // 24 / 40 / 20 / 40
    ux = 15      : CONST; // 56 / 56 / 60 / 60
    
  LOCAL
    lp = 2       : CONST; //  8 / 10
    ln = 2       : CONST; //  8
    up = 5       : CONST; // 20 
    un = 4       : CONST; // 16

  LOCAL
    c            : CLOCK(16); // c = ux + 1

  AUTOMATON aresetClock
  {
    STATE reset { INV   c <= ux;  
                  TRANS { GUARD   c >= ux;  
                          DO   c' = 0;  
                          GOTO reset;
                        }
                } 
  }
  
  INST binp1 FROM inputLow WITH
  {
    lx           AS lx;
    ux           AS ux;
    outerVal     AS input1;
    c            AS c;
  } 

  LOCAL
    input1       : DISCRETE(1);
  
  INST binp2 FROM inputLow WITH
  {
    lx           AS lx;
    ux           AS ux;
    outerVal     AS input2;
    c            AS c;
  }  

  LOCAL
    input2       : DISCRETE(1);     

  LOCAL
    outputNAND1  : DISCRETE(1);
    
  INST cNAND1 FROM NANDGateHigh WITH
  {
    lp           AS lp;
    ln           AS ln;
    up           AS up;
    un           AS un;
    input1       AS input1;
    input2       AS input2;
    output1      AS outputNAND1;
  }
}

REACHABILITY CHECK System
USE BDD
{
  VAR 
    initial: REGION;

  COMMANDS

//    initial := REACH FROM INITIALREGION FORWARD;

    initial := INITIALREGION;
   
    IF( ISREACHABLE FROM initial TO FALSE FORWARD ) {
      PRINT "State high in NOR1 reached."; }
    ELSE {
      PRINT "State high in NOR1 not reached."; } 

}