Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

#

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Jump to bottom

Verilog generation runs indefinitely #2834

Open
kleinreact opened this issue Oct 28, 2024 · 4 comments
Open

Verilog generation runs indefinitely #2834

kleinreact opened this issue Oct 28, 2024 · 4 comments
Labels
bug

Comments

@kleinreact
Copy link
Member

Clash seems to diverge on the following reproducer (if being called with the --verilog flag).

-- diverges for: Size > 1
type Size = 2

topEntity :: Bit
topEntity = head table

table :: Vec Size Bit
table = lookupTable
 where
  lookupTable :: Vec Size Bit
  lookupTable = smap fill $ repeat ()

  fill :: forall n. SNat n -> () -> Bit
  fill n@(SNat :: SNat n) _ = case compareSNat n (SNat @0) of
    SNatLE -> low
    SNatGT -> case compareSNat n (SNat @Size) of
      SNatLE -> at @(n - 1) @(Size - n) SNat lookupTable
      SNatGT -> error "impossible"
@kleinreact kleinreact added the bug label Oct 28, 2024
@kleinreact
Copy link
Member Author

The compilation gets stuck in an infinite loop when calling normalizeTopLvlBndr on table[8214565720323799906], which is bound to the term referenced below.

Click here to see the term that is bound to table[8214565720323799906]. 
Clash.Sized.Vector.reverse @2
  @Clash.Sized.Internal.BitVector.Bit[8214565720323789991]
  (Clash.Sized.Vector.dfold
     @(Clash.Sized.Vector.VCons[8214565720323790001]
         Clash.Sized.Internal.BitVector.Bit[8214565720323789991])
     @2
     @GHC.Tuple.Unit[3746994889972252672]
     Test.table1[8214565720323804889][GlobalId]
     (GHC.Internal.Data.Proxy.Proxy[8214565720323796227]
        @(Data.Singletons.TyFun[8214565720323800214]
            GHC.Num.Natural.Natural[3674937295934324786]
            (GHC.Prim.TYPE[3674937295934324918]
               (GHC.Types.BoxedRep[3891110078048108766]
                  GHC.Types.Lifted[3891110078048108808]))
        -> GHC.Prim.TYPE[3674937295934324918]
             (GHC.Types.BoxedRep[3891110078048108766]
                GHC.Types.Lifted[3891110078048108808]))
        @(Clash.Sized.Vector.VCons[8214565720323790001]
            Clash.Sized.Internal.BitVector.Bit[8214565720323789991]))
     (Λl[6989586621679028560] ->
     λ(sn[6989586621679028561] :: Clash.Promoted.Nat.SNat[8214565720323789861]
                                    l[6989586621679028560]) ->
     λ(x[6989586621679028562] :: GHC.Tuple.Unit[3746994889972252672]) ->
     λ(xs'[6989586621679028563] :: Data.Singletons.Apply[8214565720323800213]
                                     GHC.Num.Natural.Natural[3674937295934324786]
                                     (GHC.Prim.TYPE[3674937295934324918]
                                        (GHC.Types.BoxedRep[3891110078048108766]
                                           GHC.Types.Lifted[3891110078048108808]))
                                     (Clash.Sized.Vector.VCons[8214565720323790001]
                                        Clash.Sized.Internal.BitVector.Bit[8214565720323789991])
                                     l[6989586621679028560]) ->
     Clash.Sized.Vector.Cons[8214565720323790005]
       @(GHC.Internal.TypeNats.+[3674937295934325540]
           l[6989586621679028560]
           1)
       @Clash.Sized.Internal.BitVector.Bit[8214565720323789991]
       @l[6989586621679028560]
       (_CO_
          @(GHC.Prim.~#[3674937295934324842]
              GHC.Num.Natural.Natural[3674937295934324786]
              GHC.Num.Natural.Natural[3674937295934324786]
              (GHC.Internal.TypeNats.+[3674937295934325540]
                 l[6989586621679028560]
                 1)
              (GHC.Internal.TypeNats.+[3674937295934325540]
                 l[6989586621679028560]
                 1)))
       (let
          wild[6341068275337658369] :: Clash.Promoted.Nat.SNat[8214565720323789861]
                                         l[6989586621679028560]
          = sn[6989586621679028561][LocalId]
       in case wild[6341068275337658369][LocalId] of
            Clash.Promoted.Nat.SNat[8214565720323789862]
              ($dKnownNat[6989586621679026853] :: GHC.Internal.TypeNats.KnownNat[3602879701896396842]
                                                    l[6989586621679028560]) ->
              case Clash.Promoted.Nat.compareSNat[8214565720323788356][GlobalId]
                     @l[6989586621679028560]
                     @0
                     wild[6341068275337658369][LocalId]
                     (Clash.Promoted.Nat.SNat[8214565720323789862] @0
                        (GHC.Num.Natural.NS 0##)) of
                Clash.Promoted.Nat.SNatLE[8214565720323789865]
                  (irred[6989586621679026872] :: GHC.Internal.TypeError.Assert[8214565720323788133]
                                                   (GHC.Internal.Data.Type.Ord.OrdCond[8214565720323788087]
                                                      GHC.Types.Bool[3674937295934324744]
                                                      (GHC.Internal.Data.Type.Ord.Compare[8214565720323788094]
                                                         GHC.Num.Natural.Natural[3674937295934324786]
                                                         l[6989586621679028560]
                                                         0)
                                                      GHC.Types.True[3891110078048108586]
                                                      GHC.Types.True[3891110078048108586]
                                                      GHC.Types.False[3891110078048108556])
                                                   (GHC.Internal.TypeError.TypeError[3674937295934325098]
                                                      (GHC.Prim.CONSTRAINT[3674937295934324920]
                                                         (GHC.Types.BoxedRep[3891110078048108766]
                                                            GHC.Types.Lifted[3891110078048108808]))
                                                      (GHC.Internal.TypeError.:<>:[3891110078048108697]
                                                         (GHC.Internal.TypeError.:<>:[3891110078048108697]
                                                            (GHC.Internal.TypeError.:<>:[3891110078048108697]
                                                               (GHC.Internal.TypeError.Text[3891110078048108694]
                                                                  "Cannot satisfy: ")
                                                               (GHC.Internal.TypeError.ShowType[3891110078048108703]
                                                                  GHC.Num.Natural.Natural[3674937295934324786]
                                                                  l[6989586621679028560]))
                                                            (GHC.Internal.TypeError.Text[3891110078048108694]
                                                               " <= "))
                                                         (GHC.Internal.TypeError.ShowType[3891110078048108703]
                                                            GHC.Num.Natural.Natural[3674937295934324786]
                                                            0)))) ->
                  Clash.Sized.Internal.BitVector.low
                Clash.Promoted.Nat.SNatGT[8214565720323789864]
                  (irred[6989586621679026876] :: GHC.Internal.TypeError.Assert[8214565720323788133]
                                                   (GHC.Internal.Data.Type.Ord.OrdCond[8214565720323788087]
                                                      GHC.Types.Bool[3674937295934324744]
                                                      (GHC.Internal.Data.Type.Ord.Compare[8214565720323788094]
                                                         GHC.Num.Natural.Natural[3674937295934324786]
                                                         (GHC.Internal.TypeNats.+[3674937295934325540]
                                                            0
                                                            1)
                                                         l[6989586621679028560])
                                                      GHC.Types.True[3891110078048108586]
                                                      GHC.Types.True[3891110078048108586]
                                                      GHC.Types.False[3891110078048108556])
                                                   (GHC.Internal.TypeError.TypeError[3674937295934325098]
                                                      (GHC.Prim.CONSTRAINT[3674937295934324920]
                                                         (GHC.Types.BoxedRep[3891110078048108766]
                                                            GHC.Types.Lifted[3891110078048108808]))
                                                      (GHC.Internal.TypeError.:<>:[3891110078048108697]
                                                         (GHC.Internal.TypeError.:<>:[3891110078048108697]
                                                            (GHC.Internal.TypeError.:<>:[3891110078048108697]
                                                               (GHC.Internal.TypeError.Text[3891110078048108694]
                                                                  "Cannot satisfy: ")
                                                               (GHC.Internal.TypeError.ShowType[3891110078048108703]
                                                                  GHC.Num.Natural.Natural[3674937295934324786]
                                                                  (GHC.Internal.TypeNats.+[3674937295934325540]
                                                                     0
                                                                     1)))
                                                            (GHC.Internal.TypeError.Text[3891110078048108694]
                                                               " <= "))
                                                         (GHC.Internal.TypeError.ShowType[3891110078048108703]
                                                            GHC.Num.Natural.Natural[3674937295934324786]
                                                            l[6989586621679028560])))) ->
                  case Clash.Promoted.Nat.compareSNat[8214565720323788356][GlobalId]
                         @l[6989586621679028560]
                         @2
                         wild[6341068275337658369][LocalId]
                         (Clash.Promoted.Nat.SNat[8214565720323789862] @2
                            Test.table1[8214565720323804889][GlobalId]) of
                    Clash.Promoted.Nat.SNatLE[8214565720323789865]
                      (irred1[6989586621679026887] :: GHC.Internal.TypeError.Assert[8214565720323788133]
                                                        (GHC.Internal.Data.Type.Ord.OrdCond[8214565720323788087]
                                                           GHC.Types.Bool[3674937295934324744]
                                                           (GHC.Internal.Data.Type.Ord.Compare[8214565720323788094]
                                                              GHC.Num.Natural.Natural[3674937295934324786]
                                                              l[6989586621679028560]
                                                              2)
                                                           GHC.Types.True[3891110078048108586]
                                                           GHC.Types.True[3891110078048108586]
                                                           GHC.Types.False[3891110078048108556])
                                                        (GHC.Internal.TypeError.TypeError[3674937295934325098]
                                                           (GHC.Prim.CONSTRAINT[3674937295934324920]
                                                              (GHC.Types.BoxedRep[3891110078048108766]
                                                                 GHC.Types.Lifted[3891110078048108808]))
                                                           (GHC.Internal.TypeError.:<>:[3891110078048108697]
                                                              (GHC.Internal.TypeError.:<>:[3891110078048108697]
                                                                 (GHC.Internal.TypeError.:<>:[3891110078048108697]
                                                                    (GHC.Internal.TypeError.Text[3891110078048108694]
                                                                       "Cannot satisfy: ")
                                                                    (GHC.Internal.TypeError.ShowType[3891110078048108703]
                                                                       GHC.Num.Natural.Natural[3674937295934324786]
                                                                       l[6989586621679028560]))
                                                                 (GHC.Internal.TypeError.Text[3891110078048108694]
                                                                    " <= "))
                                                              (GHC.Internal.TypeError.ShowType[3891110078048108703]
                                                                 GHC.Num.Natural.Natural[3674937295934324786]
                                                                 2)))) ->
                      case Clash.Sized.Vector.splitAt
                             @(GHC.Internal.TypeNats.-[3674937295934325546]
                                 l[6989586621679028560]
                                 1)
                             @(GHC.Internal.TypeNats.+[3674937295934325540]
                                 (GHC.Internal.TypeNats.-[3674937295934325546]
                                    2
                                    l[6989586621679028560])
                                 1)
                             @Clash.Sized.Internal.BitVector.Bit[8214565720323789991]
                             (Clash.Promoted.Nat.SNat[8214565720323789862]
                                @(GHC.Internal.TypeNats.-[3674937295934325546]
                                    l[6989586621679028560]
                                    1)
                                (GHC.TypeLits.KnownNat.$w$cnatSing2[8214565720323787727][GlobalId]
                                   @l[6989586621679028560]
                                   @1
                                   $dKnownNat[6989586621679026853][LocalId]
                                   (GHC.Num.Natural.NS 1##)))
                             Test.table[8214565720323799906][GlobalId] of
                        GHC.Tuple.(,)[3963167672086036486]
                          (ds1[6989586621679029873] :: Clash.Sized.Vector.Vec[8214565720323790002]
                                                         (GHC.Internal.TypeNats.-[3674937295934325546]
                                                            l[6989586621679028560]
                                                            1)
                                                         Clash.Sized.Internal.BitVector.Bit[8214565720323789991])
                            (y[6989586621679029874] :: Clash.Sized.Vector.Vec[8214565720323790002]
                                                         (GHC.Internal.TypeNats.+[3674937295934325540]
                                                            (GHC.Internal.TypeNats.-[3674937295934325546]
                                                               2
                                                               l[6989586621679028560])
                                                            1)
                                                         Clash.Sized.Internal.BitVector.Bit[8214565720323789991]) ->
                          Clash.Sized.Vector.head
                            @(GHC.Internal.TypeNats.-[3674937295934325546]
                                2
                                l[6989586621679028560])
                            @Clash.Sized.Internal.BitVector.Bit[8214565720323789991]
                            y[6989586621679029874][LocalId]
                    Clash.Promoted.Nat.SNatGT[8214565720323789864]
                      (irred1[6989586621679026900] :: GHC.Internal.TypeError.Assert[8214565720323788133]
                                                        (GHC.Internal.Data.Type.Ord.OrdCond[8214565720323788087]
                                                           GHC.Types.Bool[3674937295934324744]
                                                           (GHC.Internal.Data.Type.Ord.Compare[8214565720323788094]
                                                              GHC.Num.Natural.Natural[3674937295934324786]
                                                              (GHC.Internal.TypeNats.+[3674937295934325540]
                                                                 2
                                                                 1)
                                                              l[6989586621679028560])
                                                           GHC.Types.True[3891110078048108586]
                                                           GHC.Types.True[3891110078048108586]
                                                           GHC.Types.False[3891110078048108556])
                                                        (GHC.Internal.TypeError.TypeError[3674937295934325098]
                                                           (GHC.Prim.CONSTRAINT[3674937295934324920]
                                                              (GHC.Types.BoxedRep[3891110078048108766]
                                                                 GHC.Types.Lifted[3891110078048108808]))
                                                           (GHC.Internal.TypeError.:<>:[3891110078048108697]
                                                              (GHC.Internal.TypeError.:<>:[3891110078048108697]
                                                                 (GHC.Internal.TypeError.:<>:[3891110078048108697]
                                                                    (GHC.Internal.TypeError.Text[3891110078048108694]
                                                                       "Cannot satisfy: ")
                                                                    (GHC.Internal.TypeError.ShowType[3891110078048108703]
                                                                       GHC.Num.Natural.Natural[3674937295934324786]
                                                                       (GHC.Internal.TypeNats.+[3674937295934325540]
                                                                          2
                                                                          1)))
                                                                 (GHC.Internal.TypeError.Text[3891110078048108694]
                                                                    " <= "))
                                                              (GHC.Internal.TypeError.ShowType[3891110078048108703]
                                                                 GHC.Num.Natural.Natural[3674937295934324786]
                                                                 l[6989586621679028560])))) ->
                      GHC.Internal.Err.error
                        @(GHC.Types.BoxedRep[3891110078048108766]
                            GHC.Types.Lifted[3891110078048108808])
                        @Clash.Sized.Internal.BitVector.Bit[8214565720323789991]
                        (GHC.Internal.Stack.Types.PushCallStack[8214565720323790558]
                           (GHC.CString.unpackCString# "error")
                           (GHC.Internal.Stack.Types.SrcLoc[3891110078048108655]
                              (GHC.CString.unpackCString#
                                 Test.$trModule4[8214565720323804888][GlobalId])
                              (GHC.CString.unpackCString#
                                 Test.$trModule2[8214565720323804886][GlobalId])
                              (GHC.CString.unpackCString# "/tmp/Test.hs")
                              (GHC.Types.I# 22#)
                              (GHC.Types.I# 17#)
                              (GHC.Types.I# 22#)
                              (GHC.Types.I# 22#))
                           GHC.Internal.Stack.Types.EmptyCallStack[8214565720323801273])
                        (GHC.CString.unpackCString# "impossible"))
       xs'[6989586621679028563][LocalId])
     ((Λb[6989586621679026138] ->
        Clash.Sized.Vector.Nil[8214565720323790006] @0
          @b[6989586621679026138]
          (_CO_
             @(GHC.Prim.~#[3674937295934324842]
                 GHC.Num.Natural.Natural[3674937295934324786]
                 GHC.Num.Natural.Natural[3674937295934324786]
                 0
                 0)))
        @Clash.Sized.Internal.BitVector.Bit[8214565720323789991])
     (Clash.Sized.Vector.reverse @2
        @GHC.Tuple.Unit[3746994889972252672]
        (Clash.Sized.Vector.replicate @2
           @GHC.Tuple.Unit[3746994889972252672]
           (Clash.Promoted.Nat.SNat[8214565720323789862] @2
              Test.table1[8214565720323804889][GlobalId])
           GHC.Tuple.()[3963167672086036480])))

My guess is that the problem is introduced by the recursive call to table[8214565720323799906] in the splitAt call, which results from the at call in the example above.

@kleinreact
Copy link
Member Author

Moving the local definitions to the top level also seems to solve the issue, as the following terminates as expected

type Size = 2

topEntity :: Bit
topEntity = head lookupTable

lookupTable :: Vec Size Bit
lookupTable = smap fill $ repeat ()

fill :: forall n. SNat n -> () -> Bit
fill n@(SNat :: SNat n) _ = case compareSNat n (SNat @0) of
  SNatLE -> low
  SNatGT -> case compareSNat n (SNat @Size) of
    SNatLE -> at @(n - 1) @(Size - n) SNat lookupTable
    SNatGT -> error "impossible"

@kleinreact
Copy link
Member Author

Adding a {-# NOINLINE fill #-} also makes it work.

@christiaanb
Copy link
Member

christiaanb commented Oct 29, 2024 •
edited
Loading

The problem again seems to start in the same place as #2831 (comment)

Where caseCon will not reduce the case-expression of the form:

case compareSNat d0 d0 of ...

because the subject of the case expression is not a data constructor nor a primitive.

As a result, the Clash compiler will evaluate both the subject and the alternatives in "parallel". This then causes the at @1 @1 (SNat @1 1) lookuptable to be expanced forever, as the branch is never pruned before the "parallel" evaluation of the subject and the alternatives is again performed.

# for free to join this conversation on GitHub. Already have an account? # to comment
Assignees
No one assigned
Labels
bug
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@christiaanb @kleinreact