| Conference: | Verification Futures 2019 (click here to see full programme) |
| Speaker: | Sergio Marchese, OneSpin Solutions |
| Presentation Title: | Formalizing the RISC-V ISA in a set of SystemVerilog assertions that can be proven to be complete, consistent, and free from gaps |
| Abstract: | RISC-V cores are becoming increasingly attractive for a variety of applications. High confidence that a RISC-V core correctly implements the instruction set architecture (ISA) specification is crucial to drive adoption, particularly when security and safety are key concerns. But how can a new architecture compete with established cores that are verified with flows and test suites that have been developed over the course of decades? Formal verification is an established, powerful technology that can detect the most rare corner-case bugs. However, an incomplete of erroneous set of assertions can result in missed bugs. Moreover, processor verification is generally hard and requires significant effort and specialized skills.
In this presentation, we introduce a verification IP consisting of a set of SystemVerilog assertions that formalize the RISC-V ISA. Crucially, the set of assertions can be proven to be complete and free from gaps. Moreover, the assertions do not depend on a particular core micro-architecture and can be reused across a variety of pipeline implementations. With this approach, RISC-V cores can not only demonstrate an unparalleled level of functional quality, but also provide evidence that no undocumented functions or malicious logic is present. |
| Speaker Bio: | Sergio Marchese has 19 years of experience in hardware design, constrained-random simulation, formal verification and Design-for-Test. Marchese has built and managed state-of-the-art teams, successfully achieving formal sign-off on complex designs. Before taking the role of technical marketing manager at OneSpin, he served at Huawei, leading formal verification for ARM CPU and consumer SoCs. |
| Slides |
