Remove the need for KnownDomain constraints throughout Clash designs

[martijnbastiaan]

Clash primitives currently require KnownDomain constraints in order to change their behavior depending on their synthesis domain. It's implemented using class constraints as this - apart from all the dormant bugs it exposed - didn't require adding additional logic to the Clash compiler. An example of a primitive requiring a KnownDomain constraint is register#:

clash-compiler/clash-prelude/src/Clash/Signal/Internal.hs

Lines 1078 to 1082 in 9d278c2

	register# (Clock dom) rst (fromEnable -> ena) powerUpVal0 resetVal =
	case knownDomainByName dom of
	SDomainConfiguration _name _period _edge SSynchronous _init _polarity ->
	goSync powerUpVal1 (unsafeToHighPolarity rst) ena
	SDomainConfiguration _name _period _edge SAsynchronous _init _polarity ->

To remove the need for this constraint we would need to do two things:

1. On the simulation side of things, we'd need to remove all the KnownDomain constraints on Clash primitives. We subsequently need to add them to clockGen, resetGen, and enableGen. These primitives would use knownDomain to store a SDomainConfiguration inside the constructs they're building. For example, Clock might look like:

data Clock (dom :: Domain) = 
  Clock 
    (SSymbol dom) 
    (SDomainConfiguration dom (KnownConf dom))

(If this doesn't work out, we could go for VDomainConfiguration too.) Simulation constructs can now simply extract the synthesis domains from their given clocks. Of course, deconstructing clocks, resets, and enables is still not synthesizable! Thus...

2. To get synthesis working we need domain-extracting primitives for clocks, resets, and enables. For example, for a Clock this would look like:

clockDomain :: Clock dom -> SDomainConfiguration dom (KnownConf dom)

(We might want to wrap this in a typeclass so we can use the same function on clocks, resets, and enables all the same.) Clash would need to collect all instances of KnownDomain before synthesis and insert the result of knownDomain for every clockDomain it sees.

[paddytheplaster]

Hi Martijn,

Brilliant idea.

Regards,

Paddy

[martijnbastiaan]

Me and @leonschoorl talked about this yesterday. We concluded that the easiest way is probably to add GADT wrappers around Clock, Reset, Enable, and Signal that carry the KnownDomain dictionary. E.g.:

data SClock (dom :: Domain) where
  SClock (Clock dom) :: KnownDomain dom => SClock dom 

A few observations:

• This probably doesn't need complicated changes to the compiler. Clash is already fine with wrappings like these.
• We do need to extensions to conjure up KnownDomain constraints from thin air. E.g., users should be able to use SClock System -> .. in their top entity. (Clash already keeps a list of known domains, so this shouldn't be too hard.)
• We probably also want these constraints in Signal, to prevent things like unsafeToActiveHigh to get a KnownDomain constraint.

[rowanG077]

Will you be able to do something like natToNum @(DomainPeriod dom) without a KnownDomain dom constraint with this design? Or will you require to pattern match on SClock/Signal? I guess it would be better to introduce the value level versions of these type of functions which handle the KnownDomain handling. Ex: domainPeriod :: forall dom. Num a => a or with a proxy domainPeriod :: forall proxy dom. Num a => proxy dom -> a?

edit: Ahh sorry I'm confused. KnownDomain doesn't even introduce KnownNat (DomainPeriod dom) anyway

[martijnbastiaan]

edit: Ahh sorry I'm confused. KnownDomain doesn't even introduce KnownNat (DomainPeriod dom) anyway

It does since #2541 :-)

You will need to pattern match, yeah.

domainPeriod :: forall proxy dom. Num a => proxy dom -> a

The idea being that you can pass in any Clock/Signal/etc.? Yeah I like it.