Journal of Applied Mathematics
Volume 2013 (2013), Article ID 740194, 14 pages
http://dx.doi.org/10.1155/2013/740194
Research Article

Wu’s Characteristic Set Method for SystemVerilog Assertions Verification

Xinyan Gao,1 Ning Zhou,2,3 Jinzhao Wu,4 and Dakui Li1

1School of Software of Dalian University of Technology, Dalian 116620, China
2School of Computer and Information Technology, Beijing Jiaotong University, Beijing 10044, China
3School of Electronic and Information Engineering, Lanzhou Jiaotong University, Lanzhou 730070, China
4Guangxi Key Laboratory of Hybrid Computation and IC Design Analysis, Guangxi University for Nationalities, Nanning 530006, China

Received 8 February 2013; Revised 9 April 2013; Accepted 9 April 2013

Academic Editor: Xiaoyu Song

Copyright © 2013 Xinyan Gao et al. This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.

Abstract

We propose a verification solution based on characteristic set of Wu’s method towards SystemVerilog assertion checking over digital circuit systems. We define a suitable subset of SVAs so that an efficient polynomial modeling mechanism for both circuit descriptions and assertions can be applied. We present an algorithm framework based on the algebraic representations using characteristic set of polynomial system. This symbolic algebraic approach is a useful supplement to the existent verification methods based on simulation.