pono
HWMCC’24
Pono は、C++ で実装された、パフォーマンスが高く、適応性があり、拡張可能な SMT ベースのモデル チェッカーです。 SMT 解決用の汎用 C++ API である Smt-Switch を利用します。 Pono は次世代 CoSA として開発されたため、当初はcosa2と名付けられました。
ポノとはハワイ語で適切、正しい、善良さを意味します。これは口語的に「善」または「正しさ」という道徳的な意味で使用されることが多いですが、「適切な手順」または「正しさ」を指すこともあります。私たちはこの言葉を複数の意味で使用します。私たちの目標は、人々がシステムの正しさを検証するための有用なツールとして Pono を提供することであり、それは確かに正しいことです。
Pono は、全体で最も多くのベンチマークを解決したことにより、HWMCC'19 で元の名前cosa2で Oski Award を受賞しました。
./contrib/setup-bison.shおよび./contrib/setup-flex.shを実行します。-lyをロードできないというエラーが発生する可能性があります。このような場合は、bison セットアップ スクリプトを実行します。./contrib/setup-smt-switch.shを実行します -- Bitwuzla を使用して smt-switch をビルドします./deps/mathsatに変更します。--with-msatフラグをsetup-smt-switch.shコマンドに追加します。./contrib/setup-btor2tools.shを実行します。./configure.shを実行します。configure.shのオプションとして--with-msatも含めますcd build実行します。make実行します。libgmp-staticインストールすることで修正できます。gperftools ライブラリにリンクしてプロファイリング データを生成します。プロファイリングを有効にするには、フラグ--with-profilingを指定して./configure.shを実行し、 buildディレクトリでmakeを実行して Pono を再コンパイルします。これは、前に gperftools ライブラリをインストールしていることを前提としています。たとえば、Ubuntu でsudo apt-get install google-perftools libgoogle-perftools-dev実行します。
プロファイリングするには、 ./pono --profiling-log=<log-file> ...を実行します。 <log-file>は、プロファイリング データが書き込まれるファイルへのパスです。 Pono の正常終了または異常終了 (シグナル送信など) 後、収集されたプロファイル データは、たとえばgoogle-pprof --text ./pono <log-file>を実行することで分析され、テキスト プロファイルが生成されます。その他のオプションについては、 man google-pprofを参照してください。
一般に、gperftools の詳細については、https://github.com/gperftools/gperftools/tree/master/docs を参照してください。
gperftools は BSD 3 条項ライセンスに基づいてライセンスされています。https://github.com/gperftools/gperftools/blob/master/COPYING を参照してください。
移行システム インターフェイスには 2 つあります。
Smt-switch は、SMT ソルバー用の C++ ソルバーに依存しない API です。覚えておくべき重要なことは、すべてはポインターであるということです。オブジェクトはusingステートメントで「typedef 化」されている可能性がありますが、それでもshared_ptrです。したがって、ソルバーまたは項を使用する場合は、 ->アクセスを使用する必要があります。
詳細については、smt-switch テストでの使用例を参照してください。他にアクセスすると便利なファイルは次のとおりです。
smt-switch/include/solver.h : これは、使用するメインインターフェイスです。smt-switch/include/ops.h : これには必要なすべての ops が含まれていますOp(Extract, 7, 4)のようなインデックス付き操作を作成します。 pono Python バインディングを構築するには、まず Cython バージョン 0.29 以上がインストールされていることを確認してください。次に、 smt-switchとその Python バインディングがインストールされていることを確認します。最後に、 ./configure.sh --pythonを使用して設定し、通常どおりビルドします。コマンドのシーケンスは次のようになります。
# Optional recommended step: start a python virtualenv
# If you install in the virtualenv, you will need to activate it each time before using pono
# and deactivate the virtualenv with: deactivate
python3 -m venv env
source ./env/bin/activate
pip install Cython==0.29 pytest
./contrib/setup-smt-switch.sh --python
./contrib/setup-btor2tools.sh
pip install -e ./deps/smt-switch/build/python
./configure.sh --python
cd build
make -j4
pip install -e ./python
cd ../
# Test the bindings
pytest ./tests
Verilog から BTOR2 を作成するための最適なツールは Yosys です。 Yosys には素晴らしいマニュアルがあります。引数なしで yosys を実行することで、yosys を対話的に実行することもできます。その後、 help <command>を使用して各コマンドのヘルプ メッセージを表示できます。引数を指定せずにhelp実行すると、すべてのコマンドがリストされます。
問題が発生した場合に特に便利なコマンドはshowです。これは、Yosys の回線の現在の状態を表示できます。
以下は、./samples/counter-false.v の BTOR2 ファイルを生成する各コマンドを説明するコメント付きのサンプル ファイルです。ほとんどのユースケースではこれで十分です。
yosysインストールしたら、以下のテキストをこのリポジトリの最上位にあるgen-btor.ysにコピーします。次に、 yosys -s gen-btor.ys実行すると、BTOR2 ファイルが生成されます。
# read in the file(s) -- there can be multiple
# whitespace separated files, and you can
# escape new lines if necessary
read -formal ./samples/counter-false.v;
# prep does a conservative elaboration
# of the top module provided
prep -top counter;
# this command just does a sanity check
# of the hierarchy
hierarchy -check;
# If an assumption is flopped, you might
# see strange behavior at the last state
# (because the clock hasn't toggled)
# this command ensures that assumptions
# hold at every state
chformal -assume -early;
# this processes memories
# nomap means it will keep them as arrays
memory -nomap;
# flatten the design hierarchy
flatten;
# (optional) uncomment and set values to simulate reset signal
# use -resetn for an active low pin
# -n configures the number of cycles to simulate
# -rstlen configures how long the reset is active (recommended to keep it active for the whole simulation)
# -w tells it to write back the final state of the simulation as the initial state in the btor2 file
# another useful option is -zinit which zero initializes any uninitialized state
# sim -clock <clockpin> -reset <resetpin> -n <number of cycles> -rstlen <number of cycles> -w <top_module>
# (optional) use an "explicit" clock
# e.g. every state is a half cycle of the
# fastest clock
# use this option if you see errors that
# refer to "adff" or asynchronous components
# IMPORTANT NOTE: the clocks are not
# automatically toggled if you use this option
# clk2fflogic;
# This turns all undriven signals into
# inputs
setundef -undriven -expose;
# This writes to a file in BTOR2 format
write_btor counter-false.btor2
