我試圖使用Yosys正式驗證功能以及Verific解析器。yosys具有驗證功能的正式功能是什麼？
與「read_verilog -formal」命令相比，yosys具有用於形式驗證的驗證功能的支持功能是什麼？ 例如，正式的代碼快速編譯與read_verilog的作品給了我一個錯誤「承擔財產」語法： 「上廣電指令不是時鐘敏感的使用時鐘指令不被支持。」
我不確定我是否應該以任何方式修改Verific庫標誌以使其支持更多功能，或者它不受支持。
目前Yosys只有非常有限的SVA支持，無論是否爲Verific。不過，我們計劃在不久的將來通過Verific大大擴展Yosys對SVA的支持。目標是爲Verific可以解析的所有內容提供非常全面的支持。
關於「sva指令對時鐘不敏感，不支持非指令指令」錯誤消息：這是一個驗證錯誤消息，我不認爲有一個驗證庫標誌可繞過它。 （但我不確定。）技術上的非時鐘屬性不是SystemVerilog標準afaik的一部分。 （語法允許，但標準文本沒有爲它定義語義。）
Yosys支持非時鐘的SVA屬性。 （但只有微不足道的表達性質。）
Verific和Yosys確實支持即時斷言和假設。 （這是斷言和假設的總是塊）現在，這是我推薦的大多數情況下，人們寫新的屬性，也因爲大多數模擬器有更好的立即斷言支持（或者如果支持是更容易添加迄今爲止缺失）。
現在我想說的是，與Yosys一起使用Verific的最大優勢是支持非SVA系統Verilog（和VHDL）代碼。在幾個月內，我們希望能夠通過Verific支持更多的SVA結構，但那還沒有實現。
編輯/更新：通過驗證的SVA支持現在緩慢改善。有關可通過Verific處理的示例，請參見this directory。新特性添加到Verific綁定中時添加新示例。目前counter.sv是最先進的例子。
謝謝你的回答。 Verific使用什麼編譯標誌進行正式驗證？ 另外，是否可以發佈一個推薦的用於FV的yosys腳本進行驗證？ 我想我正在運行一些操作，這些操作使數據庫與寫入的RTL有很大的不同。 – EEliaz
@EEliaz我現在添加了'example.sv'和'example.sby'到'frontends/verific /'：https：//github.com/cliffordwolf/yosys/tree/master/frontends/verific – CliffordVienna
@EEliaz請參閱編輯我的答案。通過Verific的SVA支持正在慢慢改善。請參閱tests/sva /中的示例。 – CliffordVienna