June 12, 2005
June 12, 2005
June 15, 2005
10.344.1 - 10.344.7
Considering Static Functional Verification of Digital Systems for HDL-based Courses
Department of Mathematics & Computer Science California State University, Hayward Hayward, CA 94542 firstname.lastname@example.org
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.
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 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”
Massoumi, M. (2005, June), Considering Static Functional Verification Of Digital Systems For Hdl Based Courses Paper presented at 2005 Annual Conference, Portland, Oregon. https://peer.asee.org/15495
ASEE holds the copyright on this document. It may be read by the public free of charge. Authors may archive their work on personal websites or in institutional repositories with the following citation: © 2005 American Society for Engineering Education. Other scholars may excerpt or quote from these materials with the same citation. When excerpting or quoting from Conference Proceedings, authors should, in addition to noting the ASEE copyright, list all the original authors and their institutions and name the host city of the conference. - Last updated April 1, 2015