University Homepage School Homepage School Contacts School Search

 

Paul Jackson

LFCS, ICSA & IRR, Informatics, University of Edinburgh; and Institute for System Level Integration, Alba Centre, Livingston

Formal Design of an Application-Specific Integrated Circuit.

Abstract

As IC designs become ever more complex, traditional design verification using simulations is becoming increasingly inadequate. For a while now, various formal techniques have been proposed as supplements or alternatives. These techniques involve analysing the logical structure of designs, almost always with the help of computer tools.

In this talk I'll discuss recent work carried out at Silicon Graphics [1] in using the Cadence Berkeley Labs SMV model-checking tool to formally model and verify a pipelined implementation of a directory-based cache-coherency protocol. The implementation hardware forms the most complex part of a 1M-gate ASIC that is used in SGI Origin 200 and 2000 multiprocessor servers.

The verification involves comparing the implementation against a reference specification of the protocol. It makes essential use of compositional methods to divide the verification into pieces --- each with no more than 250 bits of state --- that are manageable by the SMV tool.

The verification initially helped with the diagnosis and repair of subtle faults that only showed up in field tests of early versions of the servers. Subsequently it was used to check updated designs of the cache-coherency hardware. This work demonstrates that it is now possible for a hardware designer to formally design complex hardware within the strict time schedule of a design project.

Reference

1. The Formal Design of 1M-gate ASICs. Asgeir Th. Eiriksson. Formal Methods in Computer-Aided Design 1998. p49-63, Vol 1522, Lecture Notes in Computer Science, Springer Verlag.