Vapor

Abstraction and Verification of Verilog Models

By

Zaher Andraus and Karem Sakallah

University of Michigan, Ann Arbor

Vapor what? | News | Papers | Downloads | Help

Vapor what?

Vapor (stands for "Verilog Abstraction for Processor Verification") is an automatic tool for abstracting ("vaporizing") RTL to term-level model for verification purposes. The resulting term-level description can be analyzed using validation engines like SVC and UCLID.

Vapor allows abstracting the RTL, and applying UCLID or SVC for verification of (mainly equivalence, although not restricted to)  safety properties. In case of a counterexample trace reported by the validation engine, Vapor is capable of producing the needed information to check the feasibility of the counterexample. This is done by producing ACL2 consistency expression that can be checked for satisfiability. This aids the designer/verification engineer to easily reason about the counterexample and map it back to actual Verilog trace. In Vapor, we put special emphasis on: a) minimizing false counterexamples, b) minimizing the size of the UCLID/SVC model, and c) full automation.

The generation of ACL2 expressions is not supported anymore. Currently we are integrating Vapor in the Reveal system, which includes a counterexample-guided automatic refinement process, and reasons about false negatives via invoking a satisfiability solver. Stay tuned for the release of Reveal.

back to top

News

[04.26.05] A new bytecode release (v0.97) is now available. Please check the Downloads section.

[10.19.04] A beta bytecode release (v0.95) is now available. Please check the Downloads section.

back to top

Papers

Zaher S. Andraus and Karem A. Sakallah, "Automatic Abstraction and Verification of Verilog Models," In proceedings of the 41^st Design Automation Conference, 2004, pp. 218-223.

Abstract: Abstraction plays a critical role in verifying complex systems. A number of languages have been proposed to model hardware systems by, primarily, abstracting away their wide datapaths while keeping the low-level details of their control logic. This leads to a significant reduction in the size of the state space and makes it possible to verify intricate control interactions formally. These languages, however, require that the abstraction be done manually, a tedious and error-prone process. In this paper we describe Vapor, a tool that automatically abstracts behavioral RTL Verilog to the CLU language used by the UCLID system. Vapor performs a sound abstraction with emphasis on minimizing false errors. Our method is fast, systematic, and complements UCLID by serving as a back-end for dealing with UCLID counterexamples. Preliminary results show the feasibility of automatic abstraction and its utility in formal verification.

Download pdf version, download the presentation.

back to top

Downloads

The latest (and only publicly) available version is 0.95.

Contact Zaher Andraus for obtaining the software.

back to top

Help

Please contact Zaher Andraus for any questions/comments regarding Vapor.

back to top

This page was last updated on 04/26/2005 08:13:03 PM -0400.