Effective System Level Liveness Verification

Alexander Fedotov, Jeroen J.A. Keiren, Julien Schmaltz

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review


The language xMAS has been designed by Intel with the purpose of modelling and verification of hardware. Recently, the language was extended with finite state machines to make it more expressive [19]. Furthermore, it was shown how to prove liveness of such extended xMAS networks [19]. Unfortunately, we demonstrate that the proof technique is unsound. We provide an alternative approach which we have carefully proven to be correct. Moreover, we show that our approach scales very well, which makes it possible to prove liveness properties at the system level. In particular, we show that using our approach, it is possible to verify a power control architecture composed of 1299 state machines representing 50 power domains where each domain contains 5 master and 5 slave devices. Proving liveness of this system takes less than 10 minutes.
Originele taal-2Engels
TitelProceedings of the 20th Conference on Formal Methods in Computer-Aided Design, FMCAD 2020
RedacteurenAlexander Ivrii, Ofer Strichman, Warren A. Hunt, Georg Weissenbacher
UitgeverijInstitute of Electrical and Electronics Engineers
Aantal pagina's9
ISBN van elektronische versie9783854480426
StatusGepubliceerd - 21 sep. 2020


Duik in de onderzoeksthema's van 'Effective System Level Liveness Verification'. Samen vormen ze een unieke vingerafdruk.

Citeer dit