-
Notifications
You must be signed in to change notification settings - Fork 4
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[RFC] The Future of Families #98
Comments
FWIW, in magma we distinguish Bits from UInt based on the definition of arithmetic/comparison operators (i.e. raw bits just have logical element wise operators and equality, uint adds a notion of addition, less then, etc... since these only hav meaning if you're interpreting the bits in a certain way). However, it seems like this is inconsistent with the SMT bitvector theory? (which defines all the operators on bitvectors) |
@leonardt |
In phanrahan/magma#457 @jameshegarty requested type checking on signedness. One way we could approach the role of Unsigned is simply for type checking.
This is convenient as the code doesn't need to be littered with casts.
Now the the final error conditions is probably not desirable so we could add the
It should be noted that such a change will undoubtedly break a lot of code. @jameshegarty would a warning be sufficient? Adding that would not be hard. Another option would be to add a flag to turn strict type checking on.
However, people who extend hwtypes (read: |
I don't have much context for this discussion but maybe I can add some issues I've run into. IMO It's realllly hard to automatically figure out the type conversions for math ops (eg to cast unsigned to signed without losing precision, you need to add an extra bit, but you also may not want this a lot of the time!). Not saying it's impossible, but without spending a lot of time on this, IMO I would prefer to err on the side of just making everything explicit, at least for a hardware language. The extra casts don't bother me, personally. I would also caution against adding warnings. These are usually ignored, and don't actually enforce any behavior in the language. This is certainly the case with Verilog. I would be ok with having a way to disable checks as a temporary backwards compatibility mode though. |
btw I think my request was related to Magma in general (ie including arrays, handshakes, whatever). I don't fully understand how this repo relates to that effort. |
This is 100% true. Won't stop me from raising warnings though.
For it to be backwards compatible it would needs to be explicit enable instead of explicit disable.
This repo defines (or will define in the future) the interfaces to these types and provides python functional models. |
I wanted to comment on how I thought the code was suppose to work. Sadly, no guarantees. All operators should be strictly typed. For example, you can add two unsigned or two signed, but not a signed and an unsigned. The result should be the same type as the operands. Also, recall the type hierarchy. Bits < Arrays This means that array access are inplemented on Bits, UInt, and Sint. Bits implement bitwise operators. Current, SInt and UInt also inherit these operators. One could argue with this decision. Arithmetic and relational operators only work on Uint and SInt. Finally, type checking should also be done at the level of functions. For add(a,b) is equivalent to a+b. We are encouraging people to use <= for assignment This works because the rhs must be an output and the lhs must be an input (which differentiates this operator from less than or equal). We could do strict typing on assignment. |
I agree with that, I think that makes sense! My understanding is then, you could send a UInt[8] into a port that expects Bits[8], but could not send a SInt[8] into a UInt[8] port. And I would advocate for having the same behavior on the <= assignment as well, and the other various ways of doing wiring. |
As I mentioned above this is not this case and will break things if it is. I am fine with making things strict if we can get people to update downstream tools...
We need to unify the
|
Addendum: |
What about implementing all the operators as methods in BitVector, but only overload I do agree in general with James that we should be stricter on typing. |
This is currently the case |
@phanrahan
|
I agree that it may be confusing to not overload the operators in BitVector. We could create a new class Bits, but let me think about it. The following
would all be errors, since it would be an error to do an implicit cast.
would work. |
@phanrahan so this should be an error as well then?
Also what about
I personally am not really a user of hwtypes so have very little stake in the decision. However, I want to be clear about all the cases and ramifications of requiring an explicit type match. |
@leonardt and I discussed this case in the past
We thought that this should be allowed, with a type check that the python Generally, we would support inheritance on magma types. So, Tagged would be considered a By this reasoning, There is a question of what should be the type of the result when inheriting an operator. Should the result be the type which implements the operator, or the instance that was being called with the operator. I think it should be the type of the instance.
should return an My 2c. |
I somewhat disagree with your stance on But even without that, the rules you are describing are becoming a bit convoluted. def type_check(self, operand):
# Allow tagged_uint to work with uint but prevent uint from working with bv
if isinstance(operand, type(self)) and isinstance(self, (AbstractUnsigned, AbstractSigned)):
return True
# Allow tagged_bv to work with bv but prevent uint from working with bv
elif isinstance(operand, type(self)) and not isinstance(operand, (AbstractUnsigned, AbstractSigned)):
return True
# Allow int
elif isinstance(operand, int):
return True
# Allow types that support __int__ but not bitvector types
elif hasattr(operand, '__int__') and not isinstance(operand, AbstractBitVector):
return True
else:
return False If I have misinterpreted your goals please correct me. |
I was thinking that bitwise operators would be part of uint and sint, since these are subclasses of bits. Thinking about it some more, I am worried that checking for int is too general. My code would probable be simpler.
And then make sure the operators return type(self). |
Your code excludes |
I would only allow |
@rdaly525 @rsetaluri @leonardt As far I am concerned I would think the following is the most intuitive rule: def type_check(self, operand):
if isinstance(operand, int):
return True
elif isinstance(operand, type(self)):
return True
else:
return False But again I am not really a user so don't have a lot of stake in this. |
I agree that is more precise. Yes, it would be good to get other comments on this, including @jameshegarty. My default model for numeric types these days is Rust, which does not implicit type conversion and requires types to match on numeric operators. |
I am fine with that typechecking rule |
I am a fan of stricter rules, requiring the user to do conversion where necessary. I think the difference between the two most recent proposed rules by @cdonovick and @phanrahan is that @cdonovick uses In @cdonovick's scheme, it would be okay to do something like @phanrahan requires strict type checking (no implicit up/down cast), which is less convenient for the user but easy to understand. Can we define a clear set of rules for up/down casting w.r.t. to operators and sub/super types? |
I switched my vote from The following would be legal.
Since The following would be lilegal.
|
Okay, it seems that actually works with Caleb's rule, basically operator would be defined on uint, so it would fail an isinstance check with a bits (but the other way around would work for a bits operator). So the summary seems to be implicit upcasting (casting to the super type) is allowed. |
My only additional comment is that the type work properly for commutative operators.
|
I'm also generally in favor of allowing this implicit casting to super type and defining the ops on the the "oldest" member in the type hierarchy. |
Not sure if I should start a new issue for this, but magma has to extend the Tuple/Product types for various reasons, so I would vote to add Tuple/Product (and Sum, etc...) to be part of the family if possible. |
@phanrahan we can have def __operator__(self, other):
# Note BV[8] is not a subclass of BV[16] so this ensures a size match
if isinstance(other, type(self)):
return operator(self, other)
elif isinstance(other, int):
return operator(self, type(self)(other))
else:
return NotImplemented
def __roperator__(self, other):
if isinstance(other, type(self)):
return operator(other, self)
elif isinstance(other, int):
return operator(type(self)(other), self)
else:
return NotImplemented
Again I think we should add arithmetic operators to bits so that its inline with bitvector. |
@leonardt In my mind there is no reason you should have to subclass the ADT types. Maybe we meet to discuss what your needs are. And in any event I am strongly opposed to adding them to the family. They are not dependent on or related to BitVector types in any way. |
I'm happy with stricter rules, no implicit conversion but inheritance operators work as #98 (comment) My question is, what is explicit conversion in magma? is Currently,
Because But downcast doesn't work now.
Python doesn't have downcast, so it may still make sense, in terms of Python type. Most convenient way to convert SInt from UInt now is,
|
Type families are a hack. I would like to make them more elegant.
I want to define a class
Family
which expects that inheriting classes will have inner classesBit
andBitVector
, then automatically generatesSigned
/Unsigned
for those classes.expands to
Where
Now currently
Unsigned
is pointless as it is basically just an alias ofBitVector
. So I think we should do one of two things: drop it or remove signed dependent operators and functions fromBitVector
and require the use ofUnsigned
. Now changing the interface ofBitVector
would break a lot of code so I would lean towards just removingUnsigned
as it is basically unused.The text was updated successfully, but these errors were encountered: