Bwolen's Software

Bwolen's Software Page

Here are some software or benchmarks that I put together for my research. If you find any of these interesting or have any comments, please drop me a note. I would be very interested to hear from you. Thanks.

SMV 2.4b (276Kb tar/gzip)
This version is based on SMV version 2.4. I have done a bit of rewriting and added a few new features for my thesis research purposes. This is NOT an official version of SMV. It is released to facilitate other research and developments. Good luck hacking :). For the latest official version of SMV, click here. For more information, please see this README file.

Last updated 7/99 </DIV ALIGN="right">

PPBF: parallel PBF BDD package 0.1 (121Kb tar/gzip)
This package is a parallel BDD package based on partial breadth-first expansion. PPBF targets small scale Symmetric Multi-Processor (SMP) machines. Currently, only combinational operations are implemented. For more information, please see this README file.

Last updated 8/98 </DIV ALIGN="right">

BDD Trace Driver 0.9 (326Kb tar/gzip) (Under Construction!)
This package is a platform for executing BDD-call traces, where a BDD call trace is a record of function calls to BDD operations. The "BDD trace driver" can be used either to study or to benchmark various BDD packages. For more information, please see this README file.

Last updated 11/98 </DIV ALIGN="right">

BDD Traces
These are collections of BDD-call traces, where a BDD call trace is a record of function calls to BDD operations. These collections can be used to benchmark BDD packages.

SSS.1.0 Traces: available from this site.
Superscalar Suite 1.0 containing propositional logic formulas to be checked for being tautologies. This benchmark is created by Miroslav N. Velev (mvelev@ece.cmu.edu). For more information, please see this README file.

Last updated 4/99 </DIV ALIGN="right">

SMV-Traces98 (6.3Mb tar/gzip)
Traces generated by the Symbolic Model Verifier (SMV). For more information, please see this README file.

Last updated 8/98 </DIV ALIGN="right">

ISCAS85 Traces (170Kb tar/gzip)
This set contains the ISCAS85 benchmark circuits converted to the trace format by Yirng-An Chen (yachen@cs.cmu.edu). For more information, please see this README file.

Last updated 8/98 </DIV ALIGN="right">

SMV Models (482Kb tar/gzip) (Under Construction!)
This is a collection of SMV models. I found it useful for benchmarking new SMV improvements. I have also used these models to generate BDD-call traces to benchmark BDD packages. For more information, please see this README file.

Last updated 3/98 </DIV ALIGN="right">

To Bwolen's Home Page

Bwolen Yang bwolen@cmu.edu
[count] accesses since March 1998.