DocumentCode
288052
Title
The verification of scheduling algorithms
Author
Anderson, Damian P. ; Ainscough, John
Author_Institution
Dept. of Electr. & Electron. Eng., Manchester Metropolitan Univ., UK
fYear
1994
fDate
1994
Firstpage
42552
Lastpage
42556
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;
fLanguage
English
Publisher
iet
Conference_Titel
Structured Methods for Hardware Systems Design, IEE Colloquium on
Conference_Location
London
Type
conf
Filename
369630
Link To Document