本文檔的主要內(nèi)容詳細(xì)介紹的是可綜合的Verilog語(yǔ)法和語(yǔ)義詳細(xì)資料說(shuō)明。

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

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

　　不同的工具對(duì)Verilog有不同的解釋：像Cadence的verilogxl這樣的行業(yè)標(biāo)準(zhǔn)模擬器是基于事件調(diào)度的。合成器和周期模擬器基于不太詳細(xì)的時(shí)鐘寄存器傳輸級(jí)（RTL）語(yǔ)義。

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

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

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

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

　　除了確定Verilog文本之間的等價(jià)性這一直接目標(biāo)外，顯式語(yǔ)義還提供了一個(gè)標(biāo)準(zhǔn)，以確保不同的工具（例如模擬器和合成器）對(duì)語(yǔ)言結(jié)構(gòu)有一致的解釋。

　　下面列出了V0中遺漏的可合成Verilog的一些特性。考慮這些省略的特征可能會(huì)破壞這里給出的語(yǔ)義學(xué)風(fēng)格。
?