Rephrasing: Both the a and the c wire pair can be viewed as encoding a value by a One-Hot code. When the value is sent to the k-Latch via an a input, it stores (latches) this value until b is received. Reception of b reproduces the value via the corresponding c ouput.
Specification in Verdect:
define L( a0?, ..., a(k-1)?, b?, c0!, ..., c(k-1)! ) =
pref *[ (a0? || b?); c0!
| ...
| (a(k-1)? || b?); c(k-1)!
]
end
Also available through this link
The specification of the 3-Latch is as
follows: Specification in Verdect:
define L( a0?, a1?, a2?, b?, c0!, c1!, c2! ) =
pref *[ (a0? || b?); c0!
| (a1? || b?); c1!
| (a2? || b?); c2!
]
end
Also available through this link.
Specification in DI Algebra:
I = { a0?, .. , a(k-1)?, b? }
O = { c0?, .. , c(k-1)! }
L(k,k) = [ (,i: 0<=i < k: ai? -> L(i,k),
b? -> M(k,k)
]
L(i,k) = [ b? -> M(i,k), else -> CHAOS ], for 0<=i M(i,k), b? -> CHAOS]
M(i,k) = ci!;L(k,k)
Also available through this link
We provide the specification for the
3-Latch:
The roles of subscripts i can be permuted (on a_i and c_i simultaneously).
The k-Latch satisfies Rules Y' and Z^out, but not Z^inp (choice between a inputs).
No information available
No information available
The k-Latch is sometimes also referred to as Decision-Wait ([Lucassen94]) or kx1-Join.
