Efficient verification of VLSI circuits based on syntax and denotational semantics
Filip Van Aelten · 1989
A fully automatic circuit verification system takes in a circuit description and a specification of its behavior, and checks whether the circuit behaves as specified. Existing verification systems follow one of two approaches: a deductive approach, based on a formal logic, or a rewrite rule approach, which starts from knowledge about how transistors work, and goes straight but slowly from premises to con-clusions. I present a new, more efficient approach, which incorporates large scale knowledge about VLSI circuits in a coherent fashion. The approach is based on the denotational method for defining the semantics of a programming language. A circuit is parsed according to a circuit grammar, and the resulting parse tree is mapped into a behavioral description which is matched with the user supplied specification. The new strategy is implemented in the program Semanticist.