Theorem proving guided development of formal assertions in a resource-constrained scheduler for high-level synthesis

被引：3

作者：

Narasimhan, N ^{[1
]}

Teica, E ^{[1
]}

Radhakrishnan, R ^{[1
]}

Govindarajan, S ^{[1
]}

Vemuri, R ^{[1
]}

机构：

[1] Univ Cincinnati, Lab Digital Design Environm, Dept ECECS, Cincinnati, OH 45221 USA

来源：

INTERNATIONAL CONFERENCE ON COMPUTER DESIGN: VLSI IN COMPUTERS AND PROCESSORS, PROCEEDINGS | 1998年

关键词：

D O I：

10.1109/ICCD.1998.727079

中图分类号：

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

学科分类号：

0812 ;

摘要：

A formal specification and a proof of correctness of the widely-used Force-Directed List Scheduling (FDLS) algorithm for resource-constrained scheduling in high-level synthesis systems is presented. The proof effort is conducted using a higher-order logic theorem prover During the proof effort many interesting properties of the FDLS algorithm are discovered. These properties constitute a detailed set of formal assertions and invariants that should hold at various steps in the FDLS algorithm. They are then inserted as programming assertions in the implementation of the FDLS algorithm in a production-strength high-level synthesis system. When turned on, the programming assertions (1) certify whether a specific run of the FDLS algorithm produced correct schedules and, (2) in the event of failure, help discover and isolate errors in the FDLS implementation.

引用

页码：392 / 399

页数：8

共 50 条

[1] Theorem Proving Guided Development of Formal Assertions in a Resource-Constrained Scheduler for High-Level Synthesis
Naren Narasimhan
Elena Teica
Rajesh Radhakrishnan
Sriram Govindarajan
Ranga Vemuri
Formal Methods in System Design, 2001, 19 : 237 - 273
[2] Theorem proving guided development of formal assertions in a resource-constrained scheduler for high-level synthesis
Narasimhan, N
Teica, E
Radhakrishnan, R
Govindarajan, S
Vemuri, R
FORMAL METHODS IN SYSTEM DESIGN, 2001, 19 (03) : 237 - 273
[3] On the effectiveness of theorem proving guided discovery of formal assertions for a register allocator in a high-level synthesis system
Narasimhan, N
Vemuri, R
THEOREM PROVING IN HIGHER ORDER LOGICS, 1998, 1479 : 367 - 386
[4] Heuristic algorithm for the resource-constrained scheduling problem during high-level synthesis
Wu, Y. -H.
Yu, C. -J.
Wang, S. -D.
IET COMPUTERS AND DIGITAL TECHNIQUES, 2009, 3 (01): : 43 - 51
[5] Resource-Constrained High-Level Datapath Optimization in ASIP Design
Chen, Yuankai
Zhou, Hai
DESIGN, AUTOMATION & TEST IN EUROPE, 2013, : 198 - 201
[6] Resolution-Like Theorem Proving for High-Level Conditions
Pennemann, Karl-Heinz
GRAPH TRANSFORMATIONS, ICGT 2008, 2008, 5214 : 289 - 304
[7] SkyCastle: A Resource-Aware Multi-Loop Scheduler for High-Level Synthesis
Oppermann, Julian
Sommer, Lukas
Weber, Lukas
Reuter-Oppermann, Melanie
Koch, Andreas
Sinnen, Oliver
2019 INTERNATIONAL CONFERENCE ON FIELD-PROGRAMMABLE TECHNOLOGY (ICFPT 2019), 2019, : 36 - 44
[8] Formal Verification of High-Level Synthesis
Herklotz, Yann
Pollard, James D.
Ramanathan, Nadesh
Wickerson, John
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2021, 5 (OOPSLA):
[9] Timing and Resource Constrained Leakage Power Aware Scheduling in High-Level Synthesis
Wang, Nan
Hao, Cong
Liu, Nan
Zhang, Haoran
Yoshimura, Takeshi
2013 IEEE 10TH INTERNATIONAL CONFERENCE ON ASIC (ASICON), 2013,
[10] Correct high-level synthesis: a formal perspective
Mendias, JM
Hermida, R
Fernandez, M
DESIGN, AUTOMATION AND TEST IN EUROPE, PROCEEDINGS, 1998, : 977 - 978

← 1 2 3 4 5 →