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'.
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
Also available through this link
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]
.
Also available through this link
No information available
No information available
No information available
No information available