and8series.cta

很好的一本书

  LOCAL
    outputNMOS1  : DISCRETE(1);

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

  LOCAL
    outputPMOS2  : DISCRETE(1);

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

  LOCAL
    outputNMOS2  : DISCRETE(1);

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

  // The initial inputs are 1 so initial output of NOR gate is zero.
  INITIAL   STATE(zNOR) = low
                   AND output1 = 0;  

  AUTOMATON zNOR
  {
    STATE high  { INV   NOT ((outputPMOS1 = 0 OR outputPMOS2 = 0)
                             AND (outputNMOS1 = 1 OR outputNMOS2 = 1));
                       
                    TRANS { GUARD   (outputPMOS1 = 0 OR outputPMOS2 = 0)
                                    AND (outputNMOS1 = 1 OR outputNMOS2 = 1); 
                            DO   output1' = 0;  
                            GOTO low;
                           }
                }
    STATE low   { INV   NOT ((outputPMOS1 = 1 AND outputPMOS2 = 1) 
                             AND (outputNMOS1 = 0 AND outputNMOS2 = 0));
                       
                    TRANS { GUARD   (outputPMOS1 = 1 AND outputPMOS2 = 1)
                                    AND (outputNMOS1 = 0 AND 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 switches inputs once to random values if 0 <= clock < lx and
// keeps value if lx <= clock < ux. Initial value is 1.
MODULE inputHigh
{
  INPUT
    lx           : CONST;
    ux           : CONST;
    c            : CLOCK;    

  OUTPUT
    outerVal     : DISCRETE;

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

  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;
  }

  LOCAL
    outputNOR1   : DISCRETE(1);  

  LOCAL
    outputNAND2  : DISCRETE(1);

  INST dNOR1 FROM NORGateLow WITH
  {
    lp           AS lp;
    ln           AS ln;
    up           AS up;
    un           AS un;
    input1       AS outputNAND1;
    input2       AS outputNAND2;
    output1      AS outputNOR1;
  }

  INST binp3 FROM inputLow WITH
  {
    lx           AS lx;
    ux           AS ux;
    outerVal     AS input3;
    c            AS c;
  }

  LOCAL
    input3       : DISCRETE(1);
  
  INST binp4 FROM inputLow WITH
  {
    lx           AS lx;
    ux           AS ux;
    outerVal     AS input4;
    c            AS c;
  }

  LOCAL
    input4       : DISCRETE(1);
  
  INST cNAND2 FROM NANDGateHigh WITH
  {
    lp           AS lp;
    ln           AS ln;
    up           AS up;
    un           AS un;
    input1       AS input3;
    input2       AS input4;
    output1      AS outputNAND2;
  }

  LOCAL
    outputNOR2   : DISCRETE(1);

  LOCAL
    outerVal     : DISCRETE(1);

  INST eNAND5 FROM NANDGateHigh WITH
  {
    lp           AS lp;
    ln           AS ln;
    up           AS up;
    un           AS un;
    input1       AS outputNOR1;
    input2       AS outputNOR2;
    output1      AS outerVal;
  }

  INST binp5 FROM inputLow WITH
  {
    lx           AS lx;
    ux           AS ux;
    outerVal     AS input5;
    c            AS c;
  }

  LOCAL
    input5       : DISCRETE(1);
  
  INST binp6 FROM inputLow WITH
  {
    lx           AS lx;
    ux           AS ux;
    outerVal     AS input6;
    c            AS c;
  }

  LOCAL
    input6       : DISCRETE(1);
  
  LOCAL
    outputNAND3  : DISCRETE(1);

  INST cNAND3 FROM NANDGateHigh WITH
  {
    lp           AS lp;
    ln           AS ln;
    up           AS up;
    un           AS un;
    input1       AS input5;
    input2       AS input6;
    output1      AS outputNAND3;
  }

  LOCAL
    outputNAND4  : DISCRETE(1);

  INST dNOR2 FROM NORGateLow WITH
  {
    lp           AS lp;
    ln           AS ln;
    up           AS up;
    un           AS un;
    input1       AS outputNAND3;
    input2       AS outputNAND4;
    output1      AS outputNOR2;
  }

  INST binp7 FROM inputLow WITH
  {
    lx           AS lx;
    ux           AS ux;
    outerVal     AS input7;
    c            AS c;
  }

  LOCAL
    input7       : DISCRETE(1);

  INST binp8 FROM inputLow WITH
  {
    lx           AS lx;
    ux           AS ux;
    outerVal     AS input8;
    c            AS c;
  }

  LOCAL
    input8       : DISCRETE(1);

  INST cNAND4 FROM NANDGateHigh WITH
  {
    lp           AS lp;
    ln           AS ln;
    up           AS up;
    un           AS un;
    input1       AS input7;
    input2       AS input8;
    output1      AS outputNAND4;
  }
}

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."; } 

}