Formal methods play a significant and increasing role in hardware verification, but their effectiveness can be impaired by the ac hoc nature of mainstream hardware languages such as VHDL, Verilog and SystemC, which have convoluted semantics that often necessitate contrived proof techniques. This dissertation investigates the application of formal reasoning to hardware architectures expressed in an alternative class of semantically elegant languages, which support efficient design, whilst also having been developed with proof techniques in mind.A networkonchip architecture belonging to the SpiNNaker manycore processor is specified in Concurrent Haskell, and a hand proof is presented which verifies a novel routing mechanism by mathematical induction.A 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. Proof strategies are written in the PVS strategy language; these automatically verify temporal logic theorems concerning the resulting monadic expressions, by employing a combination of model checking and deductive reasoning. The subset of BSV which is embedded includes module definition and instantiation, methods, implicit conditions, scheduling attributes, and rule composition using methods from instantiated modules.The aforementioned subset of BSV is also embedded in the specification language of the SAL model checker, and a verification strategy is presented which combines the specialised model checking capabilities of SAL with the diverse proof strategies of PVS.
Date of Award  31 Dec 2011 

Original language  English 

Awarding Institution   The University of Manchester


Supervisor  Steve Furber (Supervisor) & David Lester (Supervisor) 

 Formal Methods
 Functional Programming
 Theorem Prover
 Model Checker
 Bluespec
 Hardware Verification
Hardware Languages and Proof
Richards, D. (Author). 31 Dec 2011
Student thesis: Phd