Initialized 1-Bit Variable

Specifications

Informal

An Initialized 1-Bit Variable has three input terminals (w0, w1, r) and three output terminals (a, v0, v1). It stores one bit. The initial value of the bit is 0. Writing is done via the terminals w0 (write 0), w1 (write 1), and a (acknowledge), on which input and output alternate. Reading is done via the terminals r (read), v0 (value 0), and v1 (value 1), on which input and output alternate as well.

The environment of a an Initialized 1-Bit Variable must guarantee mutual exlusion of the signals on w0 and w1. In contrast to an Initialized Non-Receptive 1-Bit Variable, the environment need not guarantee mutual exclusion between the write and read inputs. However, when reading the variable and changing its value through a write, the returned value is not prescribed.

XDI

Schematic diagram for an Initialized 1-Bit Variable:

[Zoom|FIG]

Specification in XDI model.

Verdect

Specification in Verdect:


define VAR( w0?, w1?, a!, r?, v0!, v1! ) =
    |[ x0, x1, y0, y1 ::
       pref *[ (w0?; x0 | w1?; x1); a! ]
    || pref *[ r?; (y0; v0! | y1; v1!) ]
    || pref (( *[y0] | *[y1] ); *[ x0; *[y0] | x1; *[y1] ])
    ]|
end

Also available through this link

DI Algebra

Specification in DI Algebra:


NAME = (Initialized 1 bit variable with arbitration)
I = { w0, w1, r }
O = { v0, v1, a }

V  = V0

V0 = [w0? -> a!; V0 , w1? -> a!; V1 , r? -> v0!; V0]
V1 = [w0? -> a!; V0 , w1? -> a!; V1 , r? -> v1!; V1]
.

Also available through this link

Properties

XDI Report.

Implementations

DI Decompositions

No information available

Using Boolean Gates

No information available

Using Transistors

No information available

Initialized 1-Bit Variable

Specifications

Informal

XDI

Verdect

DI Algebra

Properties

Implementations

DI Decompositions

Using Boolean Gates

Using Transistors

Generalizations

Miscellaneous

References

Last modified at Fri Nov 20 10:11:39 1998