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 . Furthermore, it was shown how to prove liveness of such extended xMAS networks . 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.
|Titel||Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design, FMCAD 2020|
|Redacteuren||Alexander Ivrii, Ofer Strichman, Warren A. Hunt, Georg Weissenbacher|
|Uitgeverij||Institute of Electrical and Electronics Engineers|
|ISBN van elektronische versie||9783854480426|
|Status||Gepubliceerd - 21 sep 2020|