CoSA

CoSA copied to clipboard

Enhancement Idea: Use Yosys through Python API

2

Yosys now has a Python API using `boost_python`. Enable it with: `sudo make install ENABLE_PYOSYS=1 ENABLE_LIBYOSYS=1` We can use this to encode the Verilog directly from RTLIL instead of going...

makaimann

This would restructure the BTOR encoder to use a dictionary look-up for each function, instead of a sequence of `if`s. Furthermore, it lazily casts between `bool` and `BV(1)` with a...

makaimann

makaimann

Just a reminder for me to address this when there’s time. It would be nice if parsing errors gave a line number. Especially for STS/ETS files. This might be harder...

makaimann

This also causes a bug in for loops with the condition (i >= 0) because everything defaults to unsigned comparisons.

makaimann