The examples presented here were developed as term-projects for a class on Formal Verification (Fall 1997) offered by the Department of Electrical and Computer Engineering at the University of Texas, Austin under the guidance of Dr. Adnan Aziz.

    The examples were collected by posting requests on the newsgroups comp.lsi.cad and comp.arch and mailing to VIS users and the CAV list. Many people in academics and industry showed an interest in these. We hope that they will address the need of the verification community for meaningful design examples and benchmarks. The examples are digital, synchronous, and control dominated.The computational complexity required for formal verification of these designs covers a wide range.

The people involved in these projects are:

Abhijit Jas, Alper Sen, Anand Ramachandran, Cagdas Akturan, ChiaBin Liu, Debaleena Das, I-Min Liu, Jayanta Bhadra, Justin R. Denison, Kaustubh Das, Malay K. Ganai, Padmini Gopalakrishnan, Parminder S. Chhabra, Praveen K. Jaini, Rajat Chaudhry, Ram Narayan, Ritu Chaba, Sriraman Padmanabhan, Srivatsan Srinivasan, Wasim U. Quddus, Zhao Zhe.

The paper "Examples of HW Verification using VIS " gives a brief overview of each examples with the results.

The following examples are available in texas97-benchmarks.tar.gz :

1) MSI Cache Coherence Protocol(cache_coherence)
2) PCI Local BUS (PCI_BUS)
3) PI-Bus Protocol (PI_BUS)
4) MESI Cache Coherence Protocol (p6Bus)
5) MPEG System Decoder (MPEG)
6) Instruction Fetch Control Module of the Torch Microprocessor (ifetch)
7) DLX (DLX)
8) Blackjack (Blackjack)
9) PowerPC 60x Bus Interface (PPC60X_bus)

The directory name for each example is given in brackets. Each directory includes a write-up (in Post-Script) giving the specifications, block diagrams, properties, verification methods, results and inferences. Files giving the Verilog and blif_mv (encoded and symbolic) descriptions, and CTL formulas are also provided.

To download  the examples, click on the following URL: Texas-97 benchmarks (Approx 5 MBytes)

Instructions for downloading and using the examples:

Disclaimer : Every attempt has been made for the accuracy of the models. There  is a possiblity of having undetected bug in the examples.