Model Checking in an Industrial Environment
Eva Fordran, Matthias Fruth, Ulrich Hensel, Hu Shaoyu, Madabhushi Srinivasan · MBMV · 2003
This paper presents experiences in applying model checking to register transfer level (RTL) design verification tasks. The presentation focuses on the description of typical verification problems and their formal capture as well as the application of reduction techniques. Moreover the paper briefly reports on those spots in the verification flow where model checking may be applied successfully. The paper discusses various rather typical RTL blocks that were subject to formal verification: FIFO control logics and arbiter blocks. These real-world examples provide a set of interesting verification challenges such as proper clock descriptions, synchronous constraints, multiple unaligned clock domains, usage of partial reference models, application of reduction techniques.