FV benchmarks - http://godel.ece.utexas.edu/texas97-benchmarks/

• Subject: FV benchmarks - http://godel.ece.utexas.edu/texas97-benchmarks/
• From: Adnan Aziz <adnan@tarski.ece.utexas.edu>
• Date: Thu, 26 Mar 1998 07:55:44 -0600

Dear Colleagues,

A few months ago, I sent out a request to the design and verification
communities for pointers to hardware designs which could be used as 
formal verification (FV) benchmarks.  Many of you responded, and 
through the diligent efforts of the students in my FV class last
semester, we have assembled the TEXAS-97 verification benchmarks. 

This suite is available to the general public over the web, at the 
following site:

   http://godel.ece.utexas.edu/texas97-benchmarks

The designs are digital, synchronous, and control dominated; portions
are synthesizable.  Examples include:

  - PCI/Pi/PowerPC bus protocols,

  - MESI/MSI cache coherency protocols,

  - an MPEG decoder,

  - a DLX processor, and

  - an IF decode unit.


Along with Verilog and blif-mv source (which are suitable input to 
the VIS verification tool - refer to http://www.cad.eecs.berkeley.edu/~vis),
we have included formal specifications (in CTL), and project writeups.
The reports describe both the designs and the verification process
in VIS.

I would like to stress that these examples are meant to be
representative of their real-world origins; in many cases we 
have simplified them considerably.  In several instances, we were
unable to make the designs conform to their specifications;
these examples are suitable for experimenting with falsification
algorithms.

We plan to continue this effort; I would appreciate feedback, and 
suggestions for new examples.

In closing, I would like to thank all of you for your suggestions, 
and Malay Ganai (UT), Padmini Gopalakrishnan (UT), and Tom 
Shiple (Synopsys) for help in assembling the suite,


Sincerely,
Adnan and the EE382m FV Class, Fall 1997 UT Austin

ps - my apologies if you received duplicate copies of this mail


  ---------------------------------------------------------
  Adnan Aziz
  Assistant Professor, Electrical and Computer Engineering,
  The University of Texas, Austin TX, 78712-1084, 
  512 475 9774(w) 512 795 9420(h) www.ece.utexas.edu/~adnan
  ---------------------------------------------------------

• Prev: Second Call for Participation TABLEAUX'98
• Next: IRW/FMP'98 Final Call For Papers (Completed Work Category)
• Index: AMAST Mail 1998