Specifying and verifying systems with multiple clocks

被引：4

作者：

Clarke, EM ^{[1
]}

Kroening, D ^{[1
]}

Yorav, K ^{[1
]}

机构：

[1] Carnegie Mellon Univ, Dept Comp Sci, Pittsburgh, PA 15213 USA

来源：

21ST INTERNATIONAL CONFERENCE ON COMPUTER DESIGN, PROCEEDINGS | 2003年

关键词：

D O I：

10.1109/ICCD.2003.1240872

中图分类号：

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

学科分类号：

0812 ;

摘要：

Multiple clock domains are a challenge for hardware specification and verification. We present a method for specifying the relations between multiple clocks, and for modeling the possible behaviors. We can then verify a hardware design assuming that the clocks meet these constraints. We implement our ideas in the context of SAT based Bounded Model Checking (BMC), using ANSI-C programs to specify the functional behavior of the design.

引用

页码：48 / 55

页数：8

共 50 条

[1] Verifying VHDL designs with multiple clocks in SMV
Smrcka, A.
Rehak, V.
Vojnar, T.
Safranek, D.
Matousek, P.
Rehak, Z.
Formal Methods: Applications and Technology, 2007, 4346 : 148 - 164
[2] Specifying and verifying PLC systems with TLA+
Zhang, Hehua
Merz, Stephan
Gu, Ming
THIRD INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS, 2009, : 293 - +
[3] A framework for specifying and verifying the behaviour of open systems
Bracciali, A
Brogi, A
Turini, F
JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2005, 63 (02): : 215 - 240
[4] Modelling, specifying, and verifying message passing systems
Bollig, B
Leucker, M
EIGHTH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING, PROCEEDINGS, 2001, : 240 - 247
[5] Formally specifying and verifying real-time systems
Kemmerer, RA
Kolano, PZ
FIRST IEEE INTERNATIONAL CONFERENCE ON FORMAL ENGINEERING METHODS, PROCEEDINGS, 1997, : 112 - 120
[6] SPECIFYING AND VERIFYING REQUIREMENTS OF REAL-TIME SYSTEMS
RAVN, AP
RISCHEL, H
HANSEN, KM
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1993, 19 (01) : 41 - 55
[7] Specifying and verifying real-time systems with timing uncertainty
Bae, HS
Chung, IS
Kwon, YR
JOURNAL OF SYSTEMS AND SOFTWARE, 2000, 50 (01) : 85 - 96
[8] A TOOL ENVIRONMENT FOR SPECIFYING AND VERIFYING MULTI-AGENT SYSTEMS
Schwarz, Christian
Mohammed, Ammar
Stolzenburg, Frieder
ICAART 2010: PROCEEDINGS OF THE 2ND INTERNATIONAL CONFERENCE ON AGENTS AND ARTIFICIAL INTELLIGENCE, VOL 2: AGENTS, 2010, : 323 - 326
[9] ACCEPTANCE AUTOMATA - A FRAMEWORK FOR SPECIFYING AND VERIFYING TCSP PARALLEL SYSTEMS
ALONSO, LM
PENA, R
LECTURE NOTES IN COMPUTER SCIENCE, 1991, 506 : 75 - 91
[10] Specifying and verifying PLC systems with TLA+: A case study
Zhang, Hehua
Merz, Stephan
Gu, Ming
COMPUTERS & MATHEMATICS WITH APPLICATIONS, 2010, 60 (03) : 695 - 705

← 1 2 3 4 5 →