Towards a unifying CSP approach for hierarchical verification of asynchronous hardware

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