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

# 1-Bit Variable

## Specifications

### Informal

A 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 1-Bit Variable must guarantee mutual exlusion of the signals on w0 and w1. In contrast to a 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.

The delay-insensitive specification allows the scenario where an arbitrary number of successive writes succeed before a pending read. Often a fairness requirement is imposed: if a choice situation between read and write arises `infinitely often', then both reading and writing succeed `infinitely often'.

### XDI

Schematic diagram for a 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 = "1 bit variable with arbitration"
I = { w0, w1, r }
O = { v0, v1, a }

V  = V0 ND V1

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

Exercise: Decompose any of the arbiters into a 1-Bit Variable and non-arbitrating elements.