FormalHandshake — Open Source Design and Verification Flow for Complex Hardware Circuits: Tool Paper

Abstract

Formal verification methods like bounded model checking can deliver reassurance by proving safety and security properties. However, they come with their own challenges and limits, often preventing them to be an integral part of digital system designs. In this paper we introduce FormalHandshake, a hardware design and verification tool which represents the system as a structured graph. This allows to decompose the state space early on and enables the early use of formal methods, integrating them into an efficient high level design flow. We demonstrate the tool and its design flow, and show the construction and formal verification of a RISC-V CPU generator as an extended case study.