
    <<RosemaryImpl.mesa>>
        <<Copyright © 1985 by Xerox Corporation.  All rights reserved.>>
        <<Barth, March 25, 1986 10:24:50 am PST>>
        <<Louis Monier January 10, 1986 2:48:21 pm PST>>
        <<Bertrand Serlet March 18, 1986 2:58:17 pm PST>>
        <<Last Edited by: Neil Gunther February 27, 1986 12:00:12 pm PST>>
        <<Curry, March 11, 1986 12:06:50 pm PST>>
        <<>>
    DIRECTORY Basics, BitHacks, Core, CoreClasses, CoreOps, CoreProperties, Ports, Process, Rope, Rosemary, RefTab, SymTab;

    RosemaryImpl: CEDAR PROGRAM
        IMPORTS Basics, BitHacks, CoreClasses, CoreOps, CoreProperties, Ports, Process, Rope, RefTab, SymTab
        EXPORTS Rosemary
        = BEGIN OPEN Rosemary;

ROPE: TYPE = Core.ROPE;
    WordAsBits: TYPE = PACKED ARRAY [0..16) OF BOOL;
    DWordAsBits: TYPE = PACKED ARRAY [0..32) OF BOOL;
    RoseWireList: TYPE = LIST OF RoseWire;

    roseBehaveProp: ATOM = CoreProperties.RegisterProperty[prop: $RoseBehave];
    roseWireSizeProp: ATOM = CoreProperties.RegisterProperty[prop: $RoseWireSize];
    roseFixedWireProp: ATOM = CoreProperties.RegisterProperty[prop: $RoseFixedWire];
    roseTransistorSizeProp: ATOM = CoreProperties.RegisterProperty[prop: $RoseTransistorSize];
    roseCutSetProp: ATOM = CoreProperties.RegisterProperty[prop: $RoseCutSet];
    roseClassTable: SymTab.Ref _ SymTab.Create[];

    WireBind: TYPE = REF WireBindRec;
    WireBindRec: TYPE = RECORD [
        path: PackedPath,
        wire: Core.Wire _ NIL,
        valid: BOOL _ TRUE];

<<Behaviour>>
    BindCellType: PUBLIC PROC [cellType: Core.CellType, roseClassName: ROPE] RETURNS [sameCellType: Core.CellType] = {
        CoreProperties.PutCellTypeProp[on: cellType, prop: roseBehaveProp, value: roseClassName];
        sameCellType _ cellType;
        };

    BindCellClass: PUBLIC PROC [cellClass: Core.CellClass, roseClassName: ROPE] RETURNS [sameCellClass: Core.CellClass] = {
        CoreProperties.PutCellClassProp[on: cellClass, prop: roseBehaveProp, value: roseClassName];
        sameCellClass _ cellClass;
        };

    Register: PUBLIC PROC [roseClassName: ROPE, init: InitProc _ NIL, evalSimple: EvalProc _ NIL] RETURNS [sameRoseClassName: ROPE] = {
        found: BOOL;
        val: REF ANY;
        [found, val] _  SymTab.Fetch[x: roseClassTable, key: roseClassName];
        IF found THEN {
            rct: RoseCellType _ NARROW[val];
            rct.init _ init;
            rct.evalSimple _ evalSimple;
            }
        ELSE [] _  SymTab.Store[x: roseClassTable, key: roseClassName, val: NEW[RoseCellTypeRec _ [init: init, evalSimple: evalSimple]]];
        sameRoseClassName _ roseClassName;
        };

    Stop: PUBLIC SIGNAL [msg: ROPE, data: REF ANY _ NIL] = CODE;

<<Instantiation>>
AddCutSets: PUBLIC PROC [cellType: Core.CellType, cs1, cs2, cs3, cs4, cs5, cs6: ROPE _ NIL] RETURNS [sameCellType: Core.CellType] = 
{
cutSetList: LIST OF ROPE _ NARROW[CoreProperties.GetCellTypeProp[from: cellType, prop: roseCutSetProp]];
IF cs1#NIL THEN cutSetList _ CONS[cs1, cutSetList];
IF cs2#NIL THEN cutSetList _ CONS[cs2, cutSetList];
IF cs3#NIL THEN cutSetList _ CONS[cs3, cutSetList];
IF cs4#NIL THEN cutSetList _ CONS[cs4, cutSetList];
IF cs5#NIL THEN cutSetList _ CONS[cs5, cutSetList];
IF cs6#NIL THEN cutSetList _ CONS[cs6, cutSetList];
CoreProperties.PutCellTypeProp[on: cellType, prop: roseCutSetProp, value: cutSetList];
sameCellType _ cellType;
};

SetFixedWire: PUBLIC PROC [wire: Core.Wire, level: Ports.Level] RETURNS [sameWire: Core.Wire] = {
    CoreProperties.PutWireProp[on: wire, prop: roseFixedWireProp, value: NEW[Ports.Level _ level]];
    sameWire _ wire;
};

SetWireSize: PUBLIC PROC [wire: Core.Wire, size: WireSize] RETURNS [sameWire: Core.Wire] = {
    CoreProperties.PutWireProp[on: wire, prop: roseWireSizeProp, value: NEW[Ports.Drive _ size]];
    sameWire _ wire;
};

SetTransistorCellTypeSize: PUBLIC PROC [transistor: Core.CellType, size: TransistorSize] RETURNS [sameTransistor: Core.CellType] = {
    CoreProperties.PutCellTypeProp[on: transistor, prop: roseTransistorSizeProp, value: NEW[Ports.Drive _ size]];
    sameTransistor _ transistor;
};

SetTransistorInstanceSize: PUBLIC PROC [transistor: CoreClasses.CellInstance, size: TransistorSize] RETURNS [sameTransistor: 
CoreClasses.CellInstance] = {
    CoreProperties.PutCellInstanceProp[on: transistor, prop: roseTransistorSizeProp, value: NEW[Ports.Drive _ size]];
    sameTransistor _ transistor;
};

    InstantiateCellType: PUBLIC PROC [cellType: Core.CellType, testPort: Ports.Port, statePoints: NAT _ 0] RETURNS [simulation: 
    Simulation] = {
        roseInstance: RoseCellInstance _ NEW[RoseCellInstanceRec];
        max: CARDINAL;
        wireToRoseWire: RefTab.Ref _ RefTab.Create[];
        simulation _ NEW[SimulationRec];
        simulation.coreCellType _ cellType;
        simulation.coreToRoseInstances[0] _ roseInstance;
        simulation.instanceNeedEval _ roseInstance;
        FOR strength: Ports.Drive IN Ports.Drive DO
            simulation.vicinityByStrength[strength].wires _ NEW[RoseWireSeq[1]];
            ENDLOOP;
        roseInstance.publicPort _ Ports.CreatePort[cellType.public];
        [max, simulation.roseBoolWires] _ AllocateCellTypeRoseWires[simulation, roseInstance.publicPort, cellType.public, wireToRoseWire];
        simulation.scratchValue _ NEW[Ports.LevelSequenceRec[max]];
        simulation.scratchDrive _ NEW[DriveRec[max]];
        roseInstance.roseCellType _ FindRoseCellType[cellType];
        IF roseInstance.roseCellType.init#NIL THEN roseInstance.state _ roseInstance.roseCellType.init[cellType: cellType, p: 
        roseInstance.publicPort];
        roseInstance.portBindings _ NEW[PortBindingSeq[Ports.PortLeaves[ roseInstance.publicPort]]];
        IF roseInstance.portBindings.size#ComputeCellTypeBindings[instance: roseInstance, port: roseInstance.publicPort, wire: 
        cellType.public, wireToRoseWire: wireToRoseWire, binds: roseInstance.portBindings, firstFreeBinding: 0] THEN ERROR;
        simulation.publicBindings _ NEW[PortBindingSeq[Ports.PortLeaves[testPort]]];
        IF simulation.publicBindings.size#ComputeCellTypeBindings[port: testPort, wire: cellType.public, wireToRoseWire: wireToRoseWire, 
        binds: simulation.publicBindings, firstFreeBinding: 0] THEN ERROR;
        FOR hash: HashIndex IN HashIndex DO
            FOR roseWire: RoseWire _ simulation.coreToRoseWires[hash], roseWire.nextBucket UNTIL roseWire=NIL DO
                IF roseWire.wireDrive=infinite THEN UpdateReaders[simulation, roseWire, NIL];
                ENDLOOP;
            ENDLOOP;
        simulation.testPort _ testPort;
        AllocateStatePoints[simulation, statePoints];
        EstablishInvariants[simulation];
        };

    AllocateCellTypeRoseWires: PROC [simulation: Simulation, port: Ports.Port, public: Core.Wire, wireToRoseWire: RefTab.Ref] RETURNS 
    [maxComposite: CARDINAL _ 0, boolWires: RoseWireList _ NIL] = {
        IF port.type=composite THEN {
            subBools: RoseWireList;
            subMax: CARDINAL;
            FOR sub: NAT IN [0..port.size) DO
                [subMax, subBools] _ AllocateCellTypeRoseWires[simulation, port[sub], public[sub], wireToRoseWire];
                maxComposite _ MAX[subMax, maxComposite];
                FOR bools: RoseWireList _ subBools, bools.rest UNTIL bools=NIL DO
                    boolWires _ CONS[bools.first, boolWires];
                    ENDLOOP;
                ENDLOOP;
            }
        ELSE {
            roseWire: RoseWire _ NEW[RoseWireRec];
            hash: HashIndex _ PathHash[[0, ALL[FALSE]], public];
            wireSizeRef: REF Ports.Drive _ NARROW[CoreProperties.GetWireProp[from: public, prop: roseWireSizeProp]];
            wireFixedRef: REF Ports.Level _ NARROW[CoreProperties.GetWireProp[from: public, prop: roseFixedWireProp]];
            IF wireSizeRef#NIL THEN roseWire.wireDrive _ wireSizeRef^;
            IF wireFixedRef#NIL THEN {
                roseWire.wireDrive _ infinite;
                roseWire.switchDrive _ infinite;
                roseWire.wireLevel _ wireFixedRef^
                };
            roseWire.connections _ NEW[FieldSeq[2]];
            IF NOT RefTab.Insert[x: wireToRoseWire, key: public, val: roseWire] THEN ERROR;
            IF port.type=l OR port.type=b THEN Perturb[simulation, roseWire]
            ELSE {
                maxComposite _ CoreOps.WireBits[public];
                roseWire.currentValue _ AllocateLevelSequence[maxComposite];
                };
            IF port.type=b OR port.type=bs OR port.type=c OR port.type=lc THEN boolWires _ CONS[roseWire, boolWires];
            roseWire.wire _ public;
            roseWire.nextBucket _ simulation.coreToRoseWires[hash];
            simulation.coreToRoseWires[hash] _ roseWire;
            };
        };

    ComputeCellTypeBindings: PROC [port: Ports.Port, wire: Core.Wire, wireToRoseWire: RefTab.Ref, binds: PortBindings, 
    firstFreeBinding: CARDINAL, instance: RoseCellInstance _ NIL] RETURNS [newFirstFreeBinding: CARDINAL] = {
        newFirstFreeBinding _ firstFreeBinding;
        IF port.type=composite THEN {
            FOR subPort: NAT IN [0..port.size) DO
                newFirstFreeBinding _ ComputeCellTypeBindings[port[subPort], wire[subPort], wireToRoseWire, binds, newFirstFreeBinding, instance];
                ENDLOOP;
            }
        ELSE {
            thisRoseWire: RoseWire _ NARROW[RefTab.Fetch[x: wireToRoseWire, key: wire].val];
            portBinding: PortBinding _ NEW[PortBindingRec _ [
                instance: instance,
                clientPort: port,
                fields: NEW[FieldSeq[1]],
                currentDrive: port.d]];
            field: Field _ NEW[FieldRec _ [
                portBinding: portBinding,
                roseWire: thisRoseWire]];
            portBinding.fields[0] _ field;
            field.currentValue _ AllocateLevelSequence[IF thisRoseWire.currentValue=NIL THEN 1 ELSE thisRoseWire.currentValue.size];
            binds[newFirstFreeBinding] _ portBinding;
            newFirstFreeBinding _ newFirstFreeBinding + 1;
            IF thisRoseWire.connections[0]=NIL THEN thisRoseWire.connections[0] _ field ELSE thisRoseWire.connections[1] _ field;
            };
        };

    InstantiateInstances: PUBLIC PROC [cellType: Core.CellType, testPort: Ports.Port, cutSet: ROPE _ NIL, statePoints: NAT _ 0] RETURNS 
    [simulation: Simulation] = {

        FindRoseWires: PROC [ct: Core.CellType] = {

            AllocateRoseWires: PROC [wire: Core.Wire] RETURNS [public: BOOL _ FALSE, allocated: BOOL _ FALSE] = {
                wireData: WireData _ NARROW[RefTab.Fetch[x: wireDataTab, key: wire].val];

                AllocateWire: PROC [wire: Core.Wire, wireData: WireData] = {

                    AllocateTransistorPointers: PROC [count: CARDINAL] RETURNS [transistors: RoseTransistors _ NIL] = {
                        IF count>0 THEN {
                            transistors _ NEW[RoseTransistorSeq[count]];
                            FOR i: CARDINAL IN [0..transistors.size) DO
                                transistors[i] _ NIL;
                                ENDLOOP;
                            };
                        };

                    roseWire: RoseWire _ NEW[RoseWireRec];
                    hash: HashIndex _ PathHash[packedPath, wire];
                    wireSize: NAT _ CoreOps.WireBits[wire];
                    IF wireData.connections>0 THEN {
                        roseWire.connections _ NEW[FieldSeq[wireData.connections]];
                        FOR i: CARDINAL IN [0..roseWire.connections.size) DO
                            roseWire.connections[i] _ NIL;
                            ENDLOOP;
                        };
                    IF wireSize>1 THEN roseWire.currentValue _ AllocateLevelSequence[wireSize]
                    ELSE {
                        wireSizeRef: REF Ports.Drive _ NARROW[CoreProperties.GetWireProp[from: wire, prop: roseWireSizeProp]];
                        wireFixedRef: REF Ports.Level _ NARROW[CoreProperties.GetWireProp[from: wire, prop: roseFixedWireProp]];
                        roseWire.channels _ AllocateTransistorPointers[wireData.channels];
                        roseWire.gates _ AllocateTransistorPointers[wireData.gates];
                        IF wireSizeRef#NIL THEN roseWire.wireDrive _ wireSizeRef^;
                        IF wireFixedRef#NIL THEN {
                            roseWire.wireDrive _ infinite;
                            roseWire.switchDrive _ infinite;
                            roseWire.wireLevel _ wireFixedRef^
                            };
                        Perturb[simulation, roseWire];
                        };
                    roseWire.path _ packedPath;
                    roseWire.wire _ wire;
                    roseWire.nextBucket _ simulation.coreToRoseWires[hash];
                    simulation.coreToRoseWires[hash] _ roseWire;
                    maxRoseWireSize _ MAX[maxRoseWireSize, wireSize];
                    IF wireData.boolPort THEN simulation.roseBoolWires _ CONS[roseWire, simulation.roseBoolWires];
                    wireData.allocated _ TRUE;
                    };

                IF NOT (public _ NOT PathEqual[wireData.path, packedPath]) THEN {
                    IF wireData.allocated THEN allocated _ TRUE
                    ELSE {
                        somePublic: BOOL _ FALSE;
                        FOR sub: NAT IN [0..wire.size) DO
                            subPublic, subAllocated: BOOL;
                            [subPublic, subAllocated] _ AllocateRoseWires[wire[sub]];
                            allocated _ allocated OR subAllocated;
                            somePublic _ somePublic OR subPublic;
                            ENDLOOP;
                        IF allocated OR somePublic THEN {
                            FOR sub: NAT IN [0..wire.size) DO
                                subWireData: WireData _ NARROW[RefTab.Fetch[x: wireDataTab, key: wire[sub]].val];
                                IF (NOT subWireData.allocated) AND PathEqual[subWireData.path, packedPath] THEN AllocateWire[wire[sub], subWireData];
                                ENDLOOP;
                            wireData.allocated _ TRUE;
                            }
                        ELSE {
                            IF wireData.indegree>1 OR wireData.portLeaf THEN {
                                AllocateWire[wire, wireData];
                                allocated _ TRUE;
                                };
                            };
                        };
                    wireData.indegree _ 0;
                    };
                };

            rct: CoreClasses.RecordCellType _ NARROW[ct.data];
            pathBits: NAT _ BitHacks.NBits[rct.size];
            FOR i:NAT IN [0..rct.internal.size) DO
                ComputeInDegree[rct.internal[i]];
                ENDLOOP;
            FOR in: NAT IN [0..rct.size) DO
                member, transistor: BOOL;
                subType: Core.CellType;
                [member, transistor, subType] _ CutSetMember[packedPath, rct[in], cutSet];
                IF member THEN {
                    IF transistor THEN {
                        actual: Core.Wire _ rct[in].actual;
                        wireData: WireData _ NARROW[RefTab.Fetch[x: wireDataTab, key: actual[gate]].val];
                        wireData.gates _ wireData.gates + 1;
                        wireData.portLeaf _ TRUE;
                        wireData _ NARROW[RefTab.Fetch[x: wireDataTab, key: actual[ch1]].val];
                        wireData.channels _ wireData.channels + 1;
                        wireData.portLeaf _ TRUE;
                        wireData _ NARROW[RefTab.Fetch[x: wireDataTab, key: actual[ch2]].val];
                        wireData.portLeaf _ TRUE;
                        wireData.channels _ wireData.channels + 1;
                        }
                    ELSE {
                        visited: RefTab.Ref _ RefTab.Create[];
                        FOR i: NAT IN [0..rct[in].actual.size) DO
                            MarkPortLeavesCountConnections[actual: rct[in].actual[i], public: rct[in].type.public[i], checkPort: TRUE, visited: visited]
                            ENDLOOP;
                        };
                    }
                ELSE {
                    rc: Core.CellType _ Recordify[subType];

                    BindPublicToActual: CoreOps.EachWirePairProc = {
                        val: REF ANY _ RefTab.Fetch[x: wireDataTab, key: actualWire].val;
                        IF val=NIL THEN ERROR;
                        [] _ RefTab.Store[x: wireDataTab, key: publicWire, val: val];
                        };

                    FOR i: NAT IN [0..rct[in].actual.size) DO
                        IF CoreOps.VisitBinding[actual: rct[in].actual[i], public: rc.public[i], eachWirePair: BindPublicToActual] THEN ERROR;
                        ENDLOOP;
                    FOR bit: NAT IN [0..pathBits) DO
                        packedPath.bits[packedPath.length+bit] _ BitHacks.XthBitOfN[pathBits-bit-1, in];
                        ENDLOOP;
                    packedPath.length _ packedPath.length + pathBits;
                    FindRoseWires[ct: rc];
                    packedPath.length _ packedPath.length - pathBits;
                    };
                ENDLOOP;
            FOR i: NAT IN [0..rct.internal.size) DO
                [] _ AllocateRoseWires[rct.internal[i]];
                ENDLOOP;
            };

        AllocateRoseInstances: PROC [ct: Core.CellType] = {

            MarkInvalid: CoreOps.EachWireProc = {
                bind: WireBind _ NARROW[RefTab.Fetch[x: wireBindTab, key: wire].val];
                IF bind#NIL THEN bind.valid _ FALSE;
                };

            MarkValid: CoreOps.EachWireProc = {
                bind: WireBind _ NARROW[RefTab.Fetch[x: wireBindTab, key: wire].val];
                IF bind#NIL THEN bind.valid _ TRUE;
                };

            rct: CoreClasses.RecordCellType _ NARROW[ct.data];
            pathBits: NAT _ BitHacks.NBits[rct.size];
            FOR in: NAT IN [0..rct.size) DO
                member, transistor: BOOL;
                coreInstance: CoreClasses.CellInstance _ rct[in];
                subType: Core.CellType;
                [member, transistor, subType] _ CutSetMember[packedPath, coreInstance, cutSet];
                IF member THEN {
                    IF transistor THEN {

                        InsertTransistor: PROC [transistors: RoseTransistors] = {
                            FOR t: NAT IN [0..transistors.size) DO
                                IF transistors[t]=NIL THEN {
                                    transistors[t] _ roseTransistor;
                                    EXIT;
                                    };
                                REPEAT
                                    FINISHED => ERROR;
                                ENDLOOP;
                            };

                        coreTransistor: CoreClasses.Transistor _ NARROW[subType.data];
                        roseTransistor: RoseTransistor _ NEW[RoseTransistorRec];
                        actual: Core.Wire _ coreInstance.actual;
                        transistorSizeRef: REF Ports.Drive _ NARROW[CoreProperties.GetCellInstanceProp[from: coreInstance, prop: roseTransistorSizeProp]];
                        roseTransistor.gate _ LookUpRoseWire[actual[gate]];
                        InsertTransistor[roseTransistor.gate.gates];
                        roseTransistor.ch1 _ LookUpRoseWire[actual[ch1]];
                        InsertTransistor[roseTransistor.ch1.channels];
                        roseTransistor.ch2 _ LookUpRoseWire[actual[ch2]];
                        InsertTransistor[roseTransistor.ch2.channels];
                        IF transistorSizeRef=NIL THEN transistorSizeRef _ NARROW[CoreProperties.GetCellTypeProp[from: subType, prop: 
                        roseTransistorSizeProp]];
                        IF transistorSizeRef#NIL THEN roseTransistor.conductivity _ transistorSizeRef^;
                        roseTransistor.type _ coreTransistor.type;
                        }
                    ELSE {
                        roseInstance: RoseCellInstance _ NEW[RoseCellInstanceRec];
                        hash: HashIndex _ PathHash[packedPath, coreInstance];
                        roseInstance.nextNeedEval _ simulation.instanceNeedEval;
                        simulation.instanceNeedEval _ roseInstance;
                        roseInstance.roseCellType _ FindRoseCellType[subType];
                        roseInstance.publicPort _ Ports.CreatePort[wire: subType.public];
                        roseInstance.portBindings _ NEW[PortBindingSeq[Ports.PortLeaves[ roseInstance.publicPort]]];
                        IF roseInstance.portBindings.size#ComputeBindings[instance: roseInstance, port: roseInstance.publicPort, wire: coreInstance.actual, 
                        binds: roseInstance.portBindings, firstFreeBinding: 0] THEN ERROR;
                        IF roseInstance.roseCellType.init#NIL THEN roseInstance.state _ roseInstance.roseCellType.init[cellType: coreInstance.type, p: 
                        roseInstance.publicPort];
                        roseInstance.path _ packedPath;
                        roseInstance.instance _ coreInstance;
                        roseInstance.nextBucket _ simulation.coreToRoseInstances[hash];
                        simulation.coreToRoseInstances[hash] _ roseInstance;
                        };
                    }
                ELSE {
                    rc: Core.CellType _ Recordify[subType];

                    BindPublicToActual: CoreOps.EachWirePairProc = {
                        bind: WireBind _ NARROW[RefTab.Fetch[x: wireBindTab, key: actualWire].val];
                        IF bind=NIL THEN bind _ NEW[WireBindRec _ [
                            path: packedPath,
                            wire: actualWire]]
                        ELSE IF NOT bind.valid THEN bind.path _ packedPath;
                        [] _ RefTab.Store[x: wireBindTab, key: publicWire, val: bind];
                        };

                    FOR i: NAT IN [0..rct[in].actual.size) DO
                        IF CoreOps.VisitBinding[actual: rct[in].actual[i], public: rc.public[i], eachWirePair: BindPublicToActual] THEN ERROR;
                        ENDLOOP;
                    FOR bit: NAT IN [0..pathBits) DO
                        packedPath.bits[packedPath.length+bit] _ BitHacks.XthBitOfN[pathBits-bit-1, in];
                        ENDLOOP;
                    packedPath.length _ packedPath.length + pathBits;
                    AllocateRoseInstances[ct: rc];
                    packedPath.length _ packedPath.length - pathBits;
                    };
                ENDLOOP;
            IF CoreOps.VisitWire[rct.internal, MarkInvalid] THEN ERROR;
            IF CoreOps.VisitWire[ct.public, MarkValid] THEN ERROR;
            };

        ComputeInDegree: PROC [wire: Core.Wire] = {
            found: BOOL;
            wireDataAny: REF;
            wireData: WireData;
            [found, wireDataAny] _ RefTab.Fetch[x: wireDataTab, key: wire];
            IF found THEN wireData _ NARROW[wireDataAny]
            ELSE {
                wireData _ NEW[WireDataRec];
                IF NOT RefTab.Insert[x: wireDataTab, key: wire, val: wireData] THEN ERROR;
                };
            IF wireData.indegree=0 THEN {
                wireData.path _ packedPath;
                wireData.indegree _ 1;
                wireData.connections _ 0;
                wireData.channels _ 0;
                wireData.gates _ 0;
                wireData.portLeaf _ FALSE;
                wireData.boolPort _ FALSE;
                wireData.allocated _ FALSE;
                FOR sub: NAT IN [0..wire.size) DO
                    ComputeInDegree[wire[sub]];
                    ENDLOOP;
                }
            ELSE wireData.indegree _ wireData.indegree + 1;
            };

        MarkPortLeavesCountConnections: PROC [actual: Core.Wire, public: Core.Wire, checkPort: BOOL, visited: RefTab.Ref, type: 
        Ports.PortType _ composite] = {
            actualData: WireData _ NARROW[RefTab.Fetch[x: wireDataTab, key: actual].val];
            IF NOT RefTab.Fetch[x: visited, key: actual].found THEN {
                actualData.connections _ actualData.connections + 1;
                IF checkPort THEN {
                    type _ Ports.WirePortType[public];
                    IF type # composite THEN {
                        actualData.portLeaf _ TRUE;
                        checkPort _ FALSE;
                        };
                    };
                FOR sub: NAT IN [0..actual.size) DO
                    MarkPortLeavesCountConnections[actual[sub], public[sub], checkPort, visited, type];
                    ENDLOOP;
                IF NOT RefTab.Insert[x: visited, key: actual, val: $Visited] THEN ERROR;
                };
            IF type=b OR type=bs OR type=c OR type=lc THEN actualData.boolPort _ TRUE;
            };

        ComputeBindings: PROC [port: Ports.Port, wire: Core.Wire, binds: PortBindings, firstFreeBinding: CARDINAL, instance: 
        RoseCellInstance _ NIL] RETURNS [newFirstFreeBinding: CARDINAL] = {
            newFirstFreeBinding _ firstFreeBinding;
            IF port.type=composite THEN {
                FOR subPort: NAT IN [0..port.size) DO
                    newFirstFreeBinding _ ComputeBindings[port[subPort], wire[subPort], binds, newFirstFreeBinding, instance];
                    ENDLOOP;
                }
            ELSE {
                portBinding: PortBinding _ NEW[PortBindingRec _ [
                    clientPort: port,
                    currentDrive: port.d,
                    instance: instance]];
                portBinding.fields _ NEW[FieldSeq[CountFields[wire: wire, bound: RefTab.Create[]]]];
                [] _ ComputeFields[wire: wire, portBinding: portBinding, valueStart: 0, bound: RefTab.Create[], firstFreeField: 0];
                binds[newFirstFreeBinding] _ portBinding;
                newFirstFreeBinding _ newFirstFreeBinding + 1;
                };
            };

        CountFields: PROC [wire: Core.Wire, bound: RefTab.Ref] RETURNS [fieldCount: CARDINAL _ 0] = {
            IF LookUpRoseWire[wire]=NIL THEN {
                FOR subWire: NAT IN [0..wire.size) DO
                    fieldCount _ fieldCount + CountFields[wire[subWire], bound];
                    ENDLOOP;
                }
            ELSE {
                IF NOT RefTab.Fetch[x: bound, key: wire].found THEN {
                    fieldCount _ 1;
                    IF NOT RefTab.Insert[x: bound, key: wire, val: $Bound] THEN ERROR;
                    };
                };
            };

        ComputeFields: PROC [wire: Core.Wire, portBinding: PortBinding, valueStart: NAT, bound: RefTab.Ref, firstFreeField: CARDINAL] 
        RETURNS [newFirstFreeField: CARDINAL, newValueStart: NAT] = {
            roseWire: RoseWire _ LookUpRoseWire[wire];
            newValueStart _ valueStart;
            newFirstFreeField _ firstFreeField;
            IF roseWire = NIL THEN {
                FOR subWire: NAT IN [0..wire.size) DO
                    [newFirstFreeField, newValueStart] _ ComputeFields[wire[subWire], portBinding, newValueStart, bound, newFirstFreeField];
                    ENDLOOP;
                }
            ELSE {
                IF NOT RefTab.Fetch[x: bound, key: wire].found THEN {
                    field: Field _ NEW[FieldRec _ [
                        portBinding: portBinding,
                        portStartBit: valueStart,
                        roseWire: roseWire,
                        currentValue: AllocateLevelSequence[IF roseWire.currentValue=NIL THEN 1 ELSE roseWire.currentValue.size]]];
                    FOR bit: NAT IN [0..field.currentValue.size) DO
                        field.currentValue[bit] _ L;
                        ENDLOOP;
                    portBinding.fields[firstFreeField] _ field;
                    newFirstFreeField _ newFirstFreeField + 1;
                    newValueStart _ newValueStart + field.currentValue.size;
                    FOR f: NAT IN [0..roseWire.connections.size) DO
                        IF roseWire.connections[f]=NIL THEN {
                            roseWire.connections[f] _ field;
                            EXIT;
                            };
                        REPEAT
                            FINISHED => ERROR;
                        ENDLOOP;
                    IF NOT RefTab.Insert[x: bound, key: wire, val: $Bound] THEN ERROR;
                    };
                };
            };

        CountVicinity: PROC [wire: RoseWire, currentCount: NAT _ 0] RETURNS [newCount: NAT] = {
            channels: RoseTransistors _ wire.channels;
            wire.mark _ TRUE;
            newCount _ currentCount + 1;
            IF channels#NIL THEN FOR t: CARDINAL IN [0..channels.size) DO
                tran: RoseTransistor _ channels[t];
                otherWire: RoseWire _ tran.ch1;
                IF otherWire=wire THEN otherWire _ tran.ch2;
                IF otherWire.wireDrive#infinite AND NOT otherWire.mark THEN newCount _ CountVicinity[otherWire, newCount];
                ENDLOOP;
            };

        LookUpRoseWire: PROC [wire: Core.Wire] RETURNS [roseWire: RoseWire _ NIL] = {
            bind: WireBind _ NARROW[RefTab.Fetch[x: wireBindTab, key: wire].val];
            path: PackedPath;
            IF bind=NIL THEN path _ packedPath
            ELSE {
                path _ bind.path;
                wire _ bind.wire;
                };
        FOR roseWire: RoseWire _ simulation.coreToRoseWires[PathHash[path, wire]], roseWire.nextBucket UNTIL roseWire=NIL DO
        IF PathEqual[roseWire.path, path] AND roseWire.wire=wire THEN RETURN[roseWire];
        ENDLOOP;
            };

        WireData: TYPE = REF WireDataRec;
        WireDataRec: TYPE = RECORD [
            path: PackedPath,
            indegree: CARDINAL _ 0,
            connections: CARDINAL _ 0,
            channels: CARDINAL _ 0,
            gates: CARDINAL _ 0,
            portLeaf: BOOL _ FALSE,
            boolPort: BOOL _ FALSE,
            allocated: BOOL _ FALSE];
                <<>>
        gate: NAT = 0;
        ch1: NAT = 1;
        ch2: NAT = 2;
        maxRoseWireSize: NAT _ 0;
        maxVicinity: NAT _ 0;
        packedPath: PackedPath _ [0, ALL[FALSE]];
        wireDataTab: RefTab.Ref _ RefTab.Create[];
        wireBindTab: RefTab.Ref _ RefTab.Create[];
        publicRCT: Core.CellType _ Recordify[cellType];
        simulation _ NEW[SimulationRec];
        simulation.coreCellType _ cellType;
        simulation.cutSet _ cutSet;
        FOR i: NAT IN [0..publicRCT.public.size) DO
            ComputeInDegree[publicRCT.public[i]];
            ENDLOOP;
        {
            visited: RefTab.Ref _ RefTab.Create[];
            FOR i: NAT IN [0..publicRCT.public.size) DO
                MarkPortLeavesCountConnections[publicRCT.public[i], publicRCT.public[i], TRUE, visited];
                ENDLOOP;
            };
        FindRoseWires[ct: publicRCT];
        wireDataTab _ NIL;
        simulation.publicBindings _ NEW[PortBindingSeq[Ports.PortLeaves[testPort]]];
        IF simulation.publicBindings.size#ComputeBindings[port: testPort, wire: publicRCT.public, binds: simulation.publicBindings, 
        firstFreeBinding: 0] THEN ERROR;
        AllocateRoseInstances[ct: publicRCT];
        simulation.scratchValue _ NEW[Ports.LevelSequenceRec[maxRoseWireSize]];
        simulation.scratchDrive _ NEW[DriveRec[maxRoseWireSize]];
        FOR hash: HashIndex IN HashIndex DO
            FOR roseWire: RoseWire _ simulation.coreToRoseWires[hash], roseWire.nextBucket UNTIL roseWire=NIL DO
                IF roseWire.wireDrive=infinite THEN UpdateReaders[simulation, roseWire, NIL]
                ELSE IF NOT roseWire.mark THEN maxVicinity _ MAX[maxVicinity, CountVicinity[roseWire]];
                ENDLOOP;
            ENDLOOP;
        FOR hash: HashIndex IN HashIndex DO
            FOR roseWire: RoseWire _ simulation.coreToRoseWires[hash], roseWire.nextBucket UNTIL roseWire=NIL DO
                roseWire.mark _ FALSE;
                ENDLOOP;
            ENDLOOP;
        FOR strength: Ports.Drive IN Ports.Drive DO
            simulation.vicinityByStrength[strength].wires _ NEW[RoseWireSeq[maxVicinity]];
            ENDLOOP;
        simulation.testPort _ testPort;
        AllocateStatePoints[simulation, statePoints];
        EstablishInvariants[simulation];
        };
            <<>>
    EstablishInvariants: PROC [simulation: Simulation] = {
        CleanUp[simulation: simulation, bindings: simulation.publicBindings, forceUpdate: TRUE, updateProc: NIL];
        FOR hash: HashIndex IN HashIndex DO
            FOR roseInstance: RoseCellInstance _ simulation.coreToRoseInstances[hash], roseInstance.nextBucket UNTIL roseInstance=NIL DO
                CleanUp[simulation: simulation, bindings: roseInstance.portBindings, forceUpdate: TRUE, updateProc: NIL];
                ENDLOOP;
            ENDLOOP;
        FOR hash: HashIndex IN HashIndex DO
            FOR roseWire: RoseWire _ simulation.coreToRoseWires[hash], roseWire.nextBucket UNTIL roseWire=NIL DO
                IF roseWire.connections#NIL THEN RecomputeValue[simulation: simulation, wire: roseWire, forceReaderUpdate: TRUE, updateProc: NIL];
                ENDLOOP;
            ENDLOOP;
        };

    FindRoseCellType: PROC [cellType: Core.CellType] RETURNS [roseCellType: RoseCellType] = {
        roseClassName: ROPE _ NARROW[CoreProperties.GetCellTypeProp[from: cellType, prop: roseBehaveProp]];
        found: BOOL;
        val: REF ANY;
        IF roseClassName=NIL THEN roseClassName _ NARROW[CoreProperties.GetCellClassProp[from: cellType.class, prop: roseBehaveProp]];
        [found, val] _ SymTab.Fetch[roseClassTable, roseClassName];
        roseCellType _ NARROW[val];
        };

    Recordify: PUBLIC PROC [ct: Core.CellType] RETURNS [rc: Core.CellType] = {
        FOR rc _ ct, CoreOps.Recast[rc] UNTIL rc.class.recast = NIL DO 
            <<rct.class.recast = NIL exactly when rct is a record or atomic.>>
            NULL;
            ENDLOOP;
        };

    AllocateLevelSequence: PROC [count: NAT] RETURNS [ls: Ports.LevelSequence] = {
        ls _ NEW[Ports.LevelSequenceRec[count]];
        FOR bit: NAT IN [0..count) DO 
            ls[bit] _ L;
            ENDLOOP;
        };

    Initialize: PUBLIC PROC [simulation: Simulation, steady: BOOL _ TRUE] = {
        ERROR;  -- not implemented
        };

<<Relaxation>>
    Settle: PUBLIC PROC [simulation: Simulation, updateProc: UpdateProc _ NIL] = {
        CleanUp[simulation: simulation, bindings: simulation.publicBindings, updateProc: updateProc];
        UNTIL simulation.instanceNeedEval=NIL AND simulation.perturbed=NIL DO
            UNTIL simulation.instanceNeedEval=NIL DO
                instance: RoseCellInstance _ simulation.instanceNeedEval;
                simulation.instanceNeedEval _ instance.nextNeedEval;
                instance.nextNeedEval _ NIL;
                instance.roseCellType.evalSimple[p: instance.publicPort, stateAny: instance.state];
                CleanUp[simulation: simulation, bindings: instance.portBindings, updateProc: updateProc];
                Process.CheckForAbort[];
                ENDLOOP;
            UpdatePerturbed[simulation: simulation, updateProc: updateProc];
            ENDLOOP;
        FOR roseWires: LIST OF RoseWire _ simulation.roseBoolWires, roseWires.rest UNTIL roseWires=NIL DO
            roseWire: RoseWire _ roseWires.first;
            IF roseWire.currentValue=NIL THEN {
                IF roseWire.wireLevel=X THEN ERROR;
                }
            ELSE FOR bit: CARDINAL IN [0..roseWire.currentValue.size) DO
                IF roseWire.currentValue[bit]=X THEN ERROR;
                ENDLOOP;
            ENDLOOP;
    };

    CleanUp: PROC [simulation: Simulation, bindings: PortBindings, forceUpdate: BOOL _ FALSE, updateProc: UpdateProc] = {
        FOR binds: CARDINAL IN [0..bindings.size) DO
            bind: PortBinding _ bindings[binds];
            client: Ports.Port _ bind.clientPort;
            changeDrive: BOOL _ bind.currentDrive#client.d;
            IF changeDrive THEN bind.currentDrive _ client.d;
            SELECT client.type FROM
                l, b  => {
                    field: Field _ bind.fields[0];
                    changeValue: BOOL _ FALSE;
                    clientLevel: Ports.Level _ IF client.type=l THEN client.l ELSE IF client.b THEN H ELSE L;
                    IF field.currentValue[0]#clientLevel THEN {
                        changeValue _ TRUE;
                        field.currentValue[0] _ clientLevel;
                        };
                    UpdateReader[simulation, field];
                    IF changeDrive OR changeValue OR forceUpdate THEN RecomputeValue[simulation, field.roseWire, forceUpdate, updateProc];
                    };
                ls, bs, c, lc => {
                    FOR fields: CARDINAL IN [0..bind.fields.size) DO
                        field: Field _ bind.fields[fields];
                        fieldValue: Ports.LevelSequence _ field.currentValue;
                        changeValue: BOOL _ FALSE;
                        fieldStart: NAT _ field.portStartBit+client.fieldStart;
                        FOR bit: NAT IN [0..fieldValue.size) DO
                            thisBit: NAT _ bit+fieldStart;
                            clientLevel: Ports.Level _ SELECT client.type FROM
                                ls => client.ls[thisBit],
                                bs => IF client.bs[thisBit] THEN H ELSE L,
                                c => IF LOOPHOLE[client.c, WordAsBits][thisBit] THEN H ELSE L,
                                lc => IF (IF thisBit < 16 THEN LOOPHOLE[Basics.HighHalf[client.lc], WordAsBits][thisBit] ELSE LOOPHOLE[Basics.LowHalf[client.lc], 
                                WordAsBits][thisBit - 16]) THEN H ELSE L,
                                ENDCASE => ERROR;
                            IF fieldValue[bit]#clientLevel THEN {
                                changeValue _ TRUE;
                                fieldValue[bit] _ clientLevel;
                                };
                            ENDLOOP;
                        UpdateReader[simulation, field];
                        IF changeDrive OR changeValue OR forceUpdate THEN RecomputeValue[simulation, field.roseWire, forceUpdate, updateProc];
                        ENDLOOP;
                    };
                ENDCASE => ERROR;
            ENDLOOP;
    };

    RecomputeValue: PROC [simulation: Simulation, wire: RoseWire, forceReaderUpdate: BOOL, updateProc: UpdateProc] = {
        wireValue: Ports.LevelSequence _ wire.currentValue;
        IF wireValue=NIL THEN {
            scratchLevel: Ports.Level _ wire.wireLevel;
            scratchDrive: Ports.Drive _ wire.wireDrive;
            FOR writers: CARDINAL IN [0..wire.connections.size) DO
                writer: Field _ wire.connections[writers];
                writerLevel: Ports.Level _ writer.currentValue[0];
                writerDrive: Ports.Drive _ writer.portBinding.currentDrive;
                IF writerDrive > scratchDrive THEN {
                    scratchLevel _ writerLevel;
                    scratchDrive _ writerDrive;
                    }
                ELSE IF writerDrive = scratchDrive AND scratchLevel # writerLevel AND writerDrive > none THEN scratchLevel _ X;
                ENDLOOP;
            IF scratchLevel#wire.connectionLevel OR scratchDrive#wire.connectionDrive OR forceReaderUpdate THEN {
                wire.connectionLevel _ scratchLevel;
                wire.connectionDrive _ scratchDrive;
                Perturb[simulation, wire];
                };
            }
        ELSE {
            scratchValue: Ports.LevelSequence _ simulation.scratchValue;
            scratchDrive: DriveSequence _ simulation.scratchDrive;
            changeWire: BOOL _ FALSE;
            FOR bit: NAT IN [0..wireValue.size) DO
                scratchValue[bit] _ wireValue[bit];
                scratchDrive[bit] _ none;
                ENDLOOP;
            FOR writers: CARDINAL IN [0..wire.connections.size) DO
                writer: Field _ wire.connections[writers];
                writerValue: Ports.LevelSequence _ writer.currentValue;
                writerDrive: Ports.Drive _ writer.portBinding.currentDrive;
                FOR bit: NAT IN [0..writerValue.size) DO
                    sd: Ports.Drive _ scratchDrive[bit];
                    IF writerDrive > sd THEN {
                        scratchValue[bit] _ writerValue[bit];
                        scratchDrive[bit] _ writerDrive;
                        }
                    ELSE IF writerDrive = sd AND scratchValue[bit] # writerValue[bit] AND writerDrive > none THEN scratchValue[bit] _ X;
                    ENDLOOP;
                ENDLOOP;
            FOR bit: NAT IN [0..wireValue.size) DO
                IF wireValue[bit] # scratchValue[bit] THEN {
                    wireValue[bit] _ scratchValue[bit];
                    changeWire _ TRUE;
                    };
                ENDLOOP;
            IF changeWire OR forceReaderUpdate THEN UpdateReaders[simulation, wire, updateProc];
            };
        };

    UpdateReaders: PROC [simulation: Simulation, wire: RoseWire, updateProc: UpdateProc] = {
        IF updateProc#NIL THEN updateProc[wire];
        IF wire.connections#NIL THEN FOR readers: CARDINAL IN [0..wire.connections.size) DO
            reader: Field _ wire.connections[readers];
            instance: RoseCellInstance _ reader.portBinding.instance;
            IF instance#NIL THEN IF instance.nextNeedEval=NIL THEN {
                instance.nextNeedEval _ simulation.instanceNeedEval;
                simulation.instanceNeedEval _ instance;
                };
            UpdateReader[simulation, reader];
            ENDLOOP;
        };

    UpdateReader: PROC [simulation: Simulation, reader: Field] = {
        wire: RoseWire _ reader.roseWire;
        wireValue: Ports.LevelSequence _ wire.currentValue;
        readerValue: Ports.Port _ reader.portBinding.clientPort;
        readerStart: NAT _ reader.portStartBit+readerValue.fieldStart;
        SELECT readerValue.type FROM
            l  => readerValue.l _ wire.wireLevel;
            b  => readerValue.b _ SELECT wire.wireLevel FROM
                L => FALSE,
                X => readerValue.b,
                H => TRUE,
                ENDCASE => ERROR;
            ls => FOR bit: NAT IN [0..wireValue.size) DO
                readerValue.ls[bit+readerStart] _ wireValue[bit];
                ENDLOOP;
            bs => FOR bit: NAT IN [0..wireValue.size) DO
                readerValue.bs[bit+readerStart] _ SELECT wireValue[bit] FROM
                    L => FALSE,
                    X => readerValue.bs[bit+readerStart],
                    H => TRUE,
                    ENDCASE => ERROR;
                ENDLOOP;
            c => {
                asBits: WordAsBits _ ALL[FALSE];
                FOR bit: NAT IN [0..wireValue.size) DO
                    asBits[bit+readerStart] _ SELECT wireValue[bit] FROM
                        L => FALSE,
                        X => LOOPHOLE[readerValue.c, WordAsBits][bit+readerStart],
                        H => TRUE,
                        ENDCASE => ERROR;
                    ENDLOOP;
                readerValue.c _ LOOPHOLE[asBits];
                };
            lc => {
                asBits: DWordAsBits _ ALL[FALSE];
                FOR bit: NAT IN [0..wireValue.size) DO
                    thisBit: NAT _ bit+readerStart;
                    asBits[thisBit] _ SELECT wireValue[bit] FROM
                        L => FALSE,
                        X => IF thisBit < 16 THEN LOOPHOLE[Basics.HighHalf[readerValue.lc], WordAsBits][thisBit] ELSE 
                        LOOPHOLE[Basics.LowHalf[readerValue.lc], WordAsBits][thisBit - 16],
                        H => TRUE,
                        ENDCASE => ERROR;
                    ENDLOOP;
                readerValue.lc _ LOOPHOLE[Basics.SwapHalves[LOOPHOLE[asBits]]];
                };
            ENDCASE => ERROR;
        };

    UpdatePerturbed: PROC [simulation: Simulation, updateProc: UpdateProc]  = {

        Conductance: TYPE = {on, off, unknown};

        TranOn: PROC [tran: RoseTransistor] RETURNS [cond: Conductance] = {
            gateValue: Ports.Level _ tran.gate.wireLevel;
            cond _ SELECT tran.type FROM 
                nE => SELECT gateValue FROM
                    L => off,
                    H => on,
                    X => unknown,
                    ENDCASE => ERROR,
                pE => SELECT gateValue FROM
                    L => on,
                    H => off,
                    X => unknown,
                    ENDCASE => ERROR,
                nD => on,
                ENDCASE => ERROR;
            };

        PushWireByStrength: PROC [wire: RoseWire, thisDrive: Ports.Drive] = {
            simulation.vicinityByStrength[thisDrive].wires[ simulation.vicinityByStrength[thisDrive].firstFree] _ wire;
            simulation.vicinityByStrength[thisDrive].firstFree _ simulation.vicinityByStrength[thisDrive].firstFree+1;
            };

        PushWhat: TYPE = {switch, up, down};

        FindVicinity: PROC [wire: RoseWire, what: PushWhat] = {

            UpDownStrength: PROC [notLevel: Ports.Level] RETURNS [strength: Ports.Drive] = {
                level: Ports.Level;
                IF wire.wireDrive>wire.connectionDrive THEN {
                    level _ wire.wireLevel;
                    strength _ wire.wireDrive;
                    }
                ELSE {
                    level _ wire.connectionLevel;
                    strength _ wire.connectionDrive;
                    };
                IF level=notLevel THEN strength _ none;
                };

            wireDrive: Ports.Drive _ SELECT what FROM
                switch => IF wire.wireDrive>wire.connectionDrive THEN wire.wireDrive ELSE wire.connectionDrive,
                up => UpDownStrength[L],
                down => UpDownStrength[H],
                ENDCASE => ERROR;
            channels: RoseTransistors _ wire.channels;
            wire.mark _ TRUE;
            IF channels#NIL THEN FOR t: CARDINAL IN [0..channels.size) DO
                tran: RoseTransistor _ channels[t];
                tranCond: Conductance _ TranOn[tran];
                otherWire: RoseWire _ tran.ch1;
                IF otherWire=wire THEN otherWire _ tran.ch2;
                IF tranCond=off THEN LOOP;
                IF otherWire.wireDrive=infinite THEN {
                    IF ((what=switch AND tranCond=on) OR (what=up AND otherWire.wireLevel#L) OR (what=down AND otherWire.wireLevel#H)) AND wireDrive < 
                    tran.conductivity THEN wireDrive _ tran.conductivity;
                    }
                ELSE IF NOT otherWire.mark THEN FindVicinity[otherWire, what];
                ENDLOOP;
            IF what#switch AND wireDrive < wire.switchDrive THEN wireDrive _ none;
            PushWireByStrength[wire, wireDrive];
            SELECT what FROM
                switch => {
                    next: RoseWire _ wire.nextPerturbedWire;
                    previous: RoseWire _ wire.previousPerturbedWire;
                    IF next#NIL THEN next.previousPerturbedWire _ previous;
                    IF previous#NIL THEN previous.nextPerturbedWire _ next;
                    IF simulation.perturbed=wire THEN simulation.perturbed _ next;
                    wire.nextPerturbedWire _ NIL;
                    wire.previousPerturbedWire _ NIL;
                    wire.nextRecomputed _ recomputed;
                    recomputed _ wire;
                    wire.switchDrive _ wireDrive;
                    };
                up => wire.upDrive _ wireDrive;
                down => wire.downDrive _ wireDrive;
                ENDCASE => ERROR;
            };

        PushStrength: PROC [what: PushWhat] = {
            FOR thisDrive: Ports.Drive DECREASING IN [none..infinite) DO
                firstFreeWire: CARDINAL;
                UNTIL (firstFreeWire _ simulation.vicinityByStrength[thisDrive].firstFree)=0 DO
                    wire: RoseWire _ simulation.vicinityByStrength[thisDrive].wires[ firstFreeWire-1];
                    channels: RoseTransistors _ wire.channels;
                    wire.mark _ FALSE;
                    simulation.vicinityByStrength[thisDrive].firstFree _ firstFreeWire-1;
                    IF thisDrive=none OR thisDrive < (SELECT what FROM
                        switch => wire.switchDrive,
                        up => wire.upDrive,
                        down => wire.downDrive,
                        ENDCASE => ERROR) THEN LOOP;
                    IF channels#NIL THEN FOR t: CARDINAL IN [0..channels.size) DO
                        tran: RoseTransistor _ channels[t];
                        tranCond: Conductance _ TranOn[tran];
                        driveThrough: Ports.Drive _ MIN[thisDrive, tran.conductivity];
                        otherWire: RoseWire _ tran.ch1;
                        IF otherWire=wire THEN otherWire _ tran.ch2;
                        SELECT what FROM
                            switch => IF tranCond=on AND driveThrough > otherWire.switchDrive THEN {
                                otherWire.switchDrive _ driveThrough;
                                PushWireByStrength[otherWire, driveThrough];
                                };
                            up => IF tranCond#off AND driveThrough >= otherWire.switchDrive AND driveThrough > otherWire.upDrive THEN {
                                otherWire.upDrive _ driveThrough;
                                PushWireByStrength[otherWire, driveThrough];
                                };
                            down => IF tranCond#off AND driveThrough >= otherWire.switchDrive AND driveThrough > otherWire.downDrive THEN {
                                otherWire.downDrive _ driveThrough;
                                PushWireByStrength[otherWire, driveThrough];
                                };
                            ENDCASE => ERROR;
                        ENDLOOP;
                    ENDLOOP;
                ENDLOOP;
            };

        recomputed: RoseWire _ NIL;
        UNTIL simulation.perturbed=NIL DO
            wire: RoseWire _ simulation.perturbed;
            FindVicinity[wire, switch];
            PushStrength[switch];
            FindVicinity[wire, up];
            PushStrength[up];
            FindVicinity[wire, down];
            PushStrength[down];
            ENDLOOP;
        FOR recomputed _ recomputed, recomputed.nextRecomputed UNTIL recomputed=NIL DO
            wireLevel: Ports.Level _ SELECT TRUE FROM
                recomputed.upDrive=none => L,
                recomputed.downDrive=none => H,
                ENDCASE => X;
            IF recomputed.wireLevel#wireLevel THEN {
                gates: RoseTransistors _ recomputed.gates;
                IF gates#NIL THEN FOR t: CARDINAL IN [0..gates.size) DO
                    tran: RoseTransistor _ gates[t];
                    Perturb[simulation, tran.ch1];
                    Perturb[simulation, tran.ch2];
                    ENDLOOP;
                recomputed.wireLevel _ wireLevel;
                UpdateReaders[simulation, recomputed, updateProc];
                };
            ENDLOOP;
        };

    Perturb: PROC [simulation: Simulation, wire: RoseWire] = {
        IF wire.nextPerturbedWire=NIL AND wire.previousPerturbedWire=NIL AND simulation.perturbed#wire AND wire.wireDrive<infinite THEN {
            currentHead: RoseWire _ simulation.perturbed;
            wire.nextPerturbedWire _ currentHead;
            IF currentHead#NIL THEN currentHead.previousPerturbedWire _ wire;
            simulation.perturbed _ wire;
            };
        };

<<State Access>>
    GetCellTypeState: PUBLIC PROC [simulation: Simulation] RETURNS [stateAny: REF ANY] = {
        stateAny _ simulation.coreToRoseInstances[0].state;
        };
        <<>>
    GetInstanceState: PUBLIC PROC [simulation: Simulation, instantiationPath: InstantiationPath, instance: CoreClasses.CellInstance] 
    RETURNS [stateAny: REF ANY _ NIL] = {
        packedPath: PackedPath _ ComputePackedPath[simulation, instantiationPath];
    hash: HashIndex _ PathHash[packedPath, instance];
    FOR roseInstance: RoseCellInstance _ simulation.coreToRoseInstances[hash], roseInstance.nextBucket UNTIL roseInstance=NIL DO
    IF PathEqual[roseInstance.path, packedPath] AND roseInstance.instance=instance THEN RETURN[roseInstance.state];
    ENDLOOP;
        };
        <<>>
    GetWireValue: PUBLIC PROC [simulation: Simulation, instantiationPath: InstantiationPath, wire: Core.Wire, container: 
    Ports.LevelSequence] = {
        packedPath: PackedPath _ ComputePackedPath[simulation, instantiationPath];
        binds: ValueBindings _ NIL;
        firstFreeBit: NAT _ 0;
        FOR binds _ simulation.coreToValues, binds.rest UNTIL binds=NIL DO
            IF PathEqual[packedPath, binds.first.path] AND wire=binds.first.wire THEN EXIT;
            REPEAT
                FINISHED => {

                    BindPublicToActual: CoreOps.EachWirePairProc = {
                        bind: WireBind _ NARROW[RefTab.Fetch[x: wireBindTab, key: actualWire].val];
                        IF bind=NIL THEN bind _ NEW[WireBindRec _ [
                            path: currentPath,
                            wire: actualWire]];
                        [] _ RefTab.Store[x: wireBindTab, key: publicWire, val: bind];
                        };

                    FindHereOrBelow: PROC [path: PackedPath, wire: Core.Wire] = {
                        bind: WireBind _ NARROW[RefTab.Fetch[x: wireBindTab, key: wire].val];
                        IF bind#NIL THEN {
                            path _ bind.path;
                            wire _ bind.wire;
                            };
                        FOR roseWire: RoseWire _ simulation.coreToRoseWires[PathHash[path, wire]], roseWire.nextBucket UNTIL roseWire=NIL DO
                            IF PathEqual[roseWire.path, path] AND roseWire.wire=wire THEN {
                                values _ CONS[[
                                    roseWire: roseWire,
                                    size: IF roseWire.currentValue=NIL THEN 1 ELSE roseWire.currentValue.size], values];
                                EXIT;
                                };
                            REPEAT
                                FINISHED => {
                                    FOR subWire: NAT IN [0..wire.size) DO
                                        FindHereOrBelow[path, wire[subWire]];
                                        ENDLOOP;
                                    };
                            ENDLOOP;
                        };

                    FindAbove: PROC [internal: Core.Wire] RETURNS [foundCore: BOOL _ FALSE, foundRose: BOOL _ FALSE, firstBit: NAT _ 0] = {
                        IF internal=wire THEN foundCore _ TRUE
                        ELSE FOR thisWire: NAT IN [0..internal.size) DO
                            [foundCore, foundRose, firstBit] _ FindAbove[internal[thisWire]];
                            IF foundCore AND NOT foundRose THEN {
                                path: PackedPath _ packedPath;
                                bind: WireBind _ NARROW[RefTab.Fetch[x: wireBindTab, key: internal].val];
                                IF bind#NIL THEN {
                                    path _ bind.path;
                                    internal _ bind.wire;
                                    };
                                FOR subWire: NAT IN [0..thisWire) DO
                                    firstBit _ firstBit + CoreOps.WireBits[internal[subWire]]
                                    ENDLOOP;
                                FOR roseWire: RoseWire _ simulation.coreToRoseWires[PathHash[path, internal]], roseWire.nextBucket UNTIL roseWire=NIL DO
                                    IF PathEqual[roseWire.path, path] AND roseWire.wire=internal THEN {
                                        values _ CONS[[
                                            roseWire: roseWire,
                                            firstBit: firstBit,
                                            size: CoreOps.WireBits[wire]], values];
                                        foundRose _ TRUE;
                                        EXIT;
                                        };
                                    ENDLOOP;
                                EXIT;
                                };
                            ENDLOOP;
                        };

                    values: Values _ NIL;
                    wireBindTab: RefTab.Ref _ RefTab.Create[]; 
                    currentPath: PackedPath _ [0, ALL[FALSE]];
                    coreInstance: CoreClasses.CellInstance;
                    ct: Core.CellType _ simulation.coreCellType;
                    rc: Core.CellType _ Recordify[ct];
                    rct: CoreClasses.RecordCellType _ NARROW[rc.data];
                    UNTIL currentPath.length=packedPath.length DO
                        boolWord: PACKED ARRAY [0..16) OF BOOL _ ALL[FALSE];
                        pathBits: NAT _ BitHacks.NBits[rct.size];
                        FOR bit: NAT IN [0..pathBits) DO
                            thisBit: BOOL _ packedPath.bits[currentPath.length+bit];
                            boolWord[16-pathBits+bit] _ thisBit;
                            currentPath.bits[currentPath.length+bit] _ thisBit;
                            ENDLOOP;
                        coreInstance _ rct[LOOPHOLE[boolWord]];
                        IF CutSetMember[currentPath, coreInstance, simulation.cutSet].member THEN ERROR;
                        ct _ coreInstance.type;
                        rc _ Recordify[ct];
                        rct _ NARROW[rc.data];
                        IF CoreOps.VisitBinding[actual: coreInstance.actual, public: rc.public, eachWirePair: BindPublicToActual] THEN ERROR;
                        currentPath.length _ currentPath.length+pathBits;
                        ENDLOOP;
                    FindHereOrBelow[packedPath, wire];
                    IF values=NIL THEN IF NOT FindAbove[rct.internal].foundRose THEN ERROR;
                    binds _ simulation.coreToValues _ CONS[[
                        path: packedPath,
                        wire: wire,
                        values: values], simulation.coreToValues];
                    };
            ENDLOOP;
        FOR values: Values _ binds.first.values, values.rest UNTIL values=NIL DO
            currentValue: Ports.LevelSequence _ values.first.roseWire.currentValue;
            IF currentValue=NIL THEN {
                container[firstFreeBit] _ values.first.roseWire.wireLevel;
                firstFreeBit _ firstFreeBit + 1;
                }
            ELSE {
                firstBit: NAT _ values.first.firstBit;
                FOR bit: NAT IN [0..values.first.size) DO
                    container[firstFreeBit + bit] _ currentValue[firstBit+bit];
                    ENDLOOP;
                firstFreeBit _ firstFreeBit + values.first.size;
                };
            ENDLOOP;
        };

    ComputePackedPath: PROC [simulation: Simulation, instantiationPath: InstantiationPath] RETURNS [packedPath: PackedPath] = {
        ct: Core.CellType _ simulation.coreCellType;
        packedPath.length _ 0;
        FOR path: InstantiationPath _ instantiationPath, path.rest UNTIL path=NIL DO
            rc: Core.CellType _ Recordify[ct];
            rct: CoreClasses.RecordCellType _ NARROW[rc.data];
            FOR in: NAT IN [0..rct.size) DO
                IF rct[in]=path.first THEN {
                    pathBits: NAT _ BitHacks.NBits[rct.size];
                    FOR bit: NAT IN [0..pathBits) DO
                        packedPath.bits[packedPath.length+bit] _ BitHacks.XthBitOfN[pathBits-bit-1, in];
                        ENDLOOP;
                    packedPath.length _ packedPath.length + pathBits;
                    ct _ rct[in].type;
                    EXIT;
                    };
                REPEAT
                    FINISHED => ERROR;
                ENDLOOP;
            ENDLOOP;
        };

    GetCellType: PUBLIC PROC [rootCellType: Core.CellType, path: PackedPath] RETURNS [cellType: Core.CellType _ NIL] = {
        startBit: NAT _ 0;
        cellType _ Recordify[rootCellType];
        UNTIL startBit=path.length DO
            rct: CoreClasses.RecordCellType _ NARROW[cellType.data];
            pathBits: NAT _ BitHacks.NBits[rct.size];
            instanceBits: PACKED ARRAY [0..16) OF BOOL _ ALL[FALSE];
            FOR bit: NAT IN [0..pathBits) DO
                instanceBits[16-pathBits+bit] _ path.bits[startBit+bit];
                ENDLOOP;
            startBit _ startBit+pathBits;
            cellType _ Recordify[rct[LOOPHOLE[instanceBits]].type];
            ENDLOOP;
        };

    PathEqual: PROC [one: PackedPath, other: PackedPath] RETURNS [equal: BOOL] = {
        equal _ one.length=other.length;
        IF equal THEN FOR bit: NAT IN [0..one.length) DO
            IF one.bits[bit]#other.bits[bit] THEN {
                equal _ FALSE;
                EXIT;
                };
            ENDLOOP;
        };

    PathHash: PROC [path: PackedPath, ref: REF ANY] RETURNS [hi: HashIndex] = TRUSTED {
        pathAsLN: Basics.LongNumber _ Basics.SwapHalves[LOOPHOLE[path.bits]];
    wideHI: CARDINAL;
        pathAsLN _ Basics.DoubleShiftRight[pathAsLN, 32-path.length];
    wideHI _ Basics.BITXOR[pathAsLN.lowbits, pathAsLN.highbits];
    wideHI _ Basics.BITXOR[wideHI, Basics.LowHalf[LOOPHOLE[ref]]];
    wideHI _ Basics.BITXOR[wideHI, Basics.HighHalf[LOOPHOLE[ref]]];
    hi _ Basics.BITAND[wideHI, hashMask];
        };
        hashMask: NAT _ BitHacks.TwoToThe[BitHacks.NBits[LAST[HashIndex] + 1]] - 1;

    CutSetMember: PROC [packedPath: PackedPath, instance: CoreClasses.CellInstance, cutSet: ROPE] RETURNS [member: BOOL _ FALSE, 
    transistor: BOOL _ FALSE, ct: Core.CellType] = {

        FixStupidRef: PROC [ref: REF ANY] RETURNS [rope: ROPE] = {
            rope _ WITH ref SELECT FROM
                r: REF TEXT => Rope.FromRefText[r],
                r: ROPE => r,
                ENDCASE => ERROR;
            };

        cutSets: LIST OF ROPE _ NARROW[CoreProperties.GetCellInstanceProp[from: instance, prop: roseCutSetProp]];
        ct _ instance.type;
        FOR csl: LIST OF ROPE _ cutSets, csl.rest UNTIL csl=NIL DO
            IF Rope.Equal[FixStupidRef[csl.first], cutSet] THEN {
                member _ TRUE;
                RETURN;
                };
            ENDLOOP;
        DO
            IF ct.class.recast=NIL AND FindRoseCellType[ct]#NIL AND ct.class#CoreClasses.recordCellClass THEN {
                member _ TRUE;
                RETURN;
                };
            IF ct.class=CoreClasses.transistorCellClass THEN {
                member _ TRUE;
                transistor _ TRUE;
                RETURN;
                };
            cutSets _ NARROW[CoreProperties.GetCellTypeProp[from: ct, prop: roseCutSetProp]];
            FOR csl: LIST OF ROPE _ cutSets, csl.rest UNTIL csl=NIL DO
                IF Rope.Equal[FixStupidRef[csl.first], cutSet] THEN {
                    member _ TRUE;
                    RETURN;
                    };
                ENDLOOP;
            IF ct.class#CoreClasses.identityCellClass THEN EXIT;
            ct _ NARROW[ct.data];
            ENDLOOP;
        };

    AllocateStatePoints: PUBLIC PROC [simulation: Simulation, statePoints: NAT] = {

        AllocateLevelSequenceSeq: PROC [size: NAT] RETURNS [seq: LevelSequenceSeq] = {
            seq _ NEW[LevelSequenceSeqRec[statePoints]];
            FOR s: NAT IN [0..statePoints) DO
                seq[s] _ NEW[Ports.LevelSequenceRec[size]];
                ENDLOOP;
            };

        AllocatePortBindings: PROC [binds: PortBindings] = {
            FOR b: NAT IN [0..binds.size) DO
                bind: PortBinding _ binds[b];
                bind.statePoints _ NEW[DriveRec[statePoints]];
                FOR f: NAT IN [0..bind.fields.size) DO
                    field: Field _ bind.fields[f];
                    field.statePoints _ AllocateLevelSequenceSeq[field.currentValue.size];
                    ENDLOOP;
                ENDLOOP;
            };

        FOR hash: HashIndex IN HashIndex DO
            FOR roseInstance: RoseCellInstance _ simulation.coreToRoseInstances[hash], roseInstance.nextBucket UNTIL roseInstance=NIL DO
                IF roseInstance.state#NIL THEN {
                    roseInstance.statePoints _ NEW[SRASeq[statePoints]];
                    FOR s: NAT IN [0..statePoints) DO
                        roseInstance.statePoints[s] _ roseInstance.roseCellType.init[roseInstance.instance.type, roseInstance.publicPort];
                        ENDLOOP;
                    };
                AllocatePortBindings[roseInstance.portBindings];
                ENDLOOP;
            ENDLOOP;
        FOR hash: HashIndex IN HashIndex DO
            FOR roseWire: RoseWire _ simulation.coreToRoseWires[hash], roseWire.nextBucket UNTIL roseWire=NIL DO
                roseWire.statePoints _ IF roseWire.currentValue=NIL THEN NEW[Ports.LevelSequenceRec[statePoints]] ELSE 
                AllocateLevelSequenceSeq[roseWire.currentValue.size];
                ENDLOOP;
            ENDLOOP;
        simulation.statePoints _ NEW[PortSequenceRec[statePoints]];
        FOR sp: NAT IN [0..statePoints) DO
            simulation.statePoints[sp] _ Ports.CreatePort[simulation.coreCellType.public];
            ENDLOOP;
        AllocatePortBindings[simulation.publicBindings];
        };

    StatePoint: PUBLIC PROC [simulation: Simulation, point: NAT] = {

        SavePortBindings: PROC [binds: PortBindings] = {
            FOR b: NAT IN [0..binds.size) DO
                bind: PortBinding _ binds[b];
                bind.statePoints[point] _ bind.currentDrive;
                FOR f: NAT IN [0..bind.fields.size) DO
                    field: Field _ bind.fields[f];
                    source: Ports.LevelSequence _ field.currentValue;
                    dest: Ports.LevelSequence _ field.statePoints[point];
                    FOR bit: NAT IN [0..field.currentValue.size) DO
                        dest[bit] _ source[bit];
                        ENDLOOP;
                    ENDLOOP;
                ENDLOOP;
            };

        FOR hash: HashIndex IN HashIndex DO
            FOR roseInstance: RoseCellInstance _ simulation.coreToRoseInstances[hash], roseInstance.nextBucket UNTIL roseInstance=NIL DO
                IF roseInstance.state#NIL THEN roseInstance.roseCellType.copy[from: roseInstance.state, to: roseInstance.statePoints[point]];
                SavePortBindings[roseInstance.portBindings];
                ENDLOOP;
            ENDLOOP;
        FOR hash: HashIndex IN HashIndex DO
            FOR roseWire: RoseWire _ simulation.coreToRoseWires[hash], roseWire.nextBucket UNTIL roseWire=NIL DO
                IF roseWire.currentValue=NIL THEN {
                    ls: Ports.LevelSequence _ NARROW[roseWire.statePoints];
                    ls[point] _ roseWire.wireLevel;
                    }
                ELSE {
                    sp: LevelSequenceSeq _ NARROW[roseWire.statePoints];
                    ls: Ports.LevelSequence _ sp[point];
                    FOR bit: NAT IN [0..roseWire.currentValue.size) DO
                        ls[bit] _ roseWire.currentValue[bit];
                        ENDLOOP;
                    };
                ENDLOOP;
            ENDLOOP;
        Ports.CopyPortValue[from: simulation.testPort, to: simulation.statePoints[point]];
        SavePortBindings[simulation.publicBindings];
        };

    RestoreState: PUBLIC PROC [simulation: Simulation, point: NAT] = {

        RestorePortBindings: PROC [binds: PortBindings] = {
            FOR b: NAT IN [0..binds.size) DO
                bind: PortBinding _ binds[b];
                bind.currentDrive _ bind.statePoints[point];
                FOR f: NAT IN [0..bind.fields.size) DO
                    field: Field _ bind.fields[f];
                    dest: Ports.LevelSequence _ field.currentValue;
                    source: Ports.LevelSequence _ field.statePoints[point];
                    FOR bit: NAT IN [0..field.currentValue.size) DO
                        dest[bit] _ source[bit];
                        ENDLOOP;
                    ENDLOOP;
                ENDLOOP;
            };

        Complain: UpdateProc = {
            ERROR Stop["State restoration failed, notify Rosemary wizard"];
            };

        simulation.instanceNeedEval _ NIL;
        FOR hash: HashIndex IN HashIndex DO
            FOR roseInstance: RoseCellInstance _ simulation.coreToRoseInstances[hash], roseInstance.nextBucket UNTIL roseInstance=NIL DO
                IF roseInstance.state#NIL THEN roseInstance.roseCellType.copy[from: roseInstance.statePoints[point], to: roseInstance.state];
                RestorePortBindings[roseInstance.portBindings];
                roseInstance.nextNeedEval _ simulation.instanceNeedEval;
                simulation.instanceNeedEval _ roseInstance;
                ENDLOOP;
            ENDLOOP;
        simulation.perturbed _ NIL;
        FOR hash: HashIndex IN HashIndex DO
            FOR roseWire: RoseWire _ simulation.coreToRoseWires[hash], roseWire.nextBucket UNTIL roseWire=NIL DO
                IF roseWire.currentValue=NIL THEN {
                    ls: Ports.LevelSequence _ NARROW[roseWire.statePoints];
                    roseWire.wireLevel _ ls[point];
                    roseWire.nextPerturbedWire _ simulation.perturbed;
                    roseWire.previousPerturbedWire _ NIL;
                    IF simulation.perturbed#NIL THEN simulation.perturbed.previousPerturbedWire _ roseWire;
                    simulation.perturbed _ roseWire;
                    RecomputeValue[simulation, roseWire, FALSE, NIL];
                    }
                ELSE {
                    sp: LevelSequenceSeq _ NARROW[roseWire.statePoints];
                    ls: Ports.LevelSequence _ sp[point];
                    FOR bit: NAT IN [0..roseWire.currentValue.size) DO
                        roseWire.currentValue[bit] _ ls[bit];
                        ENDLOOP;
                    };
                UpdateReaders[simulation, roseWire, NIL];
                ENDLOOP;
            ENDLOOP;
        Ports.CopyPortValue[from: simulation.statePoints[point], to: simulation.testPort];
        RestorePortBindings[simulation.publicBindings];
        Settle[simulation, Complain];
        };

    END.