# bisimulation for sequential circuits

In case you didn’t know, I teach hardware to the first year. I’m trying to improve my assessment technology for the associated exercises. This post is about the program I wrote today that might help me do that.

I set many exercises which involve constructing sequential circuits. What’s a sequential circuit? It’s a “function” from i bits of input to o bits of output that can access and update s bits of internal state. That’s to say it’s a function from s+i bits to s+o bits of output for some s. I need to tell when they’re equal up to external observation, regardless of s.

We have 2^{s} states, x. Each determines an immediate behaviour, b(x):2^{i}→2^{o} and a continuation k(x):2^{i}→2^{s}. The behaviour is directly observable but the continuation is not. The continuation can be distinguished only by *its* behaviour.

My strategy is to analyse each circuit to identify the observational equivalence classes of *concrete* states, then try to put two such analyses into bisimulation. The first part of that amounts to finding the smallest set U of *abstract* states such that we have functions p:U→Pow(2^{s}) and f:2^{s}→U such that

- p(u) is nonempty for all u∈U
- x∈p(u) iff f(x)=u
- if x,y∈p(u) then b(x)=b(y); i.e., for each u∈U, u!(u):2
^{i}→2^{o}is well defined via u!(u,m) = b(x,m) for some x∈p(u) - if x,y∈p(u) then for all m∈2
^{i}, f(k(x,m))=f(k(y,m)); i.e., for each u∈I, u?(u):2^{i}→U is well defined via u?(u,m)=f(k(x,m)) for some x∈p(u)

In other words, find the coarsest equivalence such that in equivalent states, the circuit must, for all inputs, produce equal outputs and evolve to equivalent states.

For a given (s,b,k), suppose we have such a (U,p,f,u!,u?). And for some corresponding (i.e., same i, same o) (t,c,l) let us have (V,q,g,v!,v?). Our mission is to establish an isomorphism, ~, between U and V such that

- if u~v, then u!(u)=v!(v)
- if u~v, then for all m∈2
^{i}, u?(u,m)~v?(v,m)

The analysis works by starting with the hope that all states are equivalent and then disabusing ourselves of this notion. We dump all states into a singleton partition (U=1,p(*)=2^{s},f(m)=*), then refine by a bunch of observations. To refine a partition by an observation, replace each part by the partition you get by distinguishing its elements on the basis of the observation: you can tell them apart, so you need to separate them! Start refining by b, to separate the states which behave differently immediately. Then refine by f(k(-,m) for each m: i.e, if you ever map source states to distinguished target states, you must distinguish the source states. Iterate to a fixpoint: as there are finitely many states, partitions cannot refine forever. We have grown our partition only when forced to by observable differences, so we have the smallest possible number of parts.

Now we need to grow our bisimulation, from the empty set of pairs. Start by inverting u! and v!, so that each immediate behaviour maps to the set of states which exhibit it: these must be pointwise isomorphic, which gives you a search space of candidates for pairs u~v. For every guess you make, you have to check that u?(u,m)~v?(v,m) for all m, so you learn more about what ~ must be.

The circuits are observationally equivalent, I claim, iff there exists such a bisimulation.

Here is my attempt at a Haskell implementation.