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 条

[31] Power constrained high-level synthesis of battery powered digital systems
Nielsen, SF
Madsen, J
DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION, PROCEEDINGS, 2003, : 1136 - 1137
[32] A Symbolic Methodology for Formal Verification of High-level Data-Flow Synthesis
Yang, Zhi
Lv, Chao
Ma, Guangsheng
Shao, Jingbo
2008 9TH INTERNATIONAL CONFERENCE ON SOLID-STATE AND INTEGRATED-CIRCUIT TECHNOLOGY, VOLS 1-4, 2008, : 2345 - +
[33] Formal Verification of GCSE in the Scheduling of High-level Synthesis: Work-in-Progress
Hu, Jian
Hu, Yongyang
Yu, Long
Wang, Wentao
Yang, Haitao
Kang, Yun
Cheng, Jie
PROCEEDINGS OF THE 2020 INTERNATIONAL CONFERENCE ON HARDWARE/SOFTWARE CODESIGN AND SYSTEM SYNTHESIS (CODES+ISSS), 2019, : 1 - 2
[34] Reliability-Aware Resource Allocation and Binding in High-Level Synthesis
Chen, Liang
Ebrahimi, Mojtaba
Tahoori, Mehdi B.
ACM TRANSACTIONS ON DESIGN AUTOMATION OF ELECTRONIC SYSTEMS, 2016, 21 (02)
[35] On the Correlation between Resource Minimization and Interconnect Complexities in High-Level Synthesis
Dutt, Shantanu
Zhang, Xiuyan
Shi, Ouwen
PROCEEDINGS OF THE 2021 TWENTY SECOND INTERNATIONAL SYMPOSIUM ON QUALITY ELECTRONIC DESIGN (ISQED 2021), 2021, : 355 - 360
[36] Multi-Pumping for Resource Reduction in FPGA High-Level Synthesis
Canis, Andrew
Anderson, Jason H.
Brown, Stephen D.
DESIGN, AUTOMATION & TEST IN EUROPE, 2013, : 194 - 197
[37] Temperature-aware resource allocation and binding in high-level synthesis
Mukherjee, R
Memik, SO
Memik, G
42nd Design Automation Conference, Proceedings 2005, 2005, : 196 - 201
[38] High-Level Synthesis of Resource-oriented Approximate Designs for FPGAs
Leipnitz, Marcos T.
Nazar, Gabriel L.
PROCEEDINGS OF THE 2019 56TH ACM/EDAC/IEEE DESIGN AUTOMATION CONFERENCE (DAC), 2019,
[39] Fast Resource and Timing Aware Design Optimisation for High-Level Synthesis
Perina, Andre B.
Silitonga, Arthur
Becker, Jurgen
Bonato, Vanderlei
IEEE TRANSACTIONS ON COMPUTERS, 2021, 70 (12) : 2070 - 2082
[40] Thread Weaving: Static Resource Scheduling for Multithreaded High-Level Synthesis
Hsiao, Hsuan
Anderson, Jason
PROCEEDINGS OF THE 2019 56TH ACM/EDAC/IEEE DESIGN AUTOMATION CONFERENCE (DAC), 2019,

← 1 2 3 4 5 →