From formal verification to silicon compilation

The authors report on an experiment whose main purpose was to identify the difficulties of integrating formal verification with conventional VLSI CAD (computer-aided design) methodology. The investigation was conducted using the Tamarack microprocessor designed for concrete experimentation. The authors decided to construct an implementation of Tamarack using GENESIL, a silicon compiler, in order to investigate the issues involved in the transition between a formal specification and the notation required as input to this VLSI CAD tool. The main conclusion is that the most effective use of formal hardware verification will be at the higher levels of VLSI system design, with lower levels best handled by conventional VLSI CAD tools.<>