可綜合的Verilog語法和語義詳細資料說明

本文檔的主要內容詳細介紹的是可綜合的Verilog語法和語義詳細資料說明。

　　可合成Verilog是Verilog HDL的一個子集，它位于當前合成工具（RTL和行為）的領域內。本文檔指定了Verilog的一個子集V0.1。該子集旨在作為思想快速原型化的工具。

　　開發(fā)所有可綜合Verilog的語義所選擇的方法是從過于簡單的{V0{開始，然后在簡單的語義中斷時使其更加復雜。這樣可以避免不必要的復雜性。計劃對越來越大的子集（V1、V2等）進行重新排序，這些子集將收斂到劍橋VFE project2中使用的Verilog版本。

　　不同的工具對Verilog有不同的解釋：像Cadence的verilogxl這樣的行業(yè)標準模擬器是基于事件調度的。合成器和周期模擬器基于不太詳細的時鐘寄存器傳輸級（RTL）語義。

　　有必要為Verilog提供一個明確的語義，為確定行為原型與綜合邏輯之間的等價性提供依據。Verilog的正常語義是基于事件的，即電線和寄存器中值的變化。這種事件策略可以精確地建模詳細的異步行為，但粒度非常小，不容易支持形式化驗證。大多數實用的形式化方法（如模型檢驗和定理證明）都是根據系統的執(zhí)行軌跡來描述系統的狀態(tài)序列（或樹）?？梢詫⒛M語義描述為“面向邊”，將跟蹤語義描述為“面向級別”。這兩個視圖之間的關系是通過在模擬周期中累積更改（事件）來獲得在周期結束時保持的狀態(tài)。

　　在模擬時間的連續(xù)時刻，模擬周期靜止到的狀態(tài)序列將被稱為模擬跟蹤語義或僅僅是跟蹤語義。如果存在競態(tài)條件，則給定狀態(tài)可能存在多個可能的后繼狀態(tài)，因此需要一棵樹來準確描述事件語義（即分支時間）。然而，標準硬件合成方法創(chuàng)建了確定性時序機，其執(zhí)行可以用線性描述蹤跡。因此，這里提供給Verilog的跟蹤語義將由序列而不是樹組成。我們的部分目標是提供足夠的語法條件來保證線性跟蹤語義與事件語義等價。滿足這些條件的Verilog合成的硬件將模擬源代碼。

　　跟蹤語義與事件（模擬）語義（即模擬時間）具有相同的時間標度，但在單個模擬周期（增量時間）內從單個事件中抽象出來。時鐘順序系統也可以更抽象地根據連續(xù)過程中寄存器中的狀態(tài)序列來查看時鐘周期。這種觀點將被稱為時鐘周期語義或僅僅是周期語義。3如果只考慮鎖存在時鐘邊緣的狀態(tài)，某些類型的硬件（例如透明電平敏感鎖存器）的近似性相當差，因此最好使用跟蹤語義來實現這些硬件之間的等價性。

　　在VFE項目中，ne粒度等價將被表示為跟蹤語義，而粗粒度等價將被表示為循環(huán)語義。它還打算研究eHavour級別上更松散的等價關系，在eHavour級別上，操作可以跨時鐘周期序列移動（例如，在相同的“超級狀態(tài)”中）

　　除了確定Verilog文本之間的等價性這一直接目標外，顯式語義還提供了一個標準，以確保不同的工具（例如模擬器和合成器）對語言結構有一致的解釋。

　　下面列出了V0中遺漏的可合成Verilog的一些特性?？紤]這些省略的特征可能會破壞這里給出的語義學風格。
?