Effective System Level Liveness Verification

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

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-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.
Original languageEnglish
Title of host publicationProceedings of the 20th Conference on Formal Methods in Computer-Aided Design, FMCAD 2020
EditorsAlexander Ivrii, Ofer Strichman, Warren A. Hunt, Georg Weissenbacher
PublisherInstitute of Electrical and Electronics Engineers
Number of pages9
ISBN (Electronic)9783854480426
Publication statusPublished - 21 Sept 2020


  • Formal verification
  • communication networks
  • finite state machines
  • liveness


Dive into the research topics of 'Effective System Level Liveness Verification'. Together they form a unique fingerprint.

Cite this