[Libre-soc-bugs] [Bug 835] add support for smtlib2 floating-point to yosys and nmigen

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=835

--- Comment #6 from Jacob Lifshay <programmerjake at gmail.com> ---
I created a repo on gitlab and am pushing my work there in addition to
git.libre-soc.org:
https://gitlab.com/programmerjake/nmigen/-/commits/smtlib2-expr-support

I discovered that nmigen's tests were broken (because lkcl didn't run the tests
when he added *_prst pins to the pin_layout function), and submitted a PR to
fix that:
https://gitlab.com/nmigen/nmigen/-/merge_requests/6

I added smtlib2 floating-point support to nmigen, but didn't add tests yet.

I implemented tests for all supported smtlib2 sorts (smtlib2's name for types)
and for SmtBool's functions.

It works correctly in formal proofs! (though I had to fix yosys-smtbmc's overly
simplistic parser, added to the draft yosys PR)

-- 
You are receiving this mail because:
You are on the CC list for the bug.