Leveraging formal methods for improving processor verification | DVClub Cambridge

Processors present engineers with some of the biggest challenges faced in verification. For example, complexity in the design to extract maximum performance per watt of power, and multiple dependencies between instructions in one or multiple instruction streams, processor resources, and memory accesses create a verification space that is impossible to cover using simulation, let alone identify the key verification. This challenge used to be in the hands of a few companies with large teams and dedicated resources built on a commercial model, allowing them to invest heavily in verification. This is not necessarily the case for RISC-V developers.

Formal verification has always offered the potential to cover large verification spaces completely and therefore seems to be a natural choice for processor verification. This full afternoon DVClub will explore that potential In more detail offering real case studies, practical solutions, and suggestions that can be followed up back in the office.