pono
HWMCC’24
Pono 是一个用 C++ 实现的高性能、适应性强且可扩展的基于 SMT 的模型检查器。它利用 Smt-Switch，这是一种用于 SMT 解决方案的通用 C++ API。 Pono 是作为下一代 CoSA 开发的，因此最初被命名为cosa2 。
Pono 在夏威夷语中是正确、正确或善良的意思。它经常在口语中用于道德意义上的“善”或“正确”，但也指“适当的程序”或“正确性”。我们使用这个词有多种含义。我们的目标是 Pono 可以成为人们验证系统正确性的有用工具，这无疑是正确的事情。
Pono 在 HWMCC'19 上因其解决了最大数量的基准测试而被授予 Oski 奖（原名cosa2） 。
./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 。--with-msat作为configure.sh的选项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。
有两个过渡系统接口：
Smt-switch 是用于 SMT 求解器的与 C++ 求解器无关的 API。最重要的是要记住，一切都是指针。对象可能是using语句进行“typedef-ed”的，但它们仍然是shared_ptr 。因此，当使用求解器或术语时，您需要使用->访问。
有关更多信息，请参阅 smt-switch 测试中的示例用法。其他需要访问的有用文件包括：
smt-switch/include/solver.h ：这是您将使用的主界面smt-switch/include/ops.h ：这包含您可能需要的所有操作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
