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 条

[31] TEMPORAL PREDICATE TRANSITION NETS - A NEW FORMALISM FOR SPECIFYING AND VERIFYING CONCURRENT SYSTEMS
HE, XD
INTERNATIONAL JOURNAL OF COMPUTER MATHEMATICS, 1992, 45 (3-4) : 171 - 184
[32] Modelling, specifying and verifying self-adaptive systems instantiating MAPE patterns
Hachicha, Marwa
Ben Halima, Riadh
Kacem, Ahmed Hadj
INTERNATIONAL JOURNAL OF COMPUTER APPLICATIONS IN TECHNOLOGY, 2018, 57 (01) : 28 - 44
[33] Specifying and verifying active vision-based robotic systems with the SIGNAL environment
Marchand, E
Rutten, E
Marchand, H
Chaumette, F
INTERNATIONAL JOURNAL OF ROBOTICS RESEARCH, 1998, 17 (04): : 418 - 432
[34] Specifying and verifying temporal behavior of high assurance systems using reachability tree logic
Yang, SJH
Chu, W
Lin, S
Lee, J
THIRD IEEE INTERNATIONAL HIGH-ASSURANCE SYSTEMS ENGINEERING SYMPOSIUM, PROCEEDINGS, 1998, : 150 - 156
[35] SPECIFYING, PROGRAMMING AND VERIFYING REAL-TIME SYSTEMS USING A SYNCHRONOUS DECLARATIVE LANGUAGE
HALBWACHS, N
PILAUD, D
OUABDESSELAM, F
GLORY, AC
LECTURE NOTES IN COMPUTER SCIENCE, 1990, 407 : 213 - 231
[36] Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity
Sergey, Ilya
Nanevski, Aleksandar
Banerjee, Anindya
PROGRAMMING LANGUAGES AND SYSTEMS, 2015, 9032 : 333 - 358
[37] Specifying and Verifying the Correctness of Dynamic Software Updates
Hayden, Christopher M.
Magill, Stephen
Hicks, Michael
Foster, Nate
Foster, Jeffrey S.
VERIFIED SOFTWARE: THEORIES, TOOLS, EXPERIMENTS, 2012, 7152 : 278 - +
[38] Formal methods for specifying, validating, and verifying requirements
Heitmeyer, Constance L.
JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 2007, 13 (05) : 607 - 618
[39] An approach to specifying and verifying safety-critical systems with practical formal method SOFL
Liu, SY
Asuka, M
Komaya, K
Nakamura, Y
FOURTH IEEE INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS - PROCEEDINGS, 1998, : 100 - 114
[40] Towards Formally Specifying and Verifying Transactional Memory
Doherty, Simon
Groves, Lindsay
Luchangco, Victor
Moir, Mark
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 259 : 245 - 261

← 1 2 3 4 5 →