pono
HWMCC’24
Pono عبارة عن مدقق نماذج فعال وقابل للتكيف وقابل للتوسيع يعتمد على SMT ويتم تنفيذه في C++. إنه يستفيد من Smt-Switch، وهو واجهة برمجة تطبيقات C++ عامة لحل SMT. تم تطوير Pono باعتباره الجيل التالي من CoSA وبالتالي تم تسميته في الأصل بـ cosa2 .
بونو هي كلمة هاواي تعني الصحيح أو الصحيح أو الخير. غالبًا ما يتم استخدامه بالعامية بالمعنى الأخلاقي لـ "الخير" أو "الصواب"، ولكنه يشير أيضًا إلى "الإجراء المناسب" أو "الصواب". نستخدم الكلمة لمعاني متعددة. هدفنا هو أن يكون Pono أداة مفيدة للأشخاص للتحقق من صحة الأنظمة، وهو بالتأكيد الشيء الصحيح الذي يجب القيام به.
حصل Pono على جائزة Oski تحت اسمه الأصلي cosa2 في HWMCC'19 لحل أكبر عدد من المعايير بشكل عام.
./contrib/setup-bison.sh و ./contrib/setup-flex.sh-ly . في مثل هذه الحالة، قم بتشغيل البرنامج النصي لإعداد البيسون../contrib/setup-smt-switch.sh - سيقوم بإنشاء smt-switch باستخدام Bitwuzla./deps/mathsat--with-msat إلى أمر setup-smt-switch.sh ../contrib/setup-btor2tools.sh ../configure.sh .--with-msat كخيار ل configure.shcd build .make .libgmp-static من AUR. نحن نربط مكتبة gperftools لإنشاء بيانات ملفات التعريف. لتمكين التوصيف، قم بتشغيل ./configure.sh مع العلامة --with-profiling وأعد ترجمة Pono عن طريق تشغيل make في دليل build . يفترض هذا أنك قمت بتثبيت مكتبة 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 لمزيد من الخيارات.
بشكل عام، راجع https://github.com/gperftools/gperftools/tree/master/docs لمزيد من المعلومات حول gperftools.
تم ترخيص gperftools بموجب ترخيص BSD المكون من 3 فقرات، راجع https://github.com/gperftools/gperftools/blob/master/COPYING.
هناك نوعان من واجهات النظام الانتقالي:
Smt-switch عبارة عن واجهة برمجة التطبيقات (API) غير المعتمدة على حل C++ لحلول SMT. الشيء الرئيسي الذي يجب أن تتذكره هو أن كل شيء هو مؤشر. قد تكون الكائنات "typedef-ed" using العبارات، لكنها تظل shared_ptr s. وبالتالي، عند استخدام حل أو مصطلح، تحتاج إلى استخدام -> الوصول.
لمزيد من المعلومات، راجع مثال الاستخدام في اختبارات 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
أفضل أداة لإنشاء BTOR2 من Verilog هي Yosys. Yosys لديه دليل ممتاز هنا. يمكنك أيضًا تشغيل yosys بشكل تفاعلي عن طريق تشغيل yosys بدون وسائط. ثم يمكنك عرض رسائل المساعدة لكل أمر باستخدام: help <command> . يؤدي تشغيل help بدون وسيطات إلى سرد كافة الأوامر.
الأمر المفيد بشكل خاص إذا كنت تواجه مشكلة هو show ، والذي يمكنه إظهار الحالة الحالية للدائرة في Yosys.
يوجد أدناه ملف مثال يحتوي على تعليقات تشرح كل أمر ينتج ملف BTOR2 لـ ./samples/counter-false.v. يجب أن يكون هذا كافيًا لمعظم حالات الاستخدام.
بمجرد تثبيت 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
