使用正規符號模型驗證器的聲明檢驗法

Abstract

以聲明(Assertion)為基礎的驗証法已經成為當今設計驗証法的典範。而聲明是用來檢驗電路功能的,但人們所撰寫的聲明很可能其本身即含有衝突錯誤。在此我們提出一個自動檢查聲明衝突的方法。此方法主要是將輸入的聲明轉化成有限確定自動機(Deterministic Finite Automata)及性質(Property),再利用現有的正規符號模型驗證器(Symbolic Model Verifier)對自動機和性質作交叉驗證, 以檢查出聲明之間的矛盾衝突。藉由此法能幫助聲明撰寫者在早期就自動檢查出聲明的矛盾而不需要等到模擬(Simulation)時才發現。

Assertion based verification (ABV) methodology has emerged as a paradigm of high-level design verification. An assertion is used to specify what is to be exercised and verified against the intended functionality. However assertions which may contain conflicts among themselves are not inspected until later simulation stage.In this thesis, we present an automatic assertion checking which utilizes an existing symbolic model verifier as a model checker to check if there is any conflict among input assertions. We propose an approach to convert the assertions into structural Deterministic Finite Automata (DFA) and their corresponding properties. Those converted DFA and properties are then checked by using formal model verifier. This approach may facilitate assertion checking to find out potential conflict in the early stage of design activities without simulation.