Circuit notation for cyclic circuits

Clash Help
1

I’m trying to use clash-protocols’s circuit notation to describe a circuit which has two-way communication between component1 and component2:

         +---+        +---+
         |   |  --->  |   |
   +---> | 1 |        | 2 | ---+
   |     |   |  <---  |   |    |
---+     +---+        +---+    |     +---+
   |                           +---> |   |
   |                                 | 3 | --->
   +-------------------------------> |   |
                                     +---+

component1 :: Circuit (P1 dom A, P1 dom B) (P1 dom C, P1 dom D)
component2 :: Circuit (P1 dom C) (P1 dom B)
component3 :: Circuit (P1 dom A, P1 dom D) (P1 dom E)

foo :: Circuit (P1 dom A) (P1 dom E)
foo = circuit \a -> do
    (c, d) <- component1 -< (a, b)
    b <- component2 -< c
    component3 -< (a, d)

But this fails with:

 • No instance for ‘Units (Tagged (P1 dom A) (Signal dom Ack))’

132 |     component3 -< (a, d)

(here, I have type P1 = Df.Df)

3

I get the same error even with the cycle removed:

foo :: Circuit (P1 dom A, P1 dom B) (P1 dom B, P1 dom E)
foo = circuit \(a, b) -> do
    (c, d) <- component1 -< (a, b)
    b' <- component2 -< c
    e <- component3 -< (a, d)
    idC -< (b', e)

This also fails with the missing Units instance, this time on the idC -< (b', e) statement.

4

Interestingly, this seems to work:

foo :: Circuit (P1 dom A) (P1 dom D)
foo = circuit \a -> do
    (c, d) <- component1 -< (a, b)
    b <- component2 -< c
    idC -< d

So it seems that the problem really is the pairing up of a and d to pass to component3.

Looking at it further, it seems it’s the fanout of a that is the problem, since this works:

foo :: Circuit (P1 dom A, P1 dom A) (P1 dom E)
foo = circuit \(a, a') -> do
    (c, d) <- component1 -< (a, b)
    b <- component2 -< c
    component3 -< (a', d)

And now I think I get it – of course there is no way to do fan-out, since there is no generic way to combine the upstream signals from the two consumers.

5

Don’t know if this answers your question fully, but I wanted to note that you already found one piece of this yourself: busses have to be used linearly (in the general case).

That’s because protocols are inherently bi-directional, even if maybe some way is trivial, but every protocol has a Fwd and a Bwd.

The plugin only allows linear access to a bus, because then it works out! One Fwd is connected to one circuit and the Bwd gets “filled in” once, nice!

If you now connect a to multiple components, it might be easy to copy the Fwd, but as you noticed, how would it combine the two different Bwds?

That’s also the issue if you use a bus zero times, because then where does the Bwd even come from?

There are some escape hatches for simple cases, namely using Fwd and Bwd in an expression/pattern context, but I personally haven’t used that much. But I know that @martijnbastiaan and @rslawson have used that a bunch. So something like component -< (Fwd a, b) or (Fwd x) <- component -< ...

6

Yeah you can use Fwd to both construct and deconstruct, as long as the Bwd is “trivially driveable” (i.e., unit-like).

7

And while fanout as you have done in the original post cannot be done there are components that can help with that, for Df there is Df.fanout :: Circuit (Df dom a) (C.Vec n (Df dom a)) as an example.

foo :: Circuit (P1 dom A) (P1 dom E)
foo = circuit \a -> do
    [a0, a1] <- fanout -< a
    (c, d) <- component1 -< (a0, b)
    b <- component2 -< c
    component3 -< (a1, d)

Notice how you can pattern match on the Vec n circuit output as if it were a list,.

8

Hello! Sorry for the late reply here, but as has been mentioned, this should be somewhat trivial if the backwards of P1 dom a is trivially derivable. In which case, this might look something like

component1 :: Circuit (P1 dom A, P1 dom B) (P1 dom C, P1 dom D)
component2 :: Circuit (P1 dom C) (P1 dom B)
component3 :: Circuit (P1 dom A, P1 dom D) (P1 dom E)

foo ::
  (Bwd (P1 dom a) ~ ()) => -- Or similar, otherwise you'll need to do something else
  Circuit (P1 dom A) (P1 dom E)
foo = circuit $ \(Fwd a) -> do
  (c, d) <- component1 -< (Fwd a, b)
  b <- component2 -< c
  component3 -< (Fwd a, d)

Haven’t actually typechecked this, but it passes the typechecker in my heart.