Voss | A Formal Hardware Verification System

User's Guide

Technical Report 93-45

Carl-Johan H. Seger

Department of Computer Science

University of British Columbia

Vancouver, B.C. V6T 1Z4 Canada

Email: [email protected]

December 6, 1993

Abstract

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 and is the core of the verification system. Since the metalanguage in 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.