[_CD4_]<datools7.0>Static>StaticDoc.tioga!1

StaticDoc.tioga

Rick Barth, December 9, 1986 12:05:38 pm PST

Bertrand Serlet March 30, 1987 9:59:08 pm PST

Static

CEDAR 7.0 — FOR INTERNAL XEROX USE ONLY

Static

Rick Barth

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

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;

};