pono
HWMCC’24
Pono เป็นตัวตรวจสอบโมเดลที่ใช้ SMT ที่มีประสิทธิภาพ ปรับเปลี่ยนได้ และขยายได้ ซึ่งใช้งานใน C++ มันใช้ประโยชน์จาก Smt-Switch ซึ่งเป็น C++ API ทั่วไปสำหรับการแก้ปัญหา SMT Pono ได้รับการพัฒนาให้เป็น CoSA รุ่นต่อไป และเดิมมีชื่อว่า cosa2
Pono เป็นคำภาษาฮาวายที่หมายถึง เหมาะสม ถูกต้อง หรือความดี มักใช้เรียกขานในแง่ศีลธรรมของ "ความดี" หรือ "ความถูกต้อง" แต่ยังหมายถึง "ขั้นตอนที่เหมาะสม" หรือ "ความถูกต้อง" เราใช้คำได้หลายความหมาย เป้าหมายของเราคือ Pono สามารถเป็นเครื่องมือที่มีประโยชน์สำหรับผู้คนในการตรวจสอบ ความถูกต้อง ของระบบ ซึ่งเป็นสิ่งที่ ถูกต้อง ที่ต้องทำอย่างแน่นอน
Pono ได้รับรางวัล Oski Award ภายใต้ชื่อเดิม 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.sh ด้วยcd buildmake .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-clause ดู https://github.com/gperftools/gperftools/blob/master/COPYING
มีอินเทอร์เฟซ Transition System สองแบบ:
Smt-switch เป็น API ของผู้ไม่เชื่อเรื่องพระเจ้า C++ สำหรับตัวแก้ปัญหา SMT สิ่งสำคัญที่ต้องจำคือทุกอย่างเป็นตัวชี้ วัตถุอาจเป็น "typedef-ed" โดย using คำสั่ง แต่ยังคงเป็น shared_ptr s ดังนั้น เมื่อใช้ตัวแก้ปัญหาหรือคำศัพท์ คุณต้องใช้ -> การเข้าถึง
สำหรับข้อมูลเพิ่มเติม โปรดดูตัวอย่างการใช้งานในการทดสอบสวิตช์ smt ไฟล์ที่มีประโยชน์อื่นๆ ที่ควรเข้าชม ได้แก่:
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
เครื่องมือที่ดีที่สุดสำหรับการสร้าง 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
