search

phanrahan / magma

magma circuits
Other
242 stars 23 forks source link

[RFC] Shift Operator Width #874

Open leonardt opened 3 years ago

leonardt commented 3 years ago

Right now, we expect the width of the shift amount to be the same as the width of the value being shifted. This stems from the coreir, hwtypes, and smt interface. The proposal is to support implicit extension of shift amounts that contain log2 the number of bits of the amount being shifted.

The downside is we lose compatibility with hwtypes, so we may want to consider adding it as a "frontend" feature there as well. One option would be that the internal representation can still use the SMT definition requiring equal bit widths, but the interfaces can do implicit extension before invoking the core code.

The motivation is that doing this implicit extension should be safe (in all cases?). Alternatively, we can drop this and ask the the user use smart bits instead. Does requiring the extra bits in the shift amount offer us any benefits besides maintaining consistency with the other primitives (i.e. they all use the same number of bits for the inputs/outputs)? In fact, does it provide less safety in that the user could accidentally provide a shift amount that's great than the number of bits in the value being shifted? Maybe not an error, since the result should be the same as just using the lower bits.

rsetaluri commented 3 years ago

I don't see this as being categorically different from making all the operators more loose w.r.t. bit-widths, e.g. we could also say + should be more flexible as a frontend. Also, I think in all cases, as long as we're using CoreIR we should compile to proper SMT ops.

I think the only question is whether "SmartBits"^ should become mainline or not. Which boils down to the question of are users ok entering a smart regime and popping back out while SmartBits isn't mainline. Given people aren't using it yet, my guess is they are not willing to do this, but I don't know. But I really like the idea of having access to strict types and loose types, whatever they're called (e.g. could do SmartBits -> Bits, Bits -> DumbBits 😄).

(^SmartBits is in " " because if we mainline it, it deserves a much harder look and rigorous testing.)

cdonovick commented 3 years ago

It is not without precedent for shift to be shift :: BitVector[N] -> BitVector[log(N)] -> BitVector[N] in fact this is what boolector does. I would be fine with making hwtypes type shifts as shift :: BitVector[N] -> Union[BitVector[N], BitVector[log(n)]] -> BitVector[N] if someone wants to submit a PR updating the various BV implementations.

rsetaluri commented 3 years ago

Ok, I see. I misinterpreted the intent here. Would also be ok with that as part of the base spec. for shift.