Combining Symbolic Simulation and Groebner Bases Approach for Constrained PSL Property Verification
作者： Xinyan Gao , Ning Zhou , Fengqi Li , Dakui Li
DOI: 10.1007/978-3-642-26001-8_49
关键词:
摘要: In this paper, we presents a novel method towards PSL assertion checking by using computer algebra system to perform symbolic simulation over synchronous circuit model. The studied is based on Groebner bases and can deal with constrained subset of Boolean layer. We provide an algorithm framework constructing data-flow model calculating the zero set relationship their polynomials. This paper shows that canonical representations for assertions as well models. approach will be useful supplement existent verification methods simulation.
springer.com
sci-hub.st 参考文章(9)
Cindy Eisner, Dana Fisman, A Practical Introduction to PSL (Series on Integrated Circuits and Systems) Springer-Verlag New York, Inc.. ,(2006)
Kai-Hui Chang, Wei-Ting Tu, Yi-Jong Yeh, Sy-Yen Kuo, A simulation-based temporal assertion checker for PSL midwest symposium on circuits and systems. ,vol. 3, pp. 1528- 1531 ,(2003) , 10.1109/MWSCAS.2003.1562587
Heinz Kredel, Volker Weispfenning, Thomas Becker, Gröbner Bases: A Computational Approach to Commutative Algebra ,(2011)
J. Smith, G. De Micheli, Polynomial circuit models for component matching in high-level synthesis IEEE Transactions on Very Large Scale Integration Systems. ,vol. 9, pp. 783- 800 ,(2001) , 10.1109/92.974892
John A. Darringer, The application of program verification techniques to hardware verification design automation conference. pp. 373- 379 ,(1979) , 10.5555/800292.811742
B. Buchberger, Greobner Bases : an algorithmic method in polynomial ideal theory Multidimensional Systems Theory. pp. 184- 232 ,(1985)
J.A. Darringer, The Application of Program Verification to Hardware Verification design automation conference. pp. 375- 381 ,(1979) , 10.1109/DAC.1979.1600139
Tuomas Launiainen, Keijo Heljanko, Tommi Junttila, Efficient Model Checking of PSL Safety Properties 2010 10th International Conference on Application of Concurrency to System Design. pp. 95- 104 ,(2010) , 10.1109/ACSD.2010.27
Jinzhao Wu, Lin Zhao, Multi-Valued Model Checking via Groebner Basis Approach theoretical aspects of software engineering. pp. 35- 44 ,(2007) , 10.1109/TASE.2007.35