Change simple graph check to acyclic check

3 files changed, 52 insertions, 32 deletions

diff --git a/src/VeriFuzz/Reduce.hs b/src/VeriFuzz/Reduce.hs
index d8a23ad..33cb648 100644
--- a/src/VeriFuzz/Reduce.hs
+++ b/src/VeriFuzz/Reduce.hs
@@ -282,11 +282,12 @@ fixModInst (SourceInfo _ (Verilog decl)) (ModInst n g i) = case m of
     Just m' -> ModInst n g . mapMaybe (fixModInst' m') $ zip i [0 ..]
   where
     m = safe head $ filter (isModule n) decl
-    fixModInst' (ModDecl _ o i' _ _) (ModConn e, n') | n' < length o + length i' = Just $ ModConn e
-                                                    | otherwise     = Nothing
+    fixModInst' (ModDecl _ o i' _ _) (ModConn e, n')
+        | n' < length o + length i' = Just $ ModConn e
+        | otherwise                 = Nothing
     fixModInst' (ModDecl _ o i'' _ _) (ModConnNamed i' e, _)
         | i' `elem` fmap _portName (o <> i'') = Just $ ModConnNamed i' e
-        | otherwise                  = Nothing
+        | otherwise                           = Nothing
 fixModInst _ a = a
 
 findActiveWires :: Identifier -> SourceInfo -> [Identifier]
@@ -466,11 +467,12 @@ removeDecl src = foldr fix removed allMods
   where
     removeDecl' t src' =
         src'
-            & (\a -> a & aModule t . modItems %~ filter (isUsedDecl (used <> findActiveWires t a)))
+            & (\a -> a & aModule t . modItems %~ filter
+                  (isUsedDecl (used <> findActiveWires t a))
+              )
             . (aModule t . modParams %~ filter (isUsedParam used))
             . (aModule t . modInPorts %~ filter (isUsedPort used))
-      where
-        used = nub $ allExprIds (src' ^. aModule t)
+        where used = nub $ allExprIds (src' ^. aModule t)
     allMods = src ^.. infoSrc . _Wrapped . traverse . modId
     fix t a = a & aModule t . modItems %~ fmap (fixModInst a)
     removed = foldr removeDecl' src allMods
diff --git a/src/VeriFuzz/Report.hs b/src/VeriFuzz/Report.hs
index b20fdcb..2edd31e 100644
--- a/src/VeriFuzz/Report.hs
+++ b/src/VeriFuzz/Report.hs
@@ -234,28 +234,39 @@ resultReport :: Text -> FuzzReport -> Html
 resultReport name (FuzzReport synth _ stat) = H.docTypeHtml $ do
     H.head $ do
         H.title $ "Fuzz Report - " <> H.toHtml name
-        H.meta ! A.name "viewport" ! A.content "width=device-width, initial-scale=1"
+        H.meta ! A.name "viewport" ! A.content
+            "width=device-width, initial-scale=1"
         H.meta ! A.charset "utf8"
-        H.link ! A.rel "stylesheet" ! A.href "https://cdnjs.cloudflare.com/ajax/libs/bulma/0.7.4/css/bulma.min.css"
-    H.body . (H.section ! A.class_ "section") . (H.div ! A.class_ "container") $ do
-        H.h1 ! A.class_ "title" $ "Fuzz Report - " <> H.toHtml name
-        H.h2 ! A.class_ "subtitle" $ "Synthesis Failure"
-        H.table ! A.class_ "table" $ do
-            H.thead . H.toHtml $ ( H.tr
-                                   . H.toHtml
-                                   $ [H.th "Synthesis tool", H.th "Synthesis Status"]
-                                 )
-            H.tbody . H.toHtml $ fmap synthStatusHtml stat
-        H.h2 ! A.class_ "subtitle" $ "Equivalence Check Status"
-        H.table ! A.class_ "table" $ do
-            H.thead . H.toHtml $ ( H.tr
-                                   . H.toHtml
-                                   $ [ H.th "First tool"
-                                     , H.th "Second tool"
-                                     , H.th "Equivalence Status"
-                                     ]
-                                 )
-            H.tbody . H.toHtml $ fmap synthResultHtml synth
+        H.link
+            ! A.rel "stylesheet"
+            ! A.href
+                  "https://cdnjs.cloudflare.com/ajax/libs/bulma/0.7.4/css/bulma.min.css"
+    H.body
+        . (H.section ! A.class_ "section")
+        . (H.div ! A.class_ "container")
+        $ do
+              H.h1 ! A.class_ "title" $ "Fuzz Report - " <> H.toHtml name
+              H.h2 ! A.class_ "subtitle" $ "Synthesis Failure"
+              H.table ! A.class_ "table" $ do
+                  H.thead
+                      . H.toHtml
+                      $ ( H.tr
+                        . H.toHtml
+                        $ [H.th "Synthesis tool", H.th "Synthesis Status"]
+                        )
+                  H.tbody . H.toHtml $ fmap synthStatusHtml stat
+              H.h2 ! A.class_ "subtitle" $ "Equivalence Check Status"
+              H.table ! A.class_ "table" $ do
+                  H.thead
+                      . H.toHtml
+                      $ ( H.tr
+                        . H.toHtml
+                        $ [ H.th "First tool"
+                          , H.th "Second tool"
+                          , H.th "Equivalence Status"
+                          ]
+                        )
+                  H.tbody . H.toHtml $ fmap synthResultHtml synth
 
 printResultReport :: Text -> FuzzReport -> Text
 printResultReport t f = toStrict . renderHtml $ resultReport t f
diff --git a/test/Property.hs b/test/Property.hs
index 7b1771c..001c7d3 100644
--- a/test/Property.hs
+++ b/test/Property.hs
@@ -32,11 +32,18 @@ import           VeriFuzz.Verilog.Parser
 randomDAG' :: Gen Circuit
 randomDAG' = Hog.resize 30 randomDAG
 
-simpleGraph :: Property
-simpleGraph = Hog.property $ do
+acyclicGraph :: Property
+acyclicGraph = Hog.property $ do
     xs <- Hog.forAllWith (const "") randomDAG'
     Hog.assert $ simp xs
-    where simp = G.isSimple . getCircuit
+  where
+    simp g =
+        (== G.noNodes (getCircuit g))
+            . sum
+            . fmap length
+            . G.scc
+            . getCircuit
+            $ g
 
 type GenFunctor f a b c =
     ( Functor f
@@ -76,7 +83,7 @@ propertyResultInterrupted = do
 propertyTests :: TestTree
 propertyTests = testGroup
     "Property Tests"
-    [ testProperty "simple graph generation check" simpleGraph
-    , testProperty "fmap for Result"               propertyResultInterrupted
+    [ testProperty "acyclic graph generation check" acyclicGraph
+    , testProperty "fmap for Result"                propertyResultInterrupted
     , parserTests
     ]