ATLAS: Automatic Term-Level Abstraction of RTL Designs

Bryan A. Brady, University of California, Berkeley
Randal E. Bryant, Carnegie Mellon University
Sanjit A. Seshia, University of California, Berkeley
John W. O'Leary, Intel Corporation

The final version of the paper can be found here: here: memocode2010-atlas.pdf

Download ATLAS: 32-bit binary 64-bit binary Source

ATLAS is released under the BSD license.

For information on how to use ATLAS see the user-guide. The user-guide is also located in the doc directory of the source distribution.

Download gzipped tarball containing all examples: memocode-2010-examples.tgz (180MB, expands to 860MB)

Note about USB example: There are two CRC modules present, a 16-bit and 5-bit version. Both modules pass random simulation testing, however, only the 16-bit CRC module is abstracted. The 5-bit CRC module is only present in the original USB design, not the refined design. Therefore, abstracting the 5-bit CRC module will not benefit performance because it isn't in the cone-of-influence of the property being checked.