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 条

[21] A perspective on specifying and verifying concurrent modules
Dinsdale-Young, Thomas
Pinto, Pedro da Rocha
Gardner, Philippa
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2018, 98 : 1 - 25
[22] Specifying and Verifying Advanced Control Features
Leavens, Gary T.
Naumann, David
Rajan, Hridesh
Aotani, Tomoyuki
LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: DISCUSSION, DISSEMINATION, APPLICATIONS, ISOLA 2016, PT II, 2016, 9953 : 80 - 96
[23] Specifying Languages and Verifying Programs with K
Rosu, Grigore
2013 15TH INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING (SYNASC 2013), 2014, : 28 - 31
[24] Specifying and verifying visual grasping tasks
Shkel, E
Ferrier, NJ
1997 IEEE INTERNATIONAL CONFERENCE ON ROBOTICS AND AUTOMATION - PROCEEDINGS, VOLS 1-4, 1997, : 688 - 694
[25] A NOTE ON SPECIFYING AND VERIFYING CONCURRENT PROCESSES
HOLENDERSKI, L
INFORMATION PROCESSING LETTERS, 1984, 18 (02) : 77 - 85
[26] Specifying and Verifying Sparse Matrix Codes
Arnold, Gilad
Hoelzl, Johannes
Koeksal, Ali Sinan
Bodik, Rastislav
Sagiv, Mooly
ICFP 2010: PROCEEDINGS OF THE 2010 ACM SIGPLAN INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING, 2010, : 249 - 260
[27] Specifying and Verifying Sparse Matrix Codes
Arnold, Gilad
Hoelzl, Johannes
Koeksal, Ali Sinan
Bodik, Rastislav
Sagiv, Mooly
ACM SIGPLAN NOTICES, 2010, 45 (09) : 249 - 260
[28] An environment for specifying and verifying security properties
Renaud, A
Krishnan, P
2001 AUSTRALIAN SOFTWARE ENGINEERING CONFERENCE, PROCEEDINGS, 2001, : 203 - 212
[29] Specifying and verifying reconfigurable software architectures
de Paula, VC
Justo, GRR
Cunha, PRF
INTERNATIONAL SYMPOSIUM ON SOFTWARE ENGINEERING FOR PARALLEL AND DISTRIBUTED SYSTEMS, PROCEEDINGS, 2000, : 21 - 31
[30] A runtime model-based framework for specifying and verifying adaptive RTE systems
Fredj, Nissaf
Kacem, Yessine Hadj
Abid, Mohamed
INTERNATIONAL JOURNAL OF COMPUTER APPLICATIONS IN TECHNOLOGY, 2020, 63 (04) : 309 - 326

← 1 2 3 4 5 →