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

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

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

XDI Report.

## Implementations

### DI Decompositions

No information available

### Using Boolean Gates

No information available

### Using Transistors

No information available

## Generalizations

No information available

## Miscellaneous

No information available