Specifying Hardware Timing with ET-LOTOS (extended version)

Citation

He J & Turner KJ (2001) Specifying Hardware Timing with ET-LOTOS (extended version). In: Margaria T & Melham TF (eds.) Correct Hardware Design and Verification Methods. Lecture Notes in Computer Science, Volume 2144. CHARME 2001 - 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, Livingston, Scotland, 04.09.2001-07.09.2001. Berlin: Springer Verlag, pp. 161-166. https://doi.org/10.1007/3-540-44798-9_14

Abstract
It is explained how DILL (Digital Logic in LOTOS) can be used to specify and analyse hardware timing characteristics using ET-LOTOS (Enhanced Timed LOTOS), a timed extension of the ISO standard formal language LOTOS (Language of Temporal Ordering Specification). Hardware component functionality and timing characteristics are rigorously specified and then validated. As will be seen, subtle timing problems can be found by using this approach.