Formal Analysis of SystemC Designs in Process Algebra

被引：2

作者：

Hojjat, Hossein ^{[2
]}

Mousavi, Mohammad Reza ^{[1
]}

Sirjani, Marjan ^{[3
,4
]}

机构：

[1] Eindhoven Univ Technol, Dept Comp Sci, NL-5600 MB Eindhoven, Netherlands

[2] Ecole Polytech Fed Lausanne, Stn 14, CH-1015 Lausanne, Switzerland

[3] Univ Tehran, Tehran, Iran

[4] Reykjavik Univ, Reykjavik, Iceland

来源：

FUNDAMENTA INFORMATICAE | 2011年 / 107卷 / 01期

关键词：

SystemC; Process Algebra; Formal Verification; mCRL2; VERIFICATION;

D O I：

10.3233/FI-2011-391

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

SystemC is an IEEE standard system-level language used in hardware/software co-design and has been widely adopted in the industry. This paper describes a formal approach to verifying SystemC designs by providing a mapping to the process algebra mCRL2. Our mapping formalizes both the simulation semantics as well as exhaustive state-space exploration of SystemC designs. By exploiting the existing reduction techniques of mCRL2 and also its model-checking tools, we efficiently locate the race conditions in a system and resolve them. A tool is implemented to automatically perform the proposed mapping. This mapping and the implemented tool enabled us to exploit process-algebraic verification techniques to analyze a number of case-studies, including the formal analysis of a single-cycle and a pipelined MIPS processor specified in SystemC.

引用

页码：19 / 42

页数：24

共 50 条

[1] Dependence Analysis and Automated Partitioning for Scalable Formal Analysis of SystemC Designs
Herber, Paula
Liebrenz, Timm
[J]. 2020 18TH ACM-IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR SYSTEM DESIGN (MEMOCODE), 2020, : 143 - 148
[2] Formal verification of LTL formulas for systemc designs
Grosse, D
Drechsler, R
[J]. PROCEEDINGS OF THE 2003 IEEE INTERNATIONAL SYMPOSIUM ON CIRCUITS AND SYSTEMS, VOL V: BIO-MEDICAL CIRCUITS & SYSTEMS, VLSI SYSTEMS & APPLICATIONS, NEURAL NETWORKS & SYSTEMS, 2003, : 245 - 248
[3] Formal Deadlock Checking on High-Level SystemC Designs
Chou, Chun-Nan
Hsu, Chang-Hong
Chao, Yueh-Tung
Huang, Chung-Yang
[J]. 2010 IEEE AND ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN (ICCAD), 2010, : 794 - 799
[4] Analyzing SystemC Designs: SystemC Analysis Approaches for Varying Applications
Stoppe, Jannis
Drechsler, Rolf
[J]. SENSORS, 2015, 15 (05) : 10399 - 10421
[5] Reachability analysis for formal verification of SystemC
Drechsler, R
Grosse, D
[J]. EUROMICRO SYMPOSIUM ON DIGITAL SYSTEM DESIGN, PROCEEDINGS: ARCHITECTURES, METHODS AND TOOLS, 2002, : 337 - 340
[6] Runtime deadlock analysis of SystemC designs
Cheung, Eric
Satapathy, Piyush
Pham, Vi
Hsieh, Harry
Chen, Xi
[J]. HLDVT'06: ELEVENTH ANNUAL IEEE INTERNATIONAL HIGH-LEVEL DESIGN VALIDATION AND TEST WORKSHOP, PROCEEDINGS, 2006, : 187 - +
[7] Formal Framework for Cost Analysis Based on Process Algebra
Nishizaki, Shin-ya
Kiyoto, Hiroki
[J]. COMMUNICATIONS AND INFORMATION PROCESSING, PT 1, 2012, 288 : 110 - 117
[8] Formal verification of SystemC designs using a Petri-Net based representation
Karlsson, Daniel
Eles, Petru
Peng, Zebo
[J]. 2006 DESIGN AUTOMATION AND TEST IN EUROPE, VOLS 1-3, PROCEEDINGS, 2006, : 1228 - +
[9] Checkers for SystemC designs
Grosse, D
Drechsler, R
[J]. SECOND ACM AND IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR CO-DESIGN, PROCEEDINGS, 2004, : 171 - 178
[10] Visualization of SystemC designs
Genz, Christian
Drechsler, Rolf
Angst, Gerhard
Linhard, Lothar
[J]. 2007 IEEE INTERNATIONAL SYMPOSIUM ON CIRCUITS AND SYSTEMS, VOLS 1-11, 2007, : 413 - +

← 1 2 3 4 5 →