Skip to content

Hedgehog found a counterexample in prop packet fifo id #131

@DigitalBrains1

Description

@DigitalBrains1
$ git status
On branch main
Your branch is up to date with 'origin/main'.

nothing to commit, working tree clean
$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 9.6.6
$ cabal v2-run clash-protocols:unittests -- --pattern '$NF ~ /prop packet fifo id/' --hedgehog-replay '196:bEhPz8BB6hZ3bb12Hz10BB2h3S12hIdA2bGPgv Seed 6375259335271169919 17161120250667971335'
[...]
Tests
  Protocols
    PacketStream
      Tests.Protocols.PacketStream.PacketFifo
        prop packet fifo id: FAIL (0.09s)
            ✗ prop_packet fifo id failed at src/Protocols/Hedgehog.hs:248:59
              after 196 tests and 70 shrinks.
[...]
Full output
$ git status
On branch main
Your branch is up to date with 'origin/main'.

nothing to commit, working tree clean
$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 9.6.6
$ cabal v2-run clash-protocols:unittests -- --pattern '$NF ~ /prop packet fifo id/' --hedgehog-replay '196:bEhPz8BB6hZ3bb12Hz10BB2h3S12hIdA2bGPgv Seed 6375259335271169919 17161120250667971335'
Configuration is affected by the following files:
- cabal.project
- cabal.project.local
Tests
  Protocols
    PacketStream
      Tests.Protocols.PacketStream.PacketFifo
        prop packet fifo id: FAIL (0.09s)
            ✗ prop_packet fifo id failed at src/Protocols/Hedgehog.hs:248:59
              after 196 tests and 70 shrinks.
              shrink path: 196:bEhPz8BB6hZ3bb12Hz10BB2h3S12hIdA2bGPgv
            
              forAll0 =
                ( StallWithNack , [] ) :> Nil
              
              forAll1 =
                NoStall :> Nil
              
              forAll2 =
                ( StallWithNack
                , [ 10
                  , 0
                  , 10
                  , 0
                  , 9
                  , 6
                  , 2
                  , 2
                  , 3
                  , 2
                  , 7
                  , 5
                  , 4
                  , 6
                  , 6
                  , 4
                  , 1
                  , 6
                  , 0
                  , 0
                  , 5
                  , 9
                  , 6
                  , 3
                  , 3
                  , 7
                  , 8
                  , 9
                  , 8
                  , 4
                  , 6
                  , 2
                  , 9
                  , 3
                  , 3
                  , 6
                  , 0
                  , 10
                  , 2
                  ]
                ) :>
                  Nil
              
              forAll3 =
                Stall :> Nil
              
              forAll4 =
                39
              
              forAll5 =
                [PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = True},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b...._.... :> Nil, _last = Just 0, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = True},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b...._.... :> Nil, _last = Just 0, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = True},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b...._.... :> Nil, _last = Just 0, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b...._.... :> Nil, _last = Just 0, _meta = -32768, _abort = False}]
            
              Failed
              ━━ lhs ━━
              [PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b0000_0000 :> Nil, _last = Nothing, _meta = -32768, _abort = False},PacketStreamM2S {_data = 0b...._.... :> Nil, _last = Just 0, _meta = -32768, _abort = False}]
              ━━ rhs ━━
              []
            
              This failure can be reproduced by running:
              > recheckAt (Seed 6375259335271169919 17161120250667971335) "196:bEhPz8BB6hZ3bb12Hz10BB2h3S12hIdA2bGPgv" prop_packet fifo id
            
          Use "--pattern '$NF ~ /prop packet fifo id/' --hedgehog-replay '196:bEhPz8BB6hZ3bb12Hz10BB2h3S12hIdA2bGPgv Seed 6375259335271169919 17161120250667971335'" to reproduce from the command-line.

Rowan wrote:

I expect it's because of the massive amounts of stalls.
That it just doesn't get around to sending data and times out.
Could you make an issue with this text (and critically the seed). I can take a look later

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions