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

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Wed Jun 1 11:13:34 BST 2022


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

--- Comment #29 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Jacob Lifshay from comment #28)

> Please don't, it's useful too. we can choose to have both UserValue and
> ValueCastable, they're useful for different things.

unfortunately ValueCastable causes major showstopping problems.

> > this was
> > touted as a "feature" but it's a serious problem when adding the
> > up-casting we discussed a few months back.
> 
> that's because ValueCastable is the wrong tool for that job [1]. 

the problem is that ValueCastable fails "isinstance(Value)" as well as base
class chain inheritance detection. upcasting critically relies on detecting
the highest inherited class, and casting all objects specifically to that
type.

the fact that ValueCastable derivatives may be mixed with UserValue derivatives
makes it impossible to establish the up-casting chain and consequently
ValueCastable has to go.

if you can come up with an upcasting function which guarantees that an
arbitrary
list of objects that are of multiple inheritance types from *both* UserValue
*and* ValueCastable across *multiple third party libraries* then it can stay.
no, throwing an exception if a mix is detected is not acceptable because the
up-casting function must cope with arbitrary mixed third party objects.

> [1] assuming you want simd values to be nmigen Values -- i strongly
> disagree, but we can argue about that some other time.

sorry to have to say this, but tough. i know full well that you want a total
duplication of the entire ast.py source code: i have already explained multiple
times that that is a maintenance nightmare, is utterly unnecessary, and even
worse than that it implies that there exists an API difference when there is
absolutely none at all in any way shape or form. please re-read the RFC if you
are not familiar with the logical reasoning.

> > 
> > 
> > > I also merged the CI additions into the smtlib2-expr-support branch and
> > > adjusted .gitlab-ci.yml to use our yosys 0.13 fork with the $smtlib2_expr
> > > support.
> > 
> > brilliant
> > 
> > > CI for yosys master fails because $smtlib2_expr isn't yet merged.
> > 
> > nice to have something keeping an eye on when that occurs
> 
> I'm subscribed to the github PR(s), so can easily keep track of that. I'll
> most likely put a comment here and/or on the nmigen PR when the github PR is
> merged.

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


More information about the libre-soc-bugs mailing list