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 条

[41] Performance and Resource Modeling for FPGAs using High-Level Synthesis tools
Da Silva, Bruno
Braeken, An
D'Hollander, Erik H.
Touhafi, Abdellah
PARALLEL COMPUTING: ACCELERATING COMPUTATIONAL SCIENCE AND ENGINEERING (CSE), 2014, 25 : 523 - 531
[42] Performing high-level synthesis via program transformations within a theorem power
Blumenrohr, C
Eisenbiegler, D
24TH EUROMICRO CONFERENCE - PROCEEDING, VOLS 1 AND 2, 1998, : 34 - 37
[43] A Design Approach to Automatically Synthesize ANSI-C Assertions during High-Level Synthesis of Hardware Accelerators
Ben Hammouda, Mohamed
Coussy, Philippe
Lagadec, Loic
2014 IEEE INTERNATIONAL SYMPOSIUM ON CIRCUITS AND SYSTEMS (ISCAS), 2014, : 165 - 168
[44] A high-level domain-specific language for SIEM (design, development and formal verification)
Nazir, Anam
Alam, Masoom
Malik, Saif U. R.
Akhunzada, Adnan
Cheema, Muhammad Nadeem
Khan, Muhammad Khurram
Ziang, Yang
Khan, Tanveer
Khan, Abid
CLUSTER COMPUTING-THE JOURNAL OF NETWORKS SOFTWARE TOOLS AND APPLICATIONS, 2017, 20 (03): : 2423 - 2437
[45] A high-level domain-specific language for SIEM (design, development and formal verification)
Anam Nazir
Masoom Alam
Saif U. R. Malik
Adnan Akhunzada
Muhammad Nadeem Cheema
Muhammad Khurram Khan
Yang Ziang
Tanveer Khan
Abid Khan
Cluster Computing, 2017, 20 : 2423 - 2437
[46] Selective Resource Sharing with RT-Level Retiming for Clock Enhancement in High-Level Synthesis
Hara-Azumi, Yuko
Matsuba, Toshinobu
Tomiyama, Hiroyuki
Honda, Shinya
Takada, Hiroaki
2012 IEEE 14TH INTERNATIONAL CONFERENCE ON HIGH PERFORMANCE COMPUTING AND COMMUNICATIONS & 2012 IEEE 9TH INTERNATIONAL CONFERENCE ON EMBEDDED SOFTWARE AND SYSTEMS (HPCC-ICESS), 2012, : 1534 - 1540
[47] REHLS: Resource-aware Program Transformation Workflow for High-level Synthesis
Lotfi, Atieh
Gupta, Rajesh K.
2017 IEEE 35TH INTERNATIONAL CONFERENCE ON COMPUTER DESIGN (ICCD), 2017, : 533 - 536
[48] Timing Variation-Aware Scheduling and Resource Binding in High-Level Synthesis
Mittal, Kartikey
Joshi, Arpit
Mutyam, Madhu
ACM TRANSACTIONS ON DESIGN AUTOMATION OF ELECTRONIC SYSTEMS, 2011, 16 (04)
[49] Resource allocation in high-level synthesis with the reduction of hard-to-test structure
Li, L
Wei, SJ
Yang, ZL
CHINESE JOURNAL OF ELECTRONICS, 2000, 9 (04): : 369 - 374
[50] A Design-flow for High-Level Synthesis and Resource Estimation of Reconfigurable Architectures
Pasha, Muhammad Adeel
Siddiqui, Bilal
Farooq, Umer
2015 10TH IEEE INTERNATIONAL CONFERENCE ON DESIGN & TECHNOLOGY OF INTEGRATED SYSTEMS IN NANOSCALE ERA (DTIS), 2015,

← 1 2 3 4 5 →