Technical Reports

The ICICS/CS Reading Room


UBC CS TR-90-27 Summary

Generic Specification of Digital Hardware, September 1990 Jeffrey J. Joyce

This paper argues that generic description is a powerful concept in the context of formal verification, in particular, the formal verification of digital hardware. The paper also describes a technique for creating generic specifications in any language with (at least) the expressive power of higher-order logic. This technique is based on the use of higher-order predicates parameterized by function variables and type variables. We believe that this technique is a very direct (if not the most direct) way to specify hardware generically. Two examples of generic specification are given in the pap er: a resettable counter and the programming level model of a very simple microprocessor.


If you have any questions or comments regarding this page please send mail to help@cs.ubc.ca.