aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2019-05-20 12:51:26 +0100
committerYann Herklotz <git@yannherklotz.com>2019-05-20 12:51:26 +0100
commita6c69c67a9d3923443fccad77293c365f4bbc0d3 (patch)
tree8e11bec1a75f80a7fbbd713b6867c7ad2ba086cb
parentb72c905c718ff52e623b748034d567cf8552b50e (diff)
parent9a051648695d459d4564be58ae4850e159cb3ba3 (diff)
downloadverismith-a6c69c67a9d3923443fccad77293c365f4bbc0d3.tar.gz
verismith-a6c69c67a9d3923443fccad77293c365f4bbc0d3.zip
Merge branch 'master' of github.com:ymherklotz/verifuzz
-rw-r--r--src/VeriFuzz/Reduce.hs14
-rw-r--r--src/VeriFuzz/Report.hs78
-rw-r--r--test/Property.hs17
3 files changed, 66 insertions, 43 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 5882144..2edd31e 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,62 @@ 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
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
]