Abstract :
Summary form only given. In this talk, I will introduce the formal verification challenges encountered in the design of Anton, a massively parallel, special-purpose machine for molecular dynamics simulations. I will review approaches that have had the most impact on the design verification of the chip, such as bug hunting, root-cause analysis, coverage closure and deadlock detection. A particular outcome of the verification effort for Anton is a method that attempts to identify hard-to-verify logic early in the design cycle, based on model checking. This approach allows early modifications of the RTL code that enhance its verifiability for both formal and simulation methods, reducing the long tail of verification time and effort.
Keywords :
formal verification; logic design; molecular dynamics method; operating systems (computers); program debugging; simulation; special purpose computers; Anton design massive parallel; RTL code; bug hunting; deadlock detection; design verification chip; formal verification challenges; industrial experience report; logic design cycle verification; molecular dynamics simulations; root cause analysis; simulation methods; special purpose machine; Automation; Circuit simulation; Computational modeling; Computer science; Formal verification; Hardware; Large-scale systems; Logic design; Probability distribution; System recovery;
