and16series.cta

很好的一本书

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

/* 
 * project: implementation of an 16-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)
 *
 */

// 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 pMOSTransistorLow is initialized to low
MODULE pMOSTransistorLow
{
  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 1 -> outerVal = 0. 
  INITIAL   STATE(pMOS) = stable0
                   AND c = u AND outerVal = 0;  
    
  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 nMOSTransistorHigh is initialized to high
MODULE nMOSTransistorHigh
{
  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 1 -> outerVal = 1.
  INITIAL   STATE(nMOS) = stable1
                   AND c = u AND outerVal = 1;  
    
  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
}

// 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 uses two instances of pMOS transistors and two instances of
// nMOS transistors to build a NOR gate with two inputs.
MODULE NORGateLow
{
 
  INPUT
    lp           : CONST;
    ln           : CONST;
    up           : CONST;
    un           : CONST;

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

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

  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;