This repository has been archived by the owner. It is now read-only.

`regEn#` fails to converge in sim when enable depends on previous output #104

Closed
cbiffle opened this Issue Apr 22, 2017 · 0 comments

Comments

Projects
None yet
1 participant
@cbiffle
Contributor

cbiffle commented Apr 22, 2017

In ed616b5, the (simulation-time) definition of regEn# was changed to evaluate its signal operands more eagerly and avoid a space leak. The implementation is now a recursive stream generator using a helper function:

regEn# :: SClock clk -> a -> Signal' clk Bool -> Signal' clk a -> Signal' clk a
regEn# _ = go
  where
    go o (e :- es) as@(~(x :- xs)) =
      o `seqX` o :- (as `seq` if e then go x es xs else go o es xs)

Note the tilde in the definition of go. This is a lazy pattern match, ensuring that execution can "pass" the equals sign and yield o (the register's current value) before deconstructing x :- xs (the stream of potential new values). This subtle detail ensures that a register can yield its current value when the new values depend on the current value, as in

counter f = let x = regEn 0 f (x + 1) in x

There is no tilde in the deconstruction of the enable stream e :- es. As a result, enables are eagerly deconstructed before output is yielded. If the enable signal depends on the output, evaluation cannot proceed. (In my case, this manifested as tests failing with "thread blocked indefinitely in an STM transaction" just after upgrading to the v0.7.1 tools, which bring in prelude 0.11.1 and this change.)

Here is a trivial case that no longer works with prelude 0.11.1:

-- Use regEn to re-implement register
badRegister i v =
  let x = regEn i en v
      en = const True <$> x
  in x

cbiffle added a commit to cbiffle/clash-prelude that referenced this issue Apr 22, 2017

regEn: allow enable to depend on output
This uses a lazy pattern to delay deconstruction of the enable signal
until after the current value has been yielded.

Fixes #104

cbiffle added a commit to cbiffle/clash-prelude that referenced this issue Apr 23, 2017

regEn: allow enable to depend on output
This uses a lazy pattern to delay deconstruction of the enable signal
until after the current value has been yielded.

Fixes #104

cbiffle added a commit to cbiffle/clash-prelude that referenced this issue Apr 24, 2017

regEn: allow enable to depend on output
This uses a lazy pattern to delay deconstruction of the enable signal
until after the current value has been yielded.

Fixes #104

@christiaanb christiaanb closed this in #105 Apr 24, 2017

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.