Title :
The verification of scheduling algorithms
Author :
Anderson, Damian P. ; Ainscough, John
Author_Institution :
Dept. of Electr. & Electron. Eng., Manchester Metropolitan Univ., UK
Abstract :
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
Keywords :
circuit analysis computing; formal verification; theorem proving; automated theorem prover; circuit specification; clock cycles; design representation; high-level synthesis; operational semantics; scheduling algorithms; semantics preserving properties; simulation model; transformational algorithms; verification;
Conference_Titel :
Structured Methods for Hardware Systems Design, IEE Colloquium on
Conference_Location :
London
