Pono는 C++로 구현된 성능이 뛰어나고 적응력이 뛰어나며 확장 가능한 SMT 기반 모델 검사기입니다. SMT 해결을 위한 일반 C++ API인 Smt-Switch를 활용합니다. Pono는 CoSA의 차세대 버전으로 개발되었기 때문에 원래 이름은 cosa2 였습니다.
포노(Pono)는 올바른, 올바른, 선함을 뜻하는 하와이 단어입니다. 이는 종종 "선함" 또는 "올바름"이라는 도덕적 의미로 구어체로 사용되지만, "적절한 절차" 또는 "올바름"을 의미하기도 합니다. 우리는 이 단어를 다양한 의미로 사용합니다. 우리의 목표는 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
실행하세요.--with-msat
도 configure.sh
옵션으로 포함하세요.cd build
실행합니다.make
실행하세요.libgmp-static
설치하면 문제를 해결할 수 있습니다. 프로파일링 데이터를 생성하기 위해 gperftools 라이브러리에 연결합니다. 프로파일링을 활성화하려면 --with-profiling
플래그와 함께 ./configure.sh
를 실행하고 build
디렉터리에서 make
실행하여 Pono를 다시 컴파일하세요. 이는 예를 들어 Ubuntu에서 sudo apt-get install google-perftools libgoogle-perftools-dev
실행하기 전에 gperftools 라이브러리를 설치했다고 가정합니다.
프로파일링하려면 ./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
파이썬 바인딩을 빌드하려면 먼저 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
실행하면 모든 명령이 나열됩니다.
문제가 있는 경우 특히 유용한 명령은 Yosys 회로의 현재 상태를 표시할 수 있는 show
입니다.
다음은 ./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