Towards a unifying CSP approach for hierarchical verification of asynchronous hardware
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