我們可以使用JasperGold做功能驗證嗎？

Question

任何人都可以告訴我如何使用JasperGold進行功能驗證嗎？ 我是這個工具的新手。

Answer 1

JasperGold是一個正式的驗證工具。功能驗證通常使用仿真和功能覆蓋進行。

正式工具的輸入是你的設計加上一套ASSUME屬性。 ASSUME屬性通常會限制輸入激勵的合法範圍。給定輸入的正式工具可以證明其他屬性。

E.g.如果你的設計是一個完整的加法器，並且設置了輸入介於0和5之間的ASSUME屬性，那麼形式也應該能夠證明輸出始終在0和10之間。它還應該能夠證明輸出是總是等於輸入的總和。這最後一個屬性可以被看作是「功能驗證」。你已經驗證你的HDL代碼和你的財產在功能上是平等的。

Answer 2

是的，您可以使用JasperGold進行功能驗證。 JasperGold是一個正式的財產檢查工具。

功能驗證是驗證設計功能的過程。傳統模擬（定向或隨機）可用於執行功能驗證。正式的財產檢查工具執行功能驗證。還有正式的等價性檢查工具（如Synopsys的Hector）進行功能驗證。

有一些正式的工具，不執行功能驗證。例如Formality。

要使用JasperGold，您需要使用屬性檢查語言來創建合適的屬性。 SystemVerilog斷言（或SVA）現在是行業標準。您可以從Internet上下載（令人驚訝的可讀）SystemVerilog LRM。