Effective System Level Liveness Verification

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

doi:10.34727/2020/isbn.978-3-85448-042-6_7

Effective System Level Liveness Verification

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

Abstract

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 language	English
Title of host publication	Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design, FMCAD 2020
Editors	Alexander Ivrii, Ofer Strichman, Warren A. Hunt, Georg Weissenbacher
Publisher	Institute of Electrical and Electronics Engineers
Pages	7-15
Number of pages	9
ISBN (Electronic)	9783854480426
DOIs	https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_7
Publication status	Published - 21 Sept 2020

Keywords

Formal verification
communication networks
finite state machines
liveness

Access to Document

10.34727/2020/isbn.978-3-85448-042-6_7

Cite this

Fedotov, A., Keiren, J. J. A., & Schmaltz, J. (2020). Effective System Level Liveness Verification. In A. Ivrii, O. Strichman, W. A. Hunt, & G. Weissenbacher (Eds.), Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design, FMCAD 2020 (pp. 7-15). Article 9283645 Institute of Electrical and Electronics Engineers. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_7

@inproceedings{5dba8f14866a48c8bb393dfb3f3a7162,

title = "Effective System Level Liveness Verification",

abstract = "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.",

keywords = "Formal verification, communication networks, finite state machines, liveness",

author = "Alexander Fedotov and Keiren, {Jeroen J.A.} and Julien Schmaltz",

year = "2020",

month = sep,

day = "21",

doi = "10.34727/2020/isbn.978-3-85448-042-6_7",

language = "English",

pages = "7--15",

editor = "Alexander Ivrii and Ofer Strichman and Hunt, {Warren A.} and Georg Weissenbacher",

booktitle = "Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design, FMCAD 2020",

publisher = "Institute of Electrical and Electronics Engineers",

address = "United States",

}

Effective System Level Liveness Verification. / Fedotov, Alexander; Keiren, Jeroen J.A.; Schmaltz, Julien.
Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design, FMCAD 2020. ed. / Alexander Ivrii; Ofer Strichman; Warren A. Hunt; Georg Weissenbacher. Institute of Electrical and Electronics Engineers, 2020. p. 7-15 9283645.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Effective System Level Liveness Verification

AU - Fedotov, Alexander

AU - Keiren, Jeroen J.A.

AU - Schmaltz, Julien

PY - 2020/9/21

Y1 - 2020/9/21

N2 - 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.

AB - 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.

KW - Formal verification

KW - communication networks

KW - finite state machines

KW - liveness

UR - http://www.scopus.com/inward/record.url?scp=85099263840&partnerID=8YFLogxK

U2 - 10.34727/2020/isbn.978-3-85448-042-6_7

DO - 10.34727/2020/isbn.978-3-85448-042-6_7

M3 - Conference contribution

SP - 7

EP - 15

BT - Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design, FMCAD 2020

A2 - Ivrii, Alexander

A2 - Strichman, Ofer

A2 - Hunt, Warren A.

A2 - Weissenbacher, Georg

PB - Institute of Electrical and Electronics Engineers

ER -

Effective System Level Liveness Verification

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Sound idle and block equations for finite state machines in xMAS

Cite this