私はYosysの正式な検証機能をVerificarパーサーとともに使用しようとしています。正式なyosysの正式な機能とは何ですか？
「read_verilog -formal」コマンドと比較して、正式な検証に有効なyosysのサポートされている機能は何ですか？ は、例えば、read_verilogで動作する正式なコードの迅速なコンパイルが構文「プロパティを想定して」の私にエラーを与えた： 「SVAディレクティブは、クロックに敏感ではない非クロックディレクティブがサポートされていません。」私は
をVerificライブラリのフラグを何らかの形で変更してより多くの機能をサポートする必要があるかどうか、またはサポートされていないものがあるかどうかは不明です。
現在、YosysはVerificの有無にかかわらず、SVAのサポートは非常に限られています。しかし、私たちは近い将来、SVAのYosysサポートをVerific経由で大幅に拡張する予定です。目標は、Verificが解析できるすべてのものをほぼ完全にサポートすることです。
「svaディレクティブは時計には影響されません。ロックされていないディレクティブはサポートされていません」というエラーメッセージ：これはVerificyエラーメッセージで、それをバイパスするVerificライブラリフラグはありません。 （しかし、わかりません）技術的にロックされていないプロパティは、SystemVerilog標準afaikの一部ではありません。 （構文はそれを可能にしますが、標準テキストではその意味を定義しません）
Yosysは、クローンのないSVAプロパティをサポートしています。 （しかし、些細な表現のプロパティだけです。）
VerificとYosysは、直接のアサーションと前提をサポートしています。これは、ほとんどのシミュレータが即時アサーションをサポートしているためです（あるいは、サポートが必要な場合は追加する方が簡単かもしれません）。これまでに欠けている）。
今は、YosysでVerificを使用する最大の利点は、SVA以外のシステムVerilog（およびVHDL）コードをサポートすることです。数ヵ月後には、Verificを介してさらに多くのSVA構成をサポートしていきたいと考えていますが、まだ実装されていません。
編集/更新： Verificを経由したSVAのサポートは、現在改善が遅いです。 Verific経由で処理できる例については、this directoryを参照してください。新しい機能がVerificyバインディングに追加されると、新しい例が追加されます。現在のところ、counter.svが最も高度な例です。
ありがとうございました。 正式な検証にはVerifとどのようなコンパイルフラグを使用しますか？ また、FV用に推奨されるyosysスクリプトをverificentで投稿することは可能ですか？ 私は、データベースを書かれたRTLと大きく異なるものにするいくつかの操作を実行していると思います。 – EEliaz
@EEliaz私は 'frontends/verific /'に 'example.sv'と' example.sby'を追加しました：https://github.com/cliffordwolf/yosys/tree/master/frontends/verific – CliffordVienna
@EEliaz私の答えに編集を参照してください。 Verificを介したSVAのサポートは徐々に向上しています。 tests/sva /のサンプルを参照してください。 – CliffordVienna