March 2-5, 2020

DoubleTree Hotel, San Jose, CA

MP Associates, Inc.

TUESDAY February 26, 9:00am - 10:30am | Oak

Formal Verification Methodologies
Sean Sarfarpour - Synopsys, Inc.
Using formal verification and assertions to strengthen your methodology.

1.1Property Driven Development of a RISC-V CPU
This paper demonstrates, at the example of implementing a RISC-V CPU, a novel top-down RTL design methodology called Property-Driven Development (PDD). The methodology starts from an abstract, transaction-level, hardware description in SystemC and produces a fully and formally verified RTL implementation. We present an open-source software tool supporting PDD. Using the tool, we develop an abstract system-level CPU model for the RISC-V R32I instruction set and refine it to an RTL implementation. Two different implementations for the same abstract model are provided.
 Speaker: Tobias Ludwig - Technische Universität Kaiserslautern
 Authors: Tobias Ludwig - Technische Universität Kaiserslautern
Michael Schwarz - Technische Universität Kaiserslautern
Joakim Urdahl - Nordic Semiconductor
Lucas Deutschmann - Technische Universität Kaiserslautern
Salaheddin Hetalani - Technische Universität Kaiserslautern
Dominik Stoffel - Technische Universität Kaiserslautern
Wolfgang Kunz - Technische Universität Kaiserslautern
1.2A Coverage-driven Formal Methodology for Verification Sign-off
Formal Verification has become a mainstream verification methodology and its potential has been widely recognized in finding resilient bugs in control path oriented designs. However, in the past FV was often considered a nice-to-have complement to simulation to explore corner case bugs, and simulation was still needed for verification signoff. Moreover, due to lack of common signoff metrics between simulation and FV, it is hard to report FV progress together with simulation. This paper promotes a coverage-driven FV methodology for verification signoff. It also enables FV/Simulation co-verification with merged coverage. Results show significant ROI in terms of quality and productivity.
 Speaker: Hao Chen - Intel Corp.
 Authors: Ang Li - Intel Corp.
Hao Chen - Intel Corp.
Jason Yu - Intel Corp.
EeLoon Teoh - Intel Corp.
Iswerya Prem Anand - Intel Corp.
1.3Automating the Formal Verification Sign-off Flow of Configurable Digital IP’s
Configurable Digital IP's verification requires to assure that any potential HW implementation is respecting the sign-off criteria. Formal static verification of highly configurable IP often does not allow to run exhaustive verification of all possible HW configurations. The intent of this paper is to describe an automated flow to generate a set of configuration using a pseudo-random constraint driven approach and then automatically run formal proof on these. The flow takes advantage of coverage collection and verification plan mapping to qualify a subset of runs as sufficient to grant a sign-off which respects the agreed configurations coverage target criteria.
 Speaker: Giovanni Auditore - STMicroelectronics
 Authors: Giovanni Auditore - STMicroelectronics
Giuseppe Falconeri - STMicroelectronics