Improving Hardware Designs whilst Simplifying their Proof

We describe a study to investigate the notion of "design for verifiability". Our aim was to determine whether the cost of verification by interactive proof can be reduced by making appropriate design decisions. A major consideration was that such decisions should not compromise other design goals such as performance and functionality. We attempted to formally verify a real hardware design, noting factors which slowed the proof. On the basis of the identified bottlenecks, design changes were suggested by the verifier which would remove the problems. These were evaluated for acceptability by the original designer. Finally a new design was verified incorporating many of the suggested changes. This demonstrated that the expected advantages were realized.