A monadic approach to automated reasoning for Bluespec SystemVerilog

Add to your list(s) Download to your calendar using vCal

• Dominic Richards, The University of Manchester
• Wednesday 20 July 2011, 11:00-12:00
• Lecture Theatre 2, Computer Laboratory, William Gates Building.

If you have a question about this talk, please contact Jonathan Anderson.

A non-trivial subset of Bluespec SystemVerilog (BSV) is embedded in the higher order logic of the PVS theorem prover. Owing to the clean semantics of BSV , application of monadic techniques leads to a surprisingly elegant embedding, in which hardware designs are translated into logic almost verbatim, preserving types and language constructs. The resulting specifications are compatible with the built-in model checker of PVS , which can automatically prove an important class of temporal logic theorems, and can also be used in conjunction with the powerful proof strategies of PVS , including automatic predicate abstraction, to verify a broader class of properties than can be achieved with model checking alone. Furthermore, the above BSV subset is also embedded in the specification language of the SAL model checker, which provides a diverse array of fully-automated verification techniques.

Bluespec SystemVerilog is a hardware description language based on the guarded action model of concurrency. It has an elegant semantics, which has previously been shown to support design verification by hand proof: to date, however, little work has been conducted on the application of automated reasoning to BSV designs.

This talk is part of the CTSRD - CRASH-worthy Trusted Systems R&D series.

This talk is included in these lists:

• CTSRD - CRASH-worthy Trusted Systems R&D
• Lecture Theatre 2, Computer Laboratory, William Gates Building
• Security-related talks

Note that ex-directory lists are not shown.