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

# Initialized Non-Receptive 1-Bit Variable

## Specifications

### Informal

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

### XDI

Schematic diagram for an Initialized Non-Receptive 1-Bit Variable:

[Zoom|FIG]

XDI state graph for an Initialized 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] ; *[ x0; *[y0] | x1; *[y1] ])
]|
end
```

### DI Algebra

Specification in DI Algebra:

```
NAME = (Initialized Non-receptive one bit variable)
I = { w0, w1, r }
O = { v0, v1, a }

V  = V0

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

## Properties

XDI Report.

The subscripts 0 and 1 can be interchanged systematically, provided the initial state is then taken to be state 1.

An Initialized Non-Receptive 1-Bit Variable is output deterministic.

## Implementations

### DI Decompositions

1. An Initialized Non-Receptive 1-Bit Variable can be implemented by an Initialized 1-Bit Variable (not equ).
2. An Initialized Non-Receptive 1-Bit Variable can be implemented by state machine built around an mxn-Decision-Wait (m=3,n=2) (equ):

[Zoom|FIG]

### Using Boolean Gates

No information available

### Using Transistors

No information available

## Generalizations

No information available

## Miscellaneous

No information available