Visible to the public Formal Verification Technology for Asynchronous Communication Protocol

TitleFormal Verification Technology for Asynchronous Communication Protocol
Publication TypeConference Paper
Year of Publication2019
AuthorsHu, Yayun, Li, Dongfang
Conference Name2019 IEEE 19th International Conference on Software Quality, Reliability and Security Companion (QRS-C)
ISBN Number978-1-7281-3925-8
Keywordsaerospace FPGA software products, assert, asynchronous communication, asynchronous communication protocol, blind spots, Clocks, Collaboration, complete verification process, composability, compositionality, field programmable gate arrays, formal verification, formal verification technology, policy-based governance, privacy, process control, Product design, product design quality, property, protocol verification, Protocols, PSL, pubcrawl, Software, traditional simulation method, UART communication, verification work efficiency

For aerospace FPGA software products, traditional simulation method faces severe challenges to verify product requirements under complicated scenarios. Given the increasing maturity of formal verification technology, this method can significantly improve verification work efficiency and product design quality, by expanding coverage on those "blind spots" in product design which were not easily identified previously. Taking UART communication as an example, this paper proposes several critical points to use formal verification for asynchronous communication protocol. Experiments and practices indicate that formal verification for asynchronous communication protocol can effectively reduce the time required, ensure a complete verification process and more importantly, achieve more accurate and intuitive results.

Citation Keyhu_formal_2019