Theorem Proving Guided Development of Formal Assertions in a Resource-Constrained Scheduler For High-Level Synthesis

摘要

This paper presents a formal specification and a proof of correctness for the widely-used Force- Directed List Scheduling (FDLS) algorithm for resource-constrained scheduling of data flow graphs in high-level Synthesis systems. 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 are formally state and proved In a higher-order logic theorem proving environment.