Transforming the theorem prover into a digital design tool: From concept car to off-road vehicle

Abstract

As digital designs grow evermore complex and design cycles become ever shorter, traditional informal methods of design verification are proving inadequate. Design teams are increasingly turning to formal techniques to address this "verification crunch". The theorem prover, with its emphasis on establishing correctness, is arguably the dream design verification tool; however, theorem provers are rarely used in digital design. Much like automotive industry "concept cars", theorem provers provide a compelling vision of the future, but in the real world of industrial design they have proven to be difficult to drive and expensive to maintain. We suggest ways that the theorem prover "concept cars" of today can be adapted to become the "off-road vehicles" necessary to negotiate the rough-and-tumble terrain of digital design in the 21st century.