From 9a051648695d459d4564be58ae4850e159cb3ba3 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 19 May 2019 18:17:10 +0100 Subject: Change simple graph check to acyclic check --- src/VeriFuzz/Reduce.hs | 14 +++++++------ src/VeriFuzz/Report.hs | 53 ++++++++++++++++++++++++++++++-------------------- test/Property.hs | 17 +++++++++++----- 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 ] -- cgit