Experience with specification and verification of hardware using PROLOG

Abstract

A most important step in VLSI chip design is to write functional specifications very early in the design to debug the top-level protocols. Previously we developed a highly procedural concurrent language Sakura for functional specification; we described a complex memory system by Sakura. In this paper we take a completely opposite approach. We used PROLOG, a language based on predicate calculus, to write the behavior of the hardware as well as requirement specifications of the memory system of Dorado, a high-performance personal computer. Even though the styles of these languages are very different, we used similar methods to verify the specifications. We attached executable specifications. We attached executable requirement specifications in the form of input and output specifications. We compare these experiences.