Functional verification of MOS circuits

ABSTRACT

This report describes the ideas behind Silica Pithecus, a program which verifies synchronous digital MOS VLSI circuits. Silica Pithecus accepts the schematic of an MOS VLSI circuit, declarations of the logical relationships between the inputs signals (e.g., which inputs are mutually exclusive), and a specification of the intended digital behavior of the circuit. If the circuit fails to meet its specification Silica Pithecus returns to the designer the precise reason it fails to do so. Unlike previous verification systems, Silica Pithecus employs a realistic electrical model. It also automatically generates the constraints on the inputs of a circuit which ensure the circuit will exhibit its intended digital behavior. These constraints are necessary for hierarchical verification. Silica Pithecus operates hierarchically, interactively, and incrementally.

REFERENCES

• Barrow: Barrow, Harry. "Proving the Correctness of Digital Hardware Designs" VLSI Design, July 1984
• Bryant85: Randal Bryant, "Symbolic Verification of MOS Circuits" Proceedings from the 1985 Chapel Hill Conference on VLSI. Edited by Hem'y Fuchs. Computer Science Press. 1985
• Bryant86: Ra~dal Bryant, "Can a Simulator Verify a CircuiL?" In Formal Aspects of VZSI Design, G.J. Milne, Ed!Ltor, North-Holland, 1986
• Eveking: Hans Eveking, "The verification of mutilevel hardware descriptions," Unpublished proceedings of the Darmstadt Workshop on the Verification of Hardware Designs.
• Gordon: Gordon, Mike. "A Very Simple Model of SequentialL Behavior of nMOS," Proceedings VLSI International Conference, J Gray (ed.) Academic Press, London and New York 1981
• Gordon84: "How to Specify and Verify Hardware Us'rag Higher Order Logic" Unpublished Lecture Notes, Autumn 1984. Cambridge University, UK. 1984
• Wagner: Todd Jeffry Wagner, Hardware verification., 1977
• Weise: Daniel Weise, Formal Multilevel Hierarchical Verific4~tion of Synchrouou~ MOS VL5I Circuita, Phi) Thesis, MIT, Department of Electrical Engineering and Computer Sc~.ence, 1986.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.2 Design Aids
          Subjects: Verification

Additional Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.1 Types and Design Styles
          Subjects: Memory technologies

General Terms:
Design, Verification