StaticDoc.tioga
Rick Barth, December 9, 1986 12:05:38 pm PST
Static
CEDAR 6.0 — FOR INTERNAL XEROX USE ONLY
Static
Rick Barth
© Copyright 1985 Xerox Corporation. All rights reserved.
Abstract: Static checks that some interesting invariants hold.
Created by: Rick Barth
Maintained by: Barth <Barth.pa>
Keywords: design automation, static checking
XEROX   Xerox Corporation
    Palo Alto Research Center
    3333 Coyote Hill Road
    Palo Alto, California 94304

For Internal Xerox Use Only
Things checked by the old static:
Node pulled up more than once
depletion transitor not a pullup or a superbuffer
Assuming lightning arrested node is an Input
Assuming unsettable node is an Input
pullup/pulldown ratio =
*tpulled down (1/%d) by node %n thru %ld by %ld to node %n*n
Node name only occurs once
Node can never be set to 1
Node can never be set to 0
Value not used
Sum of 1/Z's for all pullups
Non-restored node controlling pass transistor
Gate is GND
gate is the same node as source or drain
Gate is VDD
Things which are checked by the new static:
Node name only occurs once => single connection or no connection?
Things which should be checked by the new static:
wire property to suppress these
Node can never be set to 1 check that some pE chain leads to Vdd
Node can never be set to 0 check that some nE chain leads to Gnd
Value not used => node never sensed
instance and/or celltype property to suppress these
gate is the same node as source or drain
Gate is GND
Gate is VDD
Things which might be checked by the new static:
Check that drive up and drive down ratios make sense.
pullup/pulldown ratio =
*tpulled down (1/%d) by node %n thru %ld by %ld to node %n*n
Sum of 1/Z's for all pullups
Non-restored node controlling pass transistor. Check that pass transistors can be completely shut off, i.e. for nE pass transistors check that the path to ground of the gate can pass through only nE transistors, and the opposite for pE.
Static.mesa
Copyright © 1986 by Xerox Corporation. All rights reserved.
Barth, October 22, 1986 11:48:09 am PDT
DIRECTORY Core, CoreFlat;
Static: CEDAR DEFINITIONS = BEGIN
Theory
This interface does interesting static checks.
Types
ROPE: TYPE = Core.ROPE;
Nodes Driven and Sensed
NotDrivenOK: PROC [wire: Core.Wire] RETURNS [same: Core.Wire];
Marks the wire with a property which suppresses either or both of the cannotBe1 and cannotBe0 error messages.
NotSensedOK: PROC [wire: Core.Wire] RETURNS [same: Core.Wire];
Marks the wire with a property which suppresses the neverSensed error message.
DrivenAndSensed: PROC [root: Core.CellType, quitAfter: INT ← 100] RETURNS [errors: Errors ← NIL];
Vdd is defined as a public wire of root marked with the property $RoseFixedWire with value H. Gnd is defined as a public wire of root marked with the property $RoseFixedWire with value L. Checks that every atomic wire reachable from root has a transistor chain to Vdd, that every atomic wire has a transistor chain to Gnd, and that every atomic wire is transitively connected through transistor channels, without going through Vdd or Gnd, to at least one transistor gate. Checks that every wire directly connected to a transistor gate has a pE chain to Vdd and a nE chain to Gnd. Stops looking for more errors when quitAfter errors have been found.
This is trivial to compute given the Rosemary flat representation of the circuit. The right way to implement this may be as a function in the Rosemary interface which performs all these checks given a simulation. The reason it is here is so that an algorithm which does not flatten the circuit can be thought about.
Connection Count
ConnectionCountProc: TYPE = PROC [count: INT, wireRoot: Core.Wire, wire: Core.Wire, public: BOOL, cellType: Core.CellType, unconnectedOK: BOOL];
IF public THEN
wire is a public of root
cellType is root
ELSE cellType is the record cell parent of wire
staticCutSetProp: ATOM; -- $StaticCutSet
UnconnectedOK: PROC [wire: Core.Wire] RETURNS [same: Core.Wire];
Marks the wire with a property which suppresses the bad connection count error message. The property is not propagated across cell boundaries by public actual bindings. It is propagated from a parent wire to its children.
CheckCount: ConnectionCountProc;
Checks that every internal wire has at least two connections and that every public wire has at least one connection. Reports any wire which doesn't with TerminalIO. Wires marked with UnconnectedOK do not have error messages generated.
CountLeafConnections: PROC [root: Core.CellType, eachWireCount: ConnectionCountProc, cutSet: CoreFlat.CutSet ← NIL];
Counts the connections to each atomic wire reachable from root. Calls eachWireCount with the number of leaf connections on a wire. If cutSet is NIL then checks the root for staticCutSetProp.
CountDirectConnections: PROC [root: Core.CellType, eachWireCount: ConnectionCountProc, cutSet: CoreFlat.CutSet ← NIL];
Counts the connections to each atomic wire reachable from root. Calls eachWireCount with the number of direct connections on a wire. If cutSet is NIL then checks the root for staticCutSetProp.
END.
ErrorType: TYPE = {none, cannotBe1, cannotBe0, neverSensed};
Errors: TYPE = LIST OF Error;
Error: TYPE = REF ErrorRec;
ErrorRec: TYPE = RECORD [
wire: CoreFlat.FlatWire ← NIL,
type: ErrorType ← none];
notDrivenAtom: ATOM = $StaticNotDriven;
notSensedAtom: ATOM = $StaticNotSensed;
okAtom: ATOM = $OK;
DASInfo: TYPE = REF DASInfoRec;
DASInfoRec: TYPE = RECORD [
nEequivalent: Core.Wires ← NIL,
pEequivalent: Core.Wires ← NIL,
hasGate: BOOL ← FALSE];
NotDrivenOK: PUBLIC PROC [wire: Core.Wire] RETURNS [same: Core.Wire] = {
CoreProperties.PutWireProp[on: wire, prop: notDrivenAtom, value: okAtom];
same ← wire;
};
NotSensedOK: PUBLIC PROC [wire: Core.Wire] RETURNS [same: Core.Wire] = {
CoreProperties.PutWireProp[on: wire, prop: notSensedAtom, value: okAtom];
same ← wire;
};
EnoughErrors: SIGNAL = CODE;
DrivenAndSensed: PUBLIC PROC [root: Core.CellType, quitAfter: INT ← 100] RETURNS [errors: Errors ← NIL] = {
Within a cell compute the pE and nE vicinities. Vicinities which are not connected to public wires are in error, all wires within the vicinity are in error. A set of public wires may be connected to a vicinity. A hash table can represent a vicinity. Must be able to union hash tables to do things that way.
Check: PROC [cell: Core.CellType, flatCell: CoreFlat.FlatCellTypeRec ← CoreFlat.rootCellType] = {
GetPublicInfo: PROC [publicWire: Core.Wire, thisCell: Core.CellType, thisFlatCell: CoreFlat.FlatCellTypeRec] RETURNS [publicInfo: DASInfo] = {
publicInfo ← NARROW[HashTable.Fetch[publicTable, publicWire].value];
IF publicInfo=NIL THEN {
Check[thisCell, thisFlatCell];
publicInfo ← NARROW[HashTable.Fetch[publicTable, publicWire].value];
IF publicInfo=NIL THEN ERROR;
};
};
SELECT TRUE FROM
cell.class=CoreClasses.transistorCellClass => {
tranData: CoreClasses.Transistor ← NARROW[cell.data];
gate: NAT = CoreClasses.TransistorPort.gate.ORD;
ch1: NAT = CoreClasses.TransistorPort.ch1.ORD;
ch2: NAT = CoreClasses.TransistorPort.ch2.ORD;
public: Core.Wire ← cell.public;
channelData: DASInfo ← NEW[DASInfoRec];
equivalent: Core.Wires ← LIST[public[ch1], public[ch2]];
IF tranData.type=nE THEN channelData.nEequivalent ← equivalent ELSE channelData.pEequivalent ← equivalent;
IF NOT HashTable.Insert[publicTable, public[gate], NEW[DASInfoRec ← [hasGate: TRUE]]] THEN ERROR;
IF NOT HashTable.Insert[publicTable, public[ch1], channelData] THEN ERROR;
IF NOT HashTable.Insert[publicTable, public[ch2], channelData] THEN ERROR;
};
cell.class=CoreClasses.recordCellClass => {
InsertRecordPublic: PROC [wire: Core.Wire] = {
[] ← HashTable.Insert[publicTable, wire, NEW[WireInfoRec]];
};
CheckInternal: PROC [wire: Core.Wire] = {
internalInfo: WireInfo ← NIL;
IF HashTable.Fetch[publicTable, wire].found THEN RETURN;
IF HashTable.Fetch[visitCheck, wire].found THEN RETURN;
IF NOT HashTable.Insert[visitCheck, wire, $Visited] THEN ERROR;
internalInfo ← NARROW[HashTable.Fetch[internalTable, wire].value];
IF NOT internalInfo.hasGate THEN {
errors ← CONS[?, errors];
quitAfter ← quitAfter - 1;
IF quitAfter=0 THEN SIGNAL EnoughErrors[];
};
};
rct: CoreClasses.RecordCellType ← NARROW[cell.data];
internalTable: HashTable.Table ← HashTable.Create[];
visitCheck: HashTable.Table ← HashTable.Create[];
CoreOps.VisitRootAtomics[cell.public, InsertRecordPublic];
FOR i: NAT IN [0..rct.size) DO
ComputeInternal: CoreOps.EachWirePairProc = {
actualInfo, publicInfo: WireInfo;
IF publicWire.size>0 THEN RETURN;
IF HashTable.Fetch[visitCompute, publicWire].found THEN RETURN;
IF NOT HashTable.Insert[visitCompute, publicWire, $Visited] THEN ERROR;
publicInfo ← GetPublicInfo[publicWire, rct[i].type, [CoreFlat.ExtendPath[flatCell.path, i, rct], 0], rct[i]];
actualInfo ← NARROW[HashTable.Fetch[internalTable, actualWire].value];
IF actualInfo=NIL THEN {
actualInfo ← NARROW[HashTable.Fetch[publicTable, actualWire].value];
IF actualInfo=NIL THEN {
actualInfo ← NEW[WireInfoRec];
IF NOT HashTable.Insert[internalTable, actualWire, actualInfo] THEN ERROR;
};
};
actualInfo.count ← actualInfo.count + publicInfo.count;
};
visitCompute: HashTable.Table ← HashTable.Create[];
IF CoreOps.VisitBindingSeq[rct[i].actual, rct[i].type.public, ComputeInternal] THEN ERROR;
ENDLOOP;
PropagateUnconnectedOK[rct.internal, internalTable];
CoreOps.VisitRootAtomics[rct.internal, CheckInternal];
};
ENDCASE => {
ComputePublicCount: CoreOps.EachWirePairProc = {
publicInfo: WireInfo;
IF publicWire.size>0 THEN RETURN;
publicInfo ← GetPublicInfo[publicWire, thisCell, [flatCell.path, flatCell.recastCount+1], instance];
[] ← HashTable.Insert[publicTable, actualWire, publicInfo];
};
thisCell: Core.CellType ← CoreOps.Recast[cell];
IF thisCell=cell THEN Check[cell, flatCell, instance]
ELSE IF CoreOps.VisitBindingSeq[cell.public, thisCell.public, ComputePublicCount] THEN ERROR;
};
};
publicTable: HashTable.Table ← HashTable.Create[]; -- Core.Wire to DASInfo
ComputeVicinities[root ! EnoughErrors => GOTO quit];
Check that some wire of each nEequivalent public wires of root are marked L, and pEequivalent are H. Check that all public wires of root have hasGate set to TRUE.
EXITS quit => NULL;
};