A Study and Survey on Formal Verification Methods for Validating and Verifying the Specifications of Digital Systems

確認與驗證數位系統之正規驗證方法之研究與綜覽

陳聰明

《萬能學報》 33期 (2011/07) Pp. 281-304

https://doi.org/10.29679/VJ.201107.0021

摘要

在定義一數位系統時，定義其功能性規格在整個設計週期中，乃是一重要里程碑。因為此時並無任何精確之文件可供驗證，且此階段有許多的工程設計判斷及取捨待做，因而極易有人為錯誤引入。如果在此階段，發生了設計錯誤，卻未及早發現，則其累積的代價將極高，可能高達兩百倍之鉅。本論文主要綜覽在此階段之定理證明與模型核對等正規驗證方法，分析其優劣點，因而可對定理證明與模型核對正規驗證方法，獲致適當之初步透視；並以此為出發點，研究出更有效之方法來做功能性規格確認。

關鍵字

設計確認與驗證 ； 功能性規格 ； 正規方法 ； 定理證明 ； 模型核對 ； 機器等效 ； 語言涵蘊 ； 狀態發掘

並列摘要

In designing a digital system, defining the functional specification represents the first corner stone in the whole design life cycle. Since there is not anything precise to verify against and a lot of engineering judgments and tradeoffs are involved in it, it is relatively easy to introduce design errors in it. Furthermore, if a design error occurs in this stage and is not captured earlier enough, then its accumulated effect in the following process could mean 200 times more costly than if found earlier. In this paper, the author surveys various formal methods reported by some researchers in their studies, analyzes their strengths and weakness, in order to gain some insights into this important problem and to set out finding more effective methods to validate system functional specifications. Finally, the author addresses possible future developments of design verification and validation methods for digital systems, and comes to a conclusion that a hybrid method will be necessary as a common practice in doing the validation and verification of the specifications of digital systems.

並列關鍵字

design validation and verification ； functional specification ； formal methods ； theorem proving ； model checking ； machine equivalence ； language containment ； state exploration

參考文獻

Windley, Philips J. (1990), “The Formal Verification of Generic Interpreters”, Ph.D. Thesis, Department of Computer Science, University of California, Davis

McFarland, Michael C.(1993), “Formal Verification of Sequential Hardware: A Tutorial”, IEEE Transactions on Computer-aided Design of Integrated Circuits and Systems, 12(5), 633-651

Rushby, John(1995), “Formal Methods and Their Role in the Certification of Critical Systems”, Technical Report CSL-95-1, Computer Science Laboratory, SRI International, Menlo Park, CA 94025, 19-21

Aarti Gupta, Aarti(1992), “Formal Hardware Verification Methods: A Survey”, in “Forma Methods in System Design”, Kluwer Academic Publishers

Joan J. Britt, Joan(1994), “Case study: Applying formal methods to the Traffic Alert and Collision Avoidance System (TCASII)”, Proceedings of Annual Computer Assurance Conference, 39-51