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

# Non-Receptive 1-Bit Variable

## Specifications

### 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.

### XDI

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.

### Verdect

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
```

This verification report compares the Verdect specification with the XDI specification.

### DI Algebra

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]
.
```

This verification report compares the DI Algebra specification with the XDI specification.

## Properties

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.

## Implementations

### DI Decompositions

No information available

### Using Boolean Gates

No information available

### Using Transistors

No information available

## Generalizations

No information available

## Miscellaneous

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).

## References

[Berkel93c, p. 64]