EDIS:
Guide |
FAQ |
New |
Search |
Bibliography |
Index |
Feedback

*Non-Receptive 1-Bit Variable*

### Informal

A *Non-Receptive 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 not prescribed.
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 *Non-Receptive 1-Bit Variable*
must guarantee mutual
exlusion of the signals on *w0* and *w1*.
In contrast to a 1-Bit Variable,
the environment must also guarantee mutual exclusion between the write
and read inputs.

Note that
a *Non-Receptive 1-Bit Variable* stores a proper initial value.
That is, before the first write operation, all read operations will return the
same value.
This initial value, however, is not prescribed.

Schematic diagram
for a *Non-Receptive 1-Bit Variable*:

[Zoom|FIG]

XDI state graph
for a *Non-Receptive 1-Bit Variable*:

[Zoom|FIG]

Specification in XDI model.

Specification in Verdect:

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

Also available through this link
This
verification report
compares the Verdect specification with the XDI specification.
Specification in DI Algebra:

NAME = (Non receptive one bit variable)
I = { w0, w1, r }
O = { v0, v1, a }
V = V0 ND V1
V0 = [w0? -> V0W, w1? -> V1W , r? -> V0R]
V1 = [w0? -> V0W, w1? -> V1W , r? -> V1R]
V0W = [a! -> V0, r? -> CHAOS, w1? -> CHAOS]
V1W = [a! -> V1, r? -> CHAOS, w0? -> CHAOS]
V0R = [v0! -> V0, w0? -> CHAOS, w1? -> CHAOS]
V1R = [v1! -> V1, w0? -> CHAOS, w1? -> CHAOS]
.

Also available through this link
This
verification report
compares the DI Algebra specification with the XDI specification.
XDI Report.
The subscripts 0 and 1 can be interchanged systematically.

A *Non-Receptive 1-Bit Variable* is not output deterministic,
since there is an output choice in state 1.
The output nondeterminism is static.

### DI Decompositions

*No information available*

### Using Boolean Gates

*No information available*

### Using Transistors

*No information available*

*No information available*

The state graph give in Example 3.23 of
[Berkel93c, p. 64] is
ambiguous (two initial states) and not minimal
(the upper left and middle bottom states are equivalent, as are the
middle top and bottom right states).
[Berkel93c, p. 64]

###### Last modified at Fri Nov 20 10:11:40 1998

Encyclopaedia of Delay-Insensitive Systems

Copyright © 1995-1998
Tom Verhoeff /
Tom.Verhoeff@acm.org