適用於微處理器相容性驗證之加強型自動程式產生器及其涵蓋率分析

Abstract

自動驗證程式產生器可用於自動產生大量的驗證程式。它已經成為驗證新設計微處理器相容性的重要工具。在這篇論文中，我們要改進並且加強一個現有自動驗證程式產生器的功能。此自動驗證程式產生器是以基於規則的方法，來產生事件導向的驗證程式。我們提出兩個機制:資源配置與迴圈產生。資源配置機制主要是記錄暫存器與記憶體的使用。經由公平的資源配置，我們可以產生指令序以驗證微處理器的核心設計，如複雜的記憶體管理單元。迴圈產生機制則提供一個具有彈性的方式去產生沒有無窮迴圈的迴圈區塊。這些機制使此事件導向的自動驗證程式產生器的功能更為完全，並且加強其功能以產生更符合驗證需求的驗證程式。我們可以產生包含各種不同指令組合的驗證程式，如迴圈區塊與資料相依區塊。自動驗證程式產生器經由涵蓋分析工具的引導，可以產生涵蓋率較高的驗證程式 。實驗結果顯示可以提升驗證涵蓋率20% (其中一例)。這也就是說新產生的驗證程式可以驗證相同的系統狀態，但是其程式是由涵蓋率較高的指令序所組成。經由我們的加強機制，驗證程式的產生變為更專精與精巧。因此我們的新自動驗證程式產生器可以讓微處理器相容性的驗證變得更系統化，並可加快其上市時間。

An AVPG (Automatic Verification Program Generator) intends to generate a large number of verification programs automatically. It has become an important tool to verify the design and compatibility of a new microprocessor. In this thesis, we improve and enhance an existing AVPG. The AVPG is based on a rule-based methodology that is used to generate event-driven verification programs. We propose two mechanisms: resource allocation and loop generation. The resource allocation mechanism traces the usage of registers and memory. Through fair resource allocation, we can generate instruction sequences to verify the kernel designs in a microprocessor, such as a complex memory management unit. The loop generation mechanism provides a flexible way to control the generation of loop blocks without infinite loops. These mechanisms complete the event-driven AVPG and enhance its capability to generate verification programs that can fit into verification needs. We can generate verification programs that contain different combinations of instruction sequences, such as loop blocks and data dependency blocks. By refining the AVPG based on the coverage analysis, experimental results show that it can increase the verification coverage by 20% for an example. That is, the generated verification programs can verify the same system state, but they are constructed by instruction sequences with high verification coverage. Through our enhanced mechanisms, the generation of verification programs becomes more dedicated and sophisticated. Therefore, our new AVPG can make the verification of compatible microprocessors more systematic and achieve higher time to market efficiency.