ABSTRACT:

``In the future, we will see multi-million gate devices with greater than 80% provided by pre-packaged hardware and software IP, in the form of cores or system-level macros (SLMs).''
[The VSI Alliance FAQ]

I'll describe how program verification methods can be combined with the analysis of synthesised state machines to verify algorithmic and control aspects of system-on-a-chip components. Material from recent research will be illustrated with examples drawn from an undergraduate hardware/software verification course. I'll also give an overview of related externally funded research projects at Cambridge. The talk is intended for a general audience.

[ postscript | gzipped postscript ]