eighty-twenty

This talk was about using CSP within the Balsa toolkit to model asynchronous (clock-free) hardware. Asynchronous hardware replaces the clock with explicit synchronisation using handshakes/request + acknowledgement signals.

Clockless architectures are more efficient, cheaper in transistors, and they give more opportunity for verification. They’re harder to design and designs tend to be error-prone, though. This work is focussed on the idea that verification ought to be able to offset the difficulties of working with asynchronous systems.

At sub-micron technologies, the gates are so small the manufacturing process can be inaccurate enough to cause significant differences in timing delays within the chip! Hence per-chip clock-rate limits and testing… :-/

They’re compiling a CSPish language into silicon! Cool!

• syntax-directed compilation
• doesn’t pull extra parallelism out of the code
• so writing the parallelism in is very important
• which motivates the choice of CSP

CSPish language –> “handshake network” –> gate-level network –> …

Balsa has until now been a simulation-only tool, with no verification tool available. This work is building one.

• Each interface between handshake-network components has a more-or-less session type

• Different properties are verified at different levels - some at the whole-program balsa/csp level, some at the handshake-net level, and some at the gate network level

• the top levels are synchronous models (ie. output has a continuation); lower levels are async however! so new approach used to verify async variants of csp: “protocol-based closed-circuit testing” – reminds me of behavioural type system zipper checkers! (you supply the environment and make sure it goes to zero…)

• the case study reproduced a deadlock seen in the balsa simulator, and showed positively that the fix for the problem genuinely did remove the possibility of deadlock.

• protocol at gate level is a subset of the traces of the gate net — because they have to cope with async sends at that level (?)

• standard csp semantics, standard csp model-checkers. that is the contribution - no special tools required cf. Dill and cf. Josephs