leonardt / hwtypes

Python implementations of fixed size hardware types (Bit, BitVector, UInt, SInt, ...) based on the SMT-LIB2 semantics
BSD 3-Clause "New" or "Revised" License
18 stars 4 forks source link

Unhack TypeFamilies for magma #120

Open rdaly525 opened 4 years ago

rdaly525 commented 4 years ago

Currently, Magma has a different Enum/Product/Tuple from the hwtypes.adt types. This causes a lot of hacked user code in order to get Peak to compile to magma.

I would request we add all ADT types into TypeFamily so that we can nicely define ADT types the following way:

ADT_fc(family : TypeFamily):
    class A(family.Product):
        a = family.Bit
        b = family.BitVector[16]
    T = family.Tuple[A,family.Bit] 
    # etc...

Enum/Product/Tuple are probably sufficient in the short term, but we should also add Sum, and TaggedUnion once magma supports these ADT types.

@leonardt, @cdonovick, Any issues with this?

cdonovick commented 4 years ago

This is basically impossible because magma needs to support qualification (In(T), Out(T)) and wiring. The current plan for magma support in Peak is to use a magma variant of the AADT.

This is currently blocked by the magma compiler not currently supporting arbitrary types which behave correctly but are not one of the magma primitive types.

Unfortunately even once this is unblocked it will still be a bit hacky as type annotations will need to specify the AADT. e.g. instead of

InstT = Sum[A, B]
...
@sequential
class Foo:
    ...
    def __call__(self, inst: InstT):
        ...

We will need

InstT = MagmaAADT[Sum[A, B], assembler, Bits]
...
@sequential
class Foo:
    ...
    def __call__(self, inst: InstT):
        ...
cdonovick commented 4 years ago

As for why adding to the type ADT types to families is inappropriate: there is no actual relationship with between hwtypes.Tuple and hwtypes.BitVector hence they not such relationship should be enforced.

cdonovick commented 4 years ago

There is no methods on ADT types that return BV and there is no methods on BV which return ADT, so there is no reason to bundle them.

cdonovick commented 4 years ago

The above solution will automatically give magma support for Sum and TaggedUnion once the magma compiler is updated.

cdonovick commented 4 years ago

@leonardt do we have any timeline on when the _bits_ protocol should be ready?

rdaly525 commented 4 years ago

Okay, how about aiming for something like this in terms of a coding style

def Inst_fc(family, assembler):
  @assemble(family, assembler)
  class Inst(Product):
     a=family.Bit
     b=family.BitVector[16]

  return Inst

with the 'assemble' decorator returning the appropriate assembled ADT based off of family and assembler. If assembler is None, it could just return the normal ADT type.