search

lastland / ScalaHDL2

The second version of ScalaHDL. Scala style!
6 stars 1 forks source link

type safety concerning bit length #8

Open lastland opened 8 years ago

lastland commented 8 years ago

For example, assigning the result of an addition between two 4-bit unsigned numbers to a 4-bit unsigned number would be dangerous, but assigning it to a 5-bit or even bigger unsigned number should be all right. It would be ideal if this sort of rules can be statically enforced at compile time by utilizing the Scala type system.

So instead of val a: Unsigned = Unsigned(0, 16), we may want something like this:

val a: Unsigned[16] = 0

The following code will result in type error:

val a: Unsigned[4] = 1
val b: Unsigned[4] = 2
val c: Unsigned[4] = a + b

If the users are sure that a + b will not overflow in a 4-bit unsigned register, or they intend to let it overflow, they must cast it to 4-bit explicitly.

SIP-23 may be able to help in this scenario. However, to achieve what we want, we may need something like this:

class Unsigned[N <: Int : SingleInhabitant] {
  def +(b: Unsigned[N]): Unsigned[N+1] = ...
}

It is unclear that if SIP-23 would support expressions like N+1 to be a type as shown in this case.

Indexing and slicing may become another challenge, because it is required to statically infer the type of a(x, y), where the value of x or/and y can only be dynamically determined.

lastland commented 8 years ago

This may not be the best approach for the following reasons:

  1. It would require more than literal-based type proposed in SIP-23. For example, we would require something like Unsigned[N+1] or Unsigned[X+Y]. This might be too complicated for a compiler.
  2. Not only Unsigned[N+1] but also Unsigned[N+2] and registers of many other types must accept the addition of Unsigned[N]s. This means that N+1 must be a subtype or supertype of N, which does not make much sense.
  3. This approach requires N of Unsigned[N] to be known at Scala compile time. This forbids programs from setting the bit-length at Scala runtime (e.g. from user inputs or from files).

An alternative strategy might be using refinement types and SMT solver. LiquidHaskell may be able to provide some inspirations for us.