From 4dc6b969dcd80f7ed05b2d18252785254fcc7963 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 18 May 2019 19:38:22 +0100 Subject: Add colour to the report --- src/VeriFuzz/Report.hs | 67 ++++++++++++++++++++++++++------------------------ 1 file changed, 35 insertions(+), 32 deletions(-) diff --git a/src/VeriFuzz/Report.hs b/src/VeriFuzz/Report.hs index 5882144..b20fdcb 100644 --- a/src/VeriFuzz/Report.hs +++ b/src/VeriFuzz/Report.hs @@ -41,9 +41,10 @@ import Data.Text (Text) import Data.Text.Lazy (toStrict) import Prelude hiding (FilePath) import Shelly (fromText) -import Text.Blaze.Html (Html) +import Text.Blaze.Html (Html, (!)) import Text.Blaze.Html.Renderer.Text (renderHtml) import qualified Text.Blaze.Html5 as H +import qualified Text.Blaze.Html5.Attributes as A import VeriFuzz.Config import VeriFuzz.Result import VeriFuzz.Sim @@ -210,49 +211,51 @@ descriptionToSynth s = error $ "Could not find implementation for synthesiser '" <> show s <> "'" status :: Result Failed () -> Html -status (Pass _ ) = "Passed" -status (Fail EmptyFail ) = "Failed" -status (Fail EquivFail ) = "Equivalence failed" -status (Fail SimFail ) = "Simulation failed" -status (Fail SynthFail ) = "Synthesis failed" -status (Fail EquivError ) = "Equivalence error" -status (Fail TimeoutError) = "Time out" +status (Pass _ ) = H.td ! A.class_ "is-success" $ "Passed" +status (Fail EmptyFail ) = H.td ! A.class_ "is-danger" $ "Failed" +status (Fail EquivFail ) = H.td ! A.class_ "is-danger" $ "Equivalence failed" +status (Fail SimFail ) = H.td ! A.class_ "is-danger" $ "Simulation failed" +status (Fail SynthFail ) = H.td ! A.class_ "is-danger" $ "Synthesis failed" +status (Fail EquivError ) = H.td ! A.class_ "is-danger" $ "Equivalence error" +status (Fail TimeoutError) = H.td ! A.class_ "is-warning" $ "Time out" synthStatusHtml :: SynthStatus -> Html synthStatusHtml (SynthStatus synth res) = H.tr $ do H.td . H.toHtml $ toText synth - H.td $ status res + status res synthResultHtml :: SynthResult -> Html synthResultHtml (SynthResult synth1 synth2 res) = H.tr $ do H.td . H.toHtml $ toText synth1 H.td . H.toHtml $ toText synth2 - H.td $ status res + status res resultReport :: Text -> FuzzReport -> Html resultReport name (FuzzReport synth _ stat) = H.docTypeHtml $ do - H.head . H.title $ "Fuzz Report - " <> H.toHtml name - H.body $ do - H.h1 $ "Fuzz Report - " <> H.toHtml name - H.h2 "Synthesis Failure" - H.table - . H.toHtml - $ ( H.tr - . H.toHtml - $ [H.th "Synthesis tool", H.th "Synthesis Status"] - ) - : fmap synthStatusHtml stat - H.h2 "Equivalence Check Status" - H.table - . H.toHtml - $ ( H.tr - . H.toHtml - $ [ H.th "First tool" - , H.th "Second tool" - , H.th "Equivalence Status" - ] - ) - : fmap synthResultHtml synth + 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.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 printResultReport :: Text -> FuzzReport -> Text printResultReport t f = toStrict . renderHtml $ resultReport t f -- cgit 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