Configurable initial register values

[martijnbastiaan]

Updated: 2019 June 14

This is an implementation of configurable initial register values, discussed in #516 and in the comments below. We've settled on the following design:

• All data types previously taking a Domain, now take a tag of kind Symbol denoting the domain name. For example, Clock is now: Clock (dom :: Symbol).
• Domain is no more, but DomainConfiguration now exists specified by:

-- | A domain with a name (@Symbol@). Configures the behavior of various aspects
-- of a circuits. See the documentation of this record's field types for more
-- information on the options.
--
-- See module documentation of "Clash.Explicit.Signal" for more information on
-- how to create custom synthesis domains.
data DomainConfiguration
  = DomainConfiguration
  { _tag :: Symbol
  -- ^ Domain name
  , _period :: Nat
  -- ^ Period of clock in /ps/
  , _edge :: ActiveEdge
  -- ^ Determines which edge of the clock registers are sensitive to
  , _reset :: ResetKind
  -- ^ Determines how components with reset lines respond to changes
  , _init :: InitBehavior
  -- ^ Determines the initial (or "power up") value of various components
  , _polarity :: ResetPolarity
  -- ^ Determines whether resets are active high or active low
  }
  deriving (Typeable)

• Domains are unique on their name. This is achieved by making KnownDomain a typeclass with a functional dependency on its name/configuration. Users should create their own domain by using a template function createDomain:

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

Lines 492 to 512 in 05d3fa8

	-- | Convenience method to express new domains in terms of others.
	--
	-- > createDomain (knownVDomain @System){vTag="System10", vPeriod=10}
	--
	-- This duplicates the settings in the "System" domain, replaces the name and
	-- period, and creates an instance for it. As most users often want to update
	-- the system domain, a shortcut is available in the form:
	--
	-- > createDomain vSystem{vTag="System10", vPeriod=10}
	--
	-- The function will create two extra identifiers. The first:
	--
	-- > type System10 = ..
	--
	-- You can use that to dom Clocks/Resets/Enables/Signals. For example:
	-- @Signal System10 Int@. Additionally, it will create a 'VDomainConfiguration' that you can
	-- use in later calls to 'createDomain':
	--
	-- > vSystem10 = 'knownVDomain' @System10
	--
	createDomain :: VDomainConfiguration -> Q [Dec]

• A function in need of one of these fields should indicate so by using a constraint KnownDomain. A HiddenReset or HiddenClock automatically introduces this constraint. Simple one-clock designs can continue to use SystemClockReset without making any changes.

• Reset polarity is carried in the domain, as well as its synchronicity. A Reset itself is now a very simple datatype.

• Clock gatedness as a concept does not exist anymore in Clash. Instead, users should use a separate Enable line to achieve the same. Almost all components in Clash have an Enable line.

---

To summarize the design's features:

• It should be easily extendible if we ever think of adding new domain configuration options.
• It doesn't require any new concepts over current Clash designs. Users are already familiar KnownNat constraints, the new KnownDomain constraint should feel familiar.
• Thanks to the use of AppendSymbol, these constraints are usable in a multi-clock designs. Coincidentally, we can use this strategy to support hidden clocks / resets in multi-clock designs too!

---

For reviewers:

• Core API changes can be found in 000db69.
• Core compiler changes can be found in c4da0ac.
• Primitive changes can be found in 5a4e108
• All other commits are just "fix up" commits. Nothing exciting should be in there.

---

Roadmap

• Restructure 'clash-prelude'
• Fix doctests in 'clash-prelude'
• Fix documentation
• Fix clash-lib
• Fix clash-ghc
• Fix clash-cosim
• Repair testsuite
• Fix tutorial
• Rebase on master
• Split commits in style / non-style commits (I had to touch the whole of clash-prelude, so figured I'd get it consistent with our style guide), or revert them
• Write tests for multiple hidden clocks
• Implement reset polarity in blackboxes
• Fix DDR primitives (Use deepErrorX in Clash.Explicit.DDR.ddrIn #546 I believe)
• Fix bug causing HOClock test to fail. Will be fixed in another PR.
• Extend createDomain to create type aliases
• Write a blogpost outlining the difference between all the different domain options and how to use them

[oliverbunting]

Could the domain also encompass the reset behaviour? I've always felt uneasy about the ability to connect up logic on the same clock, with different resets, which are nominally in the same domain.

I think would would make reasoning about reset behaviour over any domain easier.

[martijnbastiaan]

I think so. If I understand you correctly, this would induce the following change:

 data Domain name period initKind edgeKind
   = Domain { domainName :: SSymbol name
            , domainPeriod :: Period name period
            , domainInit :: Init name initKind
            , domainEdge :: Edge name edgeKind
+           , domainReset :: ResetNess name resetKind
            }

As a bonus, we could freely add reset polarity too:

data ResetPolarity 
  = ActiveHigh 
  | ActiveLow

-data Reset (domain :: Symbol) (synchronous :: ResetKind) where
-  Sync  :: Signal domain Bool -> Reset domain 'Synchronous
-  Async :: Signal domain Bool -> Reset domain 'Asynchronous
+data Reset (domain :: Symbol) (polarity :: ResetPolarity) where
+  Reset    :: Signal domain Bool -> Reset domain 'ActiveHigh
+  InvReset :: Signal domain Bool -> Reset domain 'ActiveLow

[martijnbastiaan]

Where ResetKind (in ResetNess for the lack of a better word) would still be:

data ResetKind
  = Synchronous
  | Asynchronous

[oliverbunting]

data ResetKind
  = Synchronous
  | Asynchronous
  | None

Although i don't know how that works out in practice. Maybe just the 2 is saner

[martijnbastiaan]

3 options is hard, because you can't (easily?) write a function which "can deal with Synchronous and Asynchronous, but not with None". I'm having the same implementation problem with:

data EdgeKind
  = Rising
  -- ^ Registers are rising edge (low-to-high) sensitive
  | Falling
  -- ^ Registers are falling edge (high-to-low) sensitive
  | Double
  -- ^ Registers are sensitive to both a rising edge (low-to-high) and a
  -- falling edge (high-to-low). [Not supported yet.]

I have to think about it some more.

[oliverbunting]

Double is a bit weird.
FPGA's certainly don't support that internally, although they do have DDR primitives at the pins.

[martijnbastiaan]

We know at least some interest exists to use Clash for ASICs so I don't think we should only focus on FPGAs :). Anyway, I mainly added it to see how much sense it makes to introduce 3 options in some domain property. And so far I still don't know, so I'll keep experimenting.

[leonschoorl]

We have some DDR primitives, their DDR signals might be annotated with edgekind Double.

[martijnbastiaan]

After an offline discussion with @oliverbunting, we concluded that we just need a delayEn. "None" can simply be achieved by not routing Reset. We still might want to move reset kind to domain though, in order to implement type-safe reset polarity.

[leonschoorl]

If you want to describe a function that could be active on either edge, but not both, maybe something like:

data ActiveEdge
  = OneEdge Edge
  | BothEdges

data Edge = Rising | Falling

f :: KnownEdge dom ('OneEdge edge)
  => Signal dom a -> Signal dom a

[martijnbastiaan]

I've confirmed something like that works @leonschoorl. The jury is out on its prettiness :P.

[christiaanb]

My initial thoughts: I'm really not liking even more KnownXYZ constraints and GADTs. I feel like much of this information could be stored as normal data types inside the constructors for the Clock type; perhaps using some phantom types and "smart constructors".

[christiaanb]

But I'd rather discuss this when I'm back in the office to understand the rational behind the current design.

[martijnbastiaan]

I'm open to suggestions! Although I don't think the Known* are too bothersome, it wasn't what I set out to do. I have tried to do it with phantom types and "normal" constructors, but I couldn't manage without making them completely cumbersome to work with. I'll see if I can reproduce the process I went though, and detail why it didn't work out tomorrow.

[martijnbastiaan]

Alright, didn't see your second comment just now. I'm fairly convinced that phantom types can't really work (conveniently), so I'll still try to write up the process tomorrow. If it fails we can try it face to face when you're back (and I'm back from the UK too, so probably in 2.5 weeks).

[christiaanb]

@martijnbastiaan my apologies, I should've waited with reacting before reading the entire PR properly. When I saw all the new KnownPeriod stuff, I was afraid the same would happen for the KnownInit, KnownEdge, etc. But I think the solution is to give up slightly on type safety in the clock type:

-- | A clock signal belonging to a @domain@
data Clock (domain :: Symbol) (gated :: ClockKind) where
  Clock
    :: SSymbol nm
    -> Integer
    -- ^ Period
    -> Clock nm 'Source

  GatedClock
    :: SSymbol nm
    -> Integer
    -- ^ Period
    -> Signal nm Bool
    -> Clock  nm 'Gated

The same can be done for the Edge and the InitKind, they can just be stored as normal value inside clock, so the values can be used where needed, ie:

-- | Get the clock period of a clock (in /ps/) as a 'Num' from a 'Domain'
clockPeriod
  :: forall domain period gated a
   . Num a
  => Clock domain gated
  -> a
clockPeriod (Clock _ p) = fromInteger p
clockPeriod (GatedClock _ p _) = fromInteger p

[christiaanb]

Another issue really needs solving properly is:

old

ddrIn 
  :: ( fast ~ 'Dom n pFast   
     , slow ~ 'Dom n (2*pFast))

vs

new:

ddrIn
  :: KnownPeriod fast pFast
  => KnownPeriod slow pSlow
  => 

where in the old/current API, when you use this function in a monomorphic context, and the periods do not exactly differ by 2*, you get a type error right away.

with the new proposed API you simply propagate the constraint:

:: (KnownPeriod "DomA" pFast, KnownPeriod "DomB" (2*pFast)

and what's now stopping me from assigning period 4 to "DomA" in one part of my design, and period 5 in another part? Using withDomain (Domain "DomA" 4) in one part, and withDomain (Domain "DomA" 5) in another part. This is bound to happen in actual code, especially as you get larger teams.

This could never happen in the old/current design, because the period was an integral part of the domain annotation on Signals. I don't think I can accept an API where the above descirbed situation can legally happen.

[martijnbastiaan]

Right, I had considered putting them in as "normal" values, but -ironically- thought that wouldn't have a chance of passing the Christiaan test :P. I'm slightly hesitant of it too, considering that you would store period/init/edge-iness in various places without type guarantees.

and what's now stopping me from assigning period 4 to "DomA" in one part of my design, and period 5 in another part?

The direct answer to this question is: we can reliably track what domains we've seen in the Clash compiler, and generate an error if we see any differences between domains with the same name. As opposed to Clock/Reset/etc we don't (shouldn't?) export the Domain constructor so we could even do some simple tracking in mkDomain. I realize this postpones errors to the simulation or synthesis stage, but the fact that we can be 100% sure this works is valuable IMO. This is opposed to Integer etc, which we can neither guarantee to correspond to their type level siblings in simulation nor while synthesizing.

The indirect answer is that using Integer for period works in practice, but I'm not so sure the same tactic would work for Edginess (for lack of a better word) without some magic. Say you have:

f :: Clock (domain :: NameAndPeriod) 'RisingEdge (gated :: ClockKind)
  -> Signal domain Int

g :: Clock (domain :: NameAndPeriod) 'FallingEdge (gated :: ClockKind)
  -> Signal domain Int

Now, you'd like to write:

h :: Clock (domain :: NameAndPeriod) edge (gated :: ClockKind)
  -> Signal domain Int

I don't think you can do it without resorting to unsafeCoerces. The same goes for Init. Because we never have to make a decision on period, we wouldn't have previously encountered this problem. We could probably put period back in domain (so instead of Symbol, you'd get OldDomainType), but it felt a bit arbitrary to leave it in after I had cooked up the current PR's method.

Last but not least, and I don't want to drag oude koeien uit de sloot, I think the current design avoids the conceptual problem of "where to put the Edge / Init", which helps from a pedagogic point of view.

To complete my sales pitch: I think the current PR proposes a method that's safe, easy to understand, easy to extend and implement. It only needs a single modification to Clash itself (that is, domain tracking). If a user manages to do something wrong, they'll get a clear and easy to understand error.

[christiaanb]

I thought of a solution yesterday, but was too tired to go back on the laptop again.
Instead of using the Hidden class for things like KnownPeriod, make it an actual class like so:

class KnownPeriod (domain :: Symbol) (period :: Nat) | dom -> period where
  knownPeriod :: SNat period

Now there can be only 1 period per domain; and we could do the same for the active clock, etc.

Also, the only safe way to construct a Clock for the user would be to use clockGen and tbClockGen; which will use the KnownPeriod, KnownEdge, etc to fill the "untagged" (Integer vs Period nat) field of the Clock constructor. I a so-called "expert" user then goes and uses the .Signal.Internal to construct an illegal clock that's their problem.

[martijnbastiaan]

That's an option @leonschoorl and I discussed, but for some reason we decided not to go with that one. I can't remember if we had a good reason or not. I'll see if it come back to me in the following days. Have a nice weekend in SF :)!

[martijnbastiaan]

I did manage to think of the reasons we shot it down, but after rereading your comment I realize the designs are slightly different, so they don't really apply. I do think the Hidden approach would still have some upsides:

1. Case-ing on Edge/Init is guaranteed to work out, as we know type information will always propagate. (And we'd finally leverage GADT support! ;))
2. Functions can explicitly indicate what things they are sensitive to, with type guarantees that they won't touch things they promise not to touch.

A minor complaint is that I don't think using instances (with domains leaking into a global namespace, even if you don't end up using it in your design) is the most elegant. It's not something I really care about though, as I doubt it would be a problem in practice.

Hopefully we can resolve this before Monday so I can freely work on it :)

[christiaanb]

clock period and active flank really need to be globally unique for a domain, so a normal type-class (constraint) is really the proper solution is that part of the design space.

[christiaanb]

This is too big of a change to be resolved before monday, as I really want to have a proper in-person discussion; and I won't be in until tuesday morning. Changing the core API simply requires more consideration and design iterations than other features and shouldn’t be rushed.

[christiaanb]

Here's some of my initial test code, but requires more experimentation: https://gist.github.com/christiaanb/8eac9bc72fc2bf44e9cce2a8499a4db8

I has:

• Globally unique flank, period, etc per domain
• Multiple implicit clocks
• Supports monomorphic implicit clocks (needs more experimentation)
• Supports un-annotated functions that have implicit clock (i.e working. type inference)
• Keeping existing Clash.Prelude API/Types seems likely

Still needs:

• Initial value handling, Reset polarity, etc.
• More testing with monomorphic and un-annotated contexts

[martijnbastiaan]

Initial value handling,

Put it in KnownConfiguration, or handle it separately with a KnownInit.

Reset polarity, etc.

Move ResetKind to KnownConfiguration, replace current holder of ResetKind with a Polarity construct.

As far as I can tell, your proposal is what I've proposed here, with the Known-constraints consolidated in a single construct *and implemented with instances. Could you confirm this? Either way, it's fine by me, but like I said earlier, you'll lose:

Functions can explicitly indicate what things they are sensitive to, with type guarantees that they won't touch things they promise not to touch.

This could be solved by reintroducing KnownInit, KnownEdge, with a single superconstraint KnownConfiguration.

And you'll also lose the ability to have dynamic subdomains (that is, part of your design with an "generated" modification to the current configuration), because you can't do hidden class instances. This can be solved, if you wanted to, by using a KnownConfiguration but without instances, but with a check in the Clash compiler itself. Edit: <-- this is the biggest reason we decided to not use the implementation with instances.

[martijnbastiaan]

One more thing

Supports un-annotated functions that have implicit clock (i.e working. type inference)

I've experimented with this and it doesn't seem an issue in practice if GHC can't. You almost always pass a "real" argument anyway (mostly Signals) that refer to the symbol allowing type inference to figure out what constraint belongs to what function call.