VOSS - A Formal Hardware Verification System User's Guide

The Voss system is a formal verification system aimed primarily at hardware verification. In particular, verification using symbolic trajectory evaluation is strongly supported. The Voss system consists of a set of programs. The main one is called fl and is the core of the verification system. Since the metalanguage in fl is a fully general functional language in which Ordered Binary Decision Diagrams (OBDDs) have been built in, the verification system is not only useful for carrying out trajectory evaluation, but also for experimenting with various verification (formal and informal) techniques that require the use of OBDDs. This document is intended as both a user's guide and (to some extent) a reference guide. For the Voss alpha release, this document is still quite incomplete, but work is underway to remedy this.