Modular SMT-Based Verification of Rule-Based Hardware Designs

The highly-concurrent nature of hardware logic designs makes their design and verification difficult. Bluespec SystemVerilog (BSV) simplifies this problem by introducing the rule-level abstraction. Modules are expressed in terms of guarded atomic actions that appear to fire in a sequential order, even when multiple rules fire concurrently per clock cycle. This allows designers to think about concurrent systems one step at a time. This thesis aims to make hardware verification easier by leveraging the rule-level abstraction for verification using SMT-based verification, e.g. bounded and unbounded model checking. The main aspect of the rule-level abstraction taken advantage of is the modularity. Rule-level modules can only be interacted with through their interface methods, so if a module looks the same as its specification with respect to the legal sequences of method calls, then they can be used interchangeably without affecting the outer module. A modular verification technique that is based off of this idea can be used to replace complex submodules with simpler versions that reduce the complexity and the number of steps required for unbounded model checking. This modular verification methodology can take many problems that are infeasible for unbounded model checking and makes them feasible. Other aspects of rule-level hardware design languages (HDLs) are taken advantage of during verification such as the use of uninterpreted functions and abstract types. In this thesis, I present Spec `n' Check, an HDL inspired by BSV that is designed for powerful modularity and easy-to-write specifications. To fully support SMT-based verification, we present formal semantics for Spec `n' Check along with a symbolic representation of the semantics that can be used in SMT solvers. We also present what it means for a module to implement a specification and the related metatheorems that describe how the implements relation can be used to verify larger modules. We show that with this work, it is possible to formally verify a RISC-V pipelined processor implemented in the synthesizable subset of Spec `n' Check against an ISA specification in a matter of minutes of SMT solver run time. This is only possible thanks to module refinement and abstraction of the control and status register file (CSRF) and the memory system, and the use of uninterpreted functions.

Name thesis:degree_name

Doctoral

Department dc:contributor.department

Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2021

Author dc:creator

• Wright, Andrew C.

Advisor dc:contributor.advisor

• Arvind

Statement dc:rights

• In Copyright - Educational Use Permitted
• Copyright MIT

Licence dc:rights.uri

• http://rightsstatements.org/page/InC-EDU/1.0/

Handle dc:identifier.uri

https://hdl.handle.net/1721.1/139491

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/139491