and16series.cta

很好的一本书

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

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

////////////////////////////////////////////////

  LOCAL
    outerVal     : DISCRETE(1);
  LOCAL
    outputNAND05  : DISCRETE(1);

  INST fNOR3 FROM NORGateLow WITH
  {
    lp           AS lp;
    ln           AS ln;
    up           AS up;
    un           AS un;
    input1       AS outputNAND5;
    input2       AS outputNAND05;
    output1      AS outerVal;
  }

////////////////////////////////////////////////

  INST binp01 FROM inputLow WITH
  {
    lx           AS lx;
    ux           AS ux;
    outerVal     AS input01;
    c            AS c;
  } 

  LOCAL
    input01       : DISCRETE(1);
  
  INST binp02 FROM inputLow WITH
  {
    lx           AS lx;
    ux           AS ux;
    outerVal     AS input02;
    c            AS c;
  }  

  LOCAL
    input02       : DISCRETE(1);     

  LOCAL
    outputNAND01  : DISCRETE(1);
    
  INST cNAND01 FROM NANDGateHigh WITH
  {
    lp           AS lp;
    ln           AS ln;
    up           AS up;
    un           AS un;
    input1       AS input01;
    input2       AS input02;
    output1      AS outputNAND01;
  }

  LOCAL
    outputNOR01   : DISCRETE(1);  

  LOCAL
    outputNAND02  : DISCRETE(1);

  INST dNOR01 FROM NORGateLow WITH
  {
    lp           AS lp;
    ln           AS ln;
    up           AS up;
    un           AS un;
    input1       AS outputNAND01;
    input2       AS outputNAND02;
    output1      AS outputNOR01;
  }

  INST binp03 FROM inputLow WITH
  {
    lx           AS lx;
    ux           AS ux;
    outerVal     AS input03;
    c            AS c;
  }

  LOCAL
    input03       : DISCRETE(1);
  
  INST binp04 FROM inputLow WITH
  {
    lx           AS lx;
    ux           AS ux;
    outerVal     AS input04;
    c            AS c;
  }

  LOCAL
    input04       : DISCRETE(1);
  
  INST cNAND02 FROM NANDGateHigh WITH
  {
    lp           AS lp;
    ln           AS ln;
    up           AS up;
    un           AS un;
    input1       AS input03;
    input2       AS input04;
    output1      AS outputNAND02;
  }

  LOCAL
    outputNOR02   : DISCRETE(1);

  INST eNAND05 FROM NANDGateHigh WITH
  {
    lp           AS lp;
    ln           AS ln;
    up           AS up;
    un           AS un;
    input1       AS outputNOR01;
    input2       AS outputNOR02;
    output1      AS outputNAND05;
  }

  INST binp05 FROM inputLow WITH
  {
    lx           AS lx;
    ux           AS ux;
    outerVal     AS input05;
    c            AS c;
  }

  LOCAL
    input05       : DISCRETE(1);
  
  INST binp06 FROM inputLow WITH
  {
    lx           AS lx;
    ux           AS ux;
    outerVal     AS input06;
    c            AS c;
  }

  LOCAL
    input06       : DISCRETE(1);
  
  LOCAL
    outputNAND03  : DISCRETE(1);

  INST cNAND03 FROM NANDGateHigh WITH
  {
    lp           AS lp;
    ln           AS ln;
    up           AS up;
    un           AS un;
    input1       AS input05;
    input2       AS input06;
    output1      AS outputNAND03;
  }

  LOCAL
    outputNAND04  : DISCRETE(1);	

  INST dNOR02 FROM NORGateLow WITH
  {
    lp           AS lp;
    ln           AS ln;
    up           AS up;
    un           AS un;
    input1       AS outputNAND03;
    input2       AS outputNAND04;
    output1      AS outputNOR02;
  }

  INST binp07 FROM inputLow WITH
  {
    lx           AS lx;
    ux           AS ux;
    outerVal     AS input07;
    c            AS c;
  }

  LOCAL
    input07       : DISCRETE(1);

  INST binp08 FROM inputLow WITH
  {
    lx           AS lx;
    ux           AS ux;
    outerVal     AS input08;
    c            AS c;
  }

  LOCAL
    input08       : DISCRETE(1);

  INST cNAND04 FROM NANDGateHigh WITH
  {
    lp           AS lp;
    ln           AS ln;
    up           AS up;
    un           AS un;
    input1       AS input07;
    input2       AS input08;
    output1      AS outputNAND04;
  }

}

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

}