Formal compliance verification of interface protocols

Ya Ching Yang; Juinn Dar Huang; Chia Chih Yen; Che Hua Shih; Jing Yang Jou

doi:10.1109/VDAT.2005.1500007

Formal compliance verification of interface protocols

Ya Ching Yang, Juinn Dar Huang, Chia Chih Yen, Che Hua Shih, Jing Yang Jou

Department of Electrical Engineering

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

7 Scopus citations

Abstract

Verifying whether a building block conforms to certain interface protocol is one of the important steps while constructing an SoC. However, most existing methods have their own limitations. Simulation-based methods have the false positive problem while formal property checking methods may suffer from memory explosion and excessive runtime. In this paper, we propose a novel branch-and-bound algorithm for interface protocol compliance verification. The properties of the interface protocol are specified as a specification FSM, and the interface logic is formally verified at the higher FSM level. Using the FSM for property specification is relatively systematic than using other proprietary property languages, which greatly reduces the possibility of incomplete property identification. And it is shown theoretically and experimentally that the proposed algorithm can finish in reasonable time complexity.

Original language	English
Title of host publication	2005 IEEE VLSI-TSA International Symposium on VLSI Design, Automation and Test,(VLSI-TSA-DAT)
Pages	12-15
Number of pages	4
DOIs	https://doi.org/10.1109/VDAT.2005.1500007
State	Published - 2005
Event	2005 IEEE VLSI-TSA International Symposium on VLSI Design, Automation and Test,(VLSI-TSA-DAT) - Hsinchu, Taiwan Duration: 27 Apr 2005 → 29 Apr 2005

Publication series

Name	2005 IEEE VLSI-TSA International Symposium on VLSI Design, Automation and Test,(VLSI-TSA-DAT)
Volume	2005

Conference

Conference	2005 IEEE VLSI-TSA International Symposium on VLSI Design, Automation and Test,(VLSI-TSA-DAT)
Country/Territory	Taiwan
City	Hsinchu
Period	27/04/05 → 29/04/05

Access to Document

10.1109/VDAT.2005.1500007

Cite this

Yang, Y. C., Huang, J. D., Yen, C. C., Shih, C. H., & Jou, J. Y. (2005). Formal compliance verification of interface protocols. In 2005 IEEE VLSI-TSA International Symposium on VLSI Design, Automation and Test,(VLSI-TSA-DAT) (pp. 12-15). Article 1500007 (2005 IEEE VLSI-TSA International Symposium on VLSI Design, Automation and Test,(VLSI-TSA-DAT); Vol. 2005). https://doi.org/10.1109/VDAT.2005.1500007

@inproceedings{2c69a21f16c94d8e89a8d04618e794fc,

title = "Formal compliance verification of interface protocols",

abstract = "Verifying whether a building block conforms to certain interface protocol is one of the important steps while constructing an SoC. However, most existing methods have their own limitations. Simulation-based methods have the false positive problem while formal property checking methods may suffer from memory explosion and excessive runtime. In this paper, we propose a novel branch-and-bound algorithm for interface protocol compliance verification. The properties of the interface protocol are specified as a specification FSM, and the interface logic is formally verified at the higher FSM level. Using the FSM for property specification is relatively systematic than using other proprietary property languages, which greatly reduces the possibility of incomplete property identification. And it is shown theoretically and experimentally that the proposed algorithm can finish in reasonable time complexity.",

author = "Yang, {Ya Ching} and Huang, {Juinn Dar} and Yen, {Chia Chih} and Shih, {Che Hua} and Jou, {Jing Yang}",

year = "2005",

doi = "10.1109/VDAT.2005.1500007",

language = "???core.languages.en_GB???",

isbn = "0780390601",

series = "2005 IEEE VLSI-TSA International Symposium on VLSI Design, Automation and Test,(VLSI-TSA-DAT)",

pages = "12--15",

booktitle = "2005 IEEE VLSI-TSA International Symposium on VLSI Design, Automation and Test,(VLSI-TSA-DAT)",

note = "2005 IEEE VLSI-TSA International Symposium on VLSI Design, Automation and Test,(VLSI-TSA-DAT) ; Conference date: 27-04-2005 Through 29-04-2005",

}

Yang, YC, Huang, JD, Yen, CC, Shih, CH & Jou, JY 2005, Formal compliance verification of interface protocols. in 2005 IEEE VLSI-TSA International Symposium on VLSI Design, Automation and Test,(VLSI-TSA-DAT)., 1500007, 2005 IEEE VLSI-TSA International Symposium on VLSI Design, Automation and Test,(VLSI-TSA-DAT), vol. 2005, pp. 12-15, 2005 IEEE VLSI-TSA International Symposium on VLSI Design, Automation and Test,(VLSI-TSA-DAT), Hsinchu, Taiwan, 27/04/05. https://doi.org/10.1109/VDAT.2005.1500007

Formal compliance verification of interface protocols. / Yang, Ya Ching; Huang, Juinn Dar; Yen, Chia Chih et al.
2005 IEEE VLSI-TSA International Symposium on VLSI Design, Automation and Test,(VLSI-TSA-DAT). 2005. p. 12-15 1500007 (2005 IEEE VLSI-TSA International Symposium on VLSI Design, Automation and Test,(VLSI-TSA-DAT); Vol. 2005).

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

TY - GEN

T1 - Formal compliance verification of interface protocols

AU - Yang, Ya Ching

AU - Huang, Juinn Dar

AU - Yen, Chia Chih

AU - Shih, Che Hua

AU - Jou, Jing Yang

PY - 2005

Y1 - 2005

N2 - Verifying whether a building block conforms to certain interface protocol is one of the important steps while constructing an SoC. However, most existing methods have their own limitations. Simulation-based methods have the false positive problem while formal property checking methods may suffer from memory explosion and excessive runtime. In this paper, we propose a novel branch-and-bound algorithm for interface protocol compliance verification. The properties of the interface protocol are specified as a specification FSM, and the interface logic is formally verified at the higher FSM level. Using the FSM for property specification is relatively systematic than using other proprietary property languages, which greatly reduces the possibility of incomplete property identification. And it is shown theoretically and experimentally that the proposed algorithm can finish in reasonable time complexity.

AB - Verifying whether a building block conforms to certain interface protocol is one of the important steps while constructing an SoC. However, most existing methods have their own limitations. Simulation-based methods have the false positive problem while formal property checking methods may suffer from memory explosion and excessive runtime. In this paper, we propose a novel branch-and-bound algorithm for interface protocol compliance verification. The properties of the interface protocol are specified as a specification FSM, and the interface logic is formally verified at the higher FSM level. Using the FSM for property specification is relatively systematic than using other proprietary property languages, which greatly reduces the possibility of incomplete property identification. And it is shown theoretically and experimentally that the proposed algorithm can finish in reasonable time complexity.

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

U2 - 10.1109/VDAT.2005.1500007

DO - 10.1109/VDAT.2005.1500007

M3 - 會議論文篇章

AN - SCOPUS:33745446679

SN - 0780390601

SN - 9780780390607

T3 - 2005 IEEE VLSI-TSA International Symposium on VLSI Design, Automation and Test,(VLSI-TSA-DAT)

SP - 12

EP - 15

BT - 2005 IEEE VLSI-TSA International Symposium on VLSI Design, Automation and Test,(VLSI-TSA-DAT)

T2 - 2005 IEEE VLSI-TSA International Symposium on VLSI Design, Automation and Test,(VLSI-TSA-DAT)

Y2 - 27 April 2005 through 29 April 2005

ER -

Formal compliance verification of interface protocols

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this