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