Problem recursing on singleton lists

[danielsmw]

Below, I have two different version of a linear feedback shift register (LFSR). The goal is to synthesize

{-# LANGUAGE DerivingVia
           , DerivingStrategies
           , LambdaCase
           , AllowAmbiguousTypes
           , ApplicativeDo
           , StandaloneDeriving
           , StandaloneKindSignatures #-}

import Clash.Prelude
import Control.Lens
import Data.Default
import Data.Singletons.Prelude
import Data.Singletons.TypeLits as TL

topEntity :: Clock System -> Reset System -> Enable System -> Signal System (Unsigned 8)
topEntity = exposeClockResetEnable fibonacciLFSR8

-- Straightforward newtype
type LFSRState :: Nat -> Type
newtype LFSRState n = LFSRState { runLFSRState :: BitVector n }
  deriving (NFDataX, AutoReg) via (BitVector n)
instance KnownNat n => Default (LFSRState n) where
  def = LFSRState (fromIntegral 1)

This first version passes the taps of the LFSR via a term-level list, and synthesizes just fine.

fibonacciLFSR8 :: HiddenClockResetEnable dom => Signal dom (Unsigned 8)
fibonacciLFSR8 = fibonacciLFSRTerm @8 [3,4,5,7]

fibonacciLFSRTerm
  :: forall (n :: Nat) dom
   . KnownNat n
  => HiddenClockResetEnable dom
  => [Int] -> Signal dom (Unsigned n)
fibonacciLFSRTerm taps =
  let lfsr = autoReg def (LFSRState <$> lfsr')
      lfsr' = do lfsrState <- lfsr
                 -- shift the bit register by one, and then replace
                 -- the bit on the end by xor of the taps (via go)
                 return $
                   shiftL (runLFSRState lfsrState) 1
                   & ix 0
                   .~ go lfsrState taps
  in unpack <$> lfsr'
                    
  where
    go :: forall (n :: Nat)
        . KnownNat n
       => LFSRState n -> [Int] -> Bit
    go b@(LFSRState bs) = \case
      -- If there is only one tap left, return that bit
      (a:[]) -> bs ^?! ix a
      -- XOR a tapped bit with the remaining taps
      (a:as) -> xor (bs ^?! ix a) (go b as)
      -- This should never happen (we can't have no taps)
      [] -> error "A no-tap LFSR is ill-defined"

This second version (which was my original attempt) passes the taps through a type-level list. It runs just fine in clashi, but fails to synthesize:

fibonacciLFSR8 :: HiddenClockResetEnable dom => Signal dom (Unsigned 8)
fibonacciLFSR8 = fibonacciLFSRType @('[3,4,5,7]) @8

fibonacciLFSRType
  :: forall (taps :: [Nat]) (n :: Nat) dom
   . SingI taps
  => KnownNat n
  => HiddenClockResetEnable dom
  => Signal dom (Unsigned n)
fibonacciLFSRType =
  let lfsr = autoReg def (LFSRState <$> lfsr')
      lfsr' = do lfsrState <- lfsr
                 -- shift the bit register by one, and then replace
                 -- the bit on the end by xor of the taps (via go)
                 return $
                   shiftL (runLFSRState lfsrState) 1
                   & ix 0
                   .~ go lfsrState (sing :: Sing taps)
  in unpack <$> lfsr'
                    
  where
    go :: forall (n :: Nat) (indices :: [Nat])
        . SingI indices
       => KnownNat n
       => LFSRState n -> SList indices -> Bit
    go b@(LFSRState bs) = \case
      -- If there is only one tap left, return that bit
      (SCons a SNil) -> withKnownNat a
                        $ bs ^?! ix (fromIntegral $ TL.natVal a)
      -- XOR a tapped bit with the remaining taps
      (SCons a as) -> withSingI as $ withKnownNat a
                        $ xor (bs ^?! ix (fromIntegral $ TL.natVal a)) (go b as)
      -- This should never happen (we can't have no taps)
      SNil -> error "A no-tap LFSR is ill-defined"

Operationally I can obviously just use the first version. But it bothers me that this second version fails to synthesize (the memory usage blew up beyond 32 GB, to the point where I had to power cycle my machine). I observed this on both clash-1.4.2 and clash-1.4.3. Is this expected behavior?

[danielsmw]

I do wonder if this is related to #578, but I wasn't getting the same warnings/errors from clash observed there; just a memory leak. Also unlike that issue, here I'm not trying to store a recursive type; I'm just trying to use it at compile time.

[christiaanb]

I guess Clash' internal rewrite mechanism makes some "wrong choices" in terms of strategy (what transformation to apply when) for the second version leading to a exponential compile-time and resource usage. Does it also fail for?

fibonacciLFSR8 :: HiddenClockResetEnable dom => Signal dom (Unsigned 8)
fibonacciLFSR8 = fibonacciLFSRType @('[3]) @8

If it succeeds, at what size of the list does it start failing?

[danielsmw]

Yes, it "fails" even with a singleton list. I terminated it early, but not until it had eaten up over 10GB of memory. By contrast, the term-level definition is almost instantaneous and generates very clean verilog.

Somewhat interestingly, it does not fail when I give it the empty list... instead it generates the following (I added some annotations):

/* AUTOMATICALLY GENERATED SYSTEMVERILOG-2005 SOURCE CODE.
** GENERATED BY CLASH 1.4.3. DO NOT MODIFY.
*/
`timescale 100fs/100fs
module topEntity
    ( // Inputs
      input logic clk  // clock
    , input logic rst  // reset
    , input logic en  // enable

      // Outputs
    , output logic [7:0] result
    );
  // src/Example/LFSR.hs:17:1-9
  logic [7:0] lfsrState = 8'b00000001;
  logic [7:0] result_1;

  assign result = result_1;

  // register begin
  always_ff @(posedge clk or  posedge  rst) begin : lfsrState_register
    if ( rst) begin
      lfsrState <= 8'b00000001;
    end else  if (en)  begin
      lfsrState <= result_1;
    end
  end
  // register end

  // replaceBit start
  always_comb begin
    result_1 = (lfsrState << (64'sd1));
    result_1[(64'sd0)] = ({1 {1'bx}});
  end
  // replaceBit end


endmodule

I'm surprised that this synthesized while the singleton list didn't, since they're both just a single non-recursive evaluation of go.

[christiaanb]

What happens when you do:

fibonacciLFSR8 :: HiddenClockResetEnable dom => Signal dom (Unsigned 8)
fibonacciLFSR8 = fibonacciLFSRType @8 (SCons (SNat @3) SNil)

fibonacciLFSRType
  :: forall (n :: Nat) (taps :: [Nat]) dom
   . KnownNat n
  => HiddenClockResetEnable dom
  => SList taps -> Signal dom (Unsigned n)
fibonacciLFSRType taps =
  let lfsr = autoReg def (LFSRState <$> lfsr')
      lfsr' = do lfsrState <- lfsr
                 -- shift the bit register by one, and then replace
                 -- the bit on the end by xor of the taps (via go)
                 return $
                   shiftL (runLFSRState lfsrState) 1
                   & ix 0
                   .~ go lfsrState taps
  in unpack <$> lfsr'
                    
  where
    go :: forall (n :: Nat) (indices :: [Nat])
        . SingI indices
       => KnownNat n
       => LFSRState n -> SList indices -> Bit
    go b@(LFSRState bs) = \case
      -- If there is only one tap left, return that bit
      (SCons a SNil) -> withKnownNat a
                        $ bs ^?! ix (fromIntegral $ TL.natVal a)
      -- XOR a tapped bit with the remaining taps
      (SCons a as) -> withSingI as $ withKnownNat a
                        $ xor (bs ^?! ix (fromIntegral $ TL.natVal a)) (go b as)
      -- This should never happen (we can't have no taps)

i.e. eliminate the (sing :: Sing taps).

I'm trying to figure out something is going on with the interplay between the recursive "building" of the sing :: Sing taps value and then the recursive go function.

[danielsmw]

Unfortunately, that code (modulo two changes needed for compilation: I had to add a SingI taps constraint to fibonacciLFSRType, and I had to specify that the SNat constructor was from the singletons library) had the same problem.

[danielsmw]

For what it's worth, I removed the SingI constraint from both go and fibonacciLFSRType and it still has the same problem.

[christiaanb]

So some debugging shows that the compiler doesn't think SList is recursive and then goes down a rabbit hole.