Stateful simulation

Clash Help
1

I was wondering if there are any ways to do stateful simulation in Clash already. With stateful simulation I mean being able to run one clock cycle at a time: feeding the inputs, checking the outputs, then determine what to do next.

Afaik the only way to simulate circuits is to pre-generate the test input list, convert it to a signal, pass it to the circuit, and sample the output signal. IMO this is way too limiting. Stateful simulation would:

  • Allow you to generate inputs “on the fly”
  • Short circuit failing tests
  • Make it easier to verify certain properties, e.g. stall stability:
data StallState a = Stalled (Maybe a) | NotStalled

-- Validates the !READY -> $stable(FWD) property.
validateStallStability ::
  (Eq a) =>
  StallState a ->
  -- ^ Current stall state
  Maybe a ->
  -- ^ DUT output
  Bool ->
  -- ^ READY to DUT
  (StallState a, Bool)
  -- ^ (Next stall state, violation)
validateStallStability stallState inp ready = (nextStallState, violation)
 where
  -- Just an example, doesn't take care of ready being undefined
  (nextStallState, violation) = case (stallState, ready) of
    (NotStalled, False) -> (Stalled inp, False)
    (NotStalled, True) -> (NotStalled, False)
    (Stalled prev, False) -> (Stalled prev, Maybe.isJust prev && prev /= inp)
    (Stalled prev, True) -> (NotStalled, Maybe.isJust prev && prev /= inp)

To be able to do this I imagine some kind of function like:

runCycle :: (Signal dom a -> C.Signal dom b) -> a -> (b, Signal dom a -> Signal dom b)

Which runs the circuit for one clock cycle given the input a, and returns the output b and the new circuit. No idea if this is even possible to implement.

Happy to hear opinions on this, because it would be pretty cool if we could improve this.

2

Both sample and fromList are lazy functions that eat a single sample at a time. In fact, if we define the following

let
  asList = a : b : c : d : ...
  asSignal = a :- b :- c :- d :- ..

where both are infinite length, then sample asSignal is identical to asList and fromList asList is identical to asSignal. : is a list constructor and :- is the sole constructor for a Signal. It basically swaps constructors. The only reason sample and fromList are not bijective and each other’s inverse is that lists can be finite.

So nothing stops feedback! The following is fine:

>>> import qualified Prelude as P
>>> f = register 0
>>> :{
||| let
|||   is = P.map (+1) os
|||   os = sample @System $ f $ fromList is
||| in P.take 10 os
||| :}
[0,0,1,2,3,4,5,6,7,8]

This is not a circuit with feedback! This a circuit whose top-level output is looped back to its top-level input during simulation. And it goes through lists. Your function eating os could do whatever it needed to produce is, including IO or dark magic.

1 Like
3

There is a given function in prelude exactly for this: SignalAutomaton

which you give some function from signal to signal and then it allows you to step through the simulation one cycle at the time.

1 Like
4

You can also use that, but for many things just walking a list seems more than sufficient, and walking the list also works with multiple domains and is easier with multiple inputs.

5

I’m not sure I follow. Could you give me a hint how for example the following would work using your list implementation:

Fetch single input from somewhere (TCP socket, file, doesn’t really matter), give it to the circuit, get an output. Send it of into a blackbox IO/async/whatever function and receive the next input. And repeat.

Granted Tims request could work as the example does not do something quite as complex. But I imagine he wants to combine this with something non-clash based, like IO or some test monad or something else.

6

I think I didn’t fully think through the interaction between monads and feedback. As soon as the monad is part of the feedback loop, I’m having trouble coming up with a solution. Monadic input is no problem, monadically processing the output is also fine, but the feedback is problematic.

1 Like
7

Thanks for the replies. signalAutomaton seems to work quite nicely, even though I need to brush up my Haskell knowledge (arrows? :p)

dut :: Signal System Int -> Signal System Int
dut = exposeClockResetEnable (register 0) clockGen resetGen enableGen

runCycle :: (Automaton (->) Int Int) -> Int -> (Int, (Automaton (->) Int Int))
runCycle (Automaton f) x = f x

test :: IO ()
test = do
  whileM
    ((< 10) . fst)
    (\(i, auto) -> do
      let (output, nextAuto) = runCycle auto (output + 2)
      print output
      return (i + 1, nextAuto)
    )
    (0 :: Int, signalAutomaton dut)

Output is as expected:

0
0
2
4
6
8
10
12
14
16
1 Like
8

IKR? :joy: It’s why I hoped to get the job done without it. I did look for that function but forgot where it was; luckily, Rowan was on the case.

Thanks for including an example of getting it working; that’s very valuable for this forum.

2 Likes