search

blarney-lang / blarney

Haskell library for hardware description
Other
98 stars 11 forks source link

Incorrect verification #130

Closed Swire42 closed 6 months ago

Swire42 commented 6 months ago

There seems to be an issue with (at least) the restricted state verification. Using the following file (in a template-project context):

import Blarney

notId :: Bit 1 -> Bit 1
notId x = s
  where
    s = x .^. c
    p = delay 0 $ delay 1 p
    c = delay 0 (p .&. s)

prop :: Bit 1 -> Action ()
prop x = assert (notId x === x) "notId === id"

main :: IO ()
main = do
  verifyWith cnfNoRestr prop
  verifyWith cnfRestr prop
  where
    cnfRestr = dfltVerifyConf { verifyConfMode = Induction (IncreaseFrom 1) True }
    cnfNoRestr = dfltVerifyConf { verifyConfMode = Induction (IncreaseFrom 1) False }

I get:

Assertion: notId === id
restricted states: disabled
(depth 1) bounded ............ valid
(depth 1) induction step ..... falsifiable
(depth 2) bounded ............ valid
(depth 2) induction step ..... falsifiable
(depth 3) bounded ............ falsifiable
not verified
Assertion: notId === id
restricted states: enabled
(depth 1) bounded ............ valid
(depth 1) induction step ..... falsifiable
(depth 2) bounded ............ valid
(depth 2) induction step ..... valid
verified

The restricted state: disabled result is correct, but the restricted state: enabled is incorrect.

The issue might also be happening with non-restricted states induction, since on this example it is bounded that rejects the property.