The application of formal verification to SPW designs

被引：1

作者：

Akbarpour, B ^{[1
]}

Tahar, S ^{[1
]}

机构：

[1] Concordia Univ, Dept Elect & Comp Engn, Montreal, PQ H3H 1M8, Canada

来源：

EUROMICRO SYMPOSIUM ON DIGITAL SYSTEM DESIGN, PROCEEDINGS | 2003年

关键词：

D O I：

10.1109/DSD.2003.1231963

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

The Signal Processing WorkSystem (SPW) of Cadence is an integrated framework for developing DSP and communications products. Formal verification is a complementary technique to simulation based on mathematical logic. The HOL system is an environment for interactive theorem proving in a higher-order logic. It has an open user-extensible architecture which makes it suitable for providing proof support for embedded languages. In this paper we propose an approach to model SPW descriptions at different abstraction levels in HOL based on the shallow embedding technique. This will enable the formal verification of SPW designs which in the past could only be verified partially using conventional simulation techniques. We illustrate this novel application through a simple case study of a Notch filter.

引用

页码：325 / 332

页数：8

共 10 条

[1] AKBARPOUR B, 2002, LNCS, V2335, P185
[2] [Anonymous], 1993, CAMBRIDGE TRACTS THE
[3] BOULTON R, 1992, IFIP TRANS A, V10, P129
[4] *CAD DES SYST INC, 1999, SIGN PROC WORKS SPW
[5] Gordon M. J., 1993, INTRO HOL THEOREM PR
[6] From the editor
Harrington, JP
[J]. JOURNAL OF PLASTIC FILM & SHEETING, 2000, 16 (01) : 3 - 4
[7] HARRISON JR, 2000, LECT NOTES COMPUTER, V2152, P217
[8] Kern C., 1999, ACM Transactions on Design Automation of Electronic Systems, V4, P123, DOI 10.1145/307988.307989
[9] EFFECTS OF FINITE REGISTER LENGTH IN DIGITAL FILTERING AND FAST FOURIER-TRANSFORM
OPPENHEIM, AV
WEINSTEIN, CJ
[J]. PROCEEDINGS OF THE INSTITUTE OF ELECTRICAL AND ELECTRONICS ENGINEERS, 1972, 60 (08): : 957 - +
[10] Wilkinson J. H., 1964, Rounding Errors in Algebraic Processes

← 1 →