Paper Authors

Abstract

NOTE: The first page of text has been automatically extracted and included below in lieu of an abstract

Considering Static Functional Verification of Digital Systems for HDL-based Courses

Mehran Massoumi

Department of Mathematics & Computer Science California State University, Hayward Hayward, CA 94542 massoumi@sbcglobal.net

Abstract: Functional verification of VLSI designs is known to be a highly time-consuming phase of the design cycle. Furthermore, with increasing complexity of ASICs and programmable ICs, this problem is becoming even more challenging. An emerging approach, which helps shorten the verification cycle, is the formal approach in which mathematical techniques are used to prove properties about a design. Due to the fact that formal checks are exhaustive and no test-vectors are needed, supporting tools have gained significant momentum as an add-on solution to simulation. It is the focus of this paper to present the formal or static approach and encourage use of the available tools in design projects for Senior/Graduate-level HDL-based courses. Advantages of the static approach will be discussed by presenting property formulation for a few RTL designs. Moreover, the property language PSL (Property Specification Language), which has the promise of becoming an IEEE standard, will be used in presenting property formulations.

Introduction:

A widely practiced approach for functional verification of digital designs is the use of simulation tools and test-bench models. Although simulation is a very effective solution, designers today are continuously faced with the challenge of exhaustive and timely verification of large systems. Many designs are taped-out with corner bugs, which is the result of non-exhaustive simulation coverage. Furthermore, with the growing complexity of IC designs and programmable parts, simulation runs are becoming prohibitively long and non-convergent. One solution, which was first commercially introduced in the mid 1990s, is the use of static tools[1] in addition to simulation. The Static approach consists of formulating properties about a design (instead of using test-benches) and proving those properties or assertions using mathematical proof techniques. A proven property is exhaustive in that it holds for all possible states, and sequences of inputs of the design. In today’s design community, static functional verification is gaining momentum as a solution for block-level verification of IC designs. The premise is that if individual blocks in a design are proven correct, then system-level verification will be a more manageable task. However, due to the capacity limitations of formal techniques, simulation is still needed for the system-level verification, where the size of designs can be prohibitively large for any formal tool to be useful.

Considering the significance of the verification problem and the emergence of static tools as an add-on solution to simulation, it is the focus of this paper to present the static approach and

“Proceedings of the 2005 American Society for Engineering Education Annual Conference & Exposition Copyright2005, American Society for Engineering Education”

• Citation

• Format
  • APA
  • APA - LaTeX bibitem
  • MLA
  • MLA - LaTeX bibitem
  • Bibtex
  • EndNote - RIS

Massoumi, M. (2005, June), Considering Static Functional Verification Of Digital Systems For Hdl Based Courses Paper presented at 2005 Annual Conference, Portland, Oregon. 10.18260/1-2--15495