The verification of scheduling algorithms
David P. Anderson, John Ainscough · 1994
Scheduling in high-level synthesis consists of assigning the operations contained within a circuit specification to clock cycles. An operational semantics of a simulation model for the design representation enables the semantics preserving properties of transformational algorithms to be established. This semantics and a simple scheduling algorithm have been mechanised in an automated theorem prover. The correctness of this algorithm has been proven.