diff options
-rw-r--r-- | app/Main.hs | 28 | ||||
-rw-r--r-- | src/VeriFuzz/Circuit/ASTGen.hs (renamed from src/VeriFuzz/Graph/ASTGen.hs) | 4 | ||||
-rw-r--r-- | src/VeriFuzz/Circuit/CodeGen.hs (renamed from src/VeriFuzz/Graph/CodeGen.hs) | 4 | ||||
-rw-r--r-- | src/VeriFuzz/Circuit/Random.hs (renamed from src/VeriFuzz/Graph/Random.hs) | 4 | ||||
-rw-r--r-- | src/VeriFuzz/Circuit/RandomAlt.hs (renamed from src/VeriFuzz/Graph/RandomAlt.hs) | 4 | ||||
-rw-r--r-- | src/VeriFuzz/Gen.hs | 35 | ||||
-rw-r--r-- | src/VeriFuzz/Internal.hs (renamed from src/VeriFuzz/Internal/Shared.hs) | 4 | ||||
-rw-r--r-- | src/VeriFuzz/Internal/Circuit.hs (renamed from src/VeriFuzz/Internal/Gen.hs) | 4 | ||||
-rw-r--r-- | src/VeriFuzz/Internal/Simulator.hs (renamed from src/VeriFuzz/Simulator/Internal/Template.hs) | 4 |
9 files changed, 65 insertions, 26 deletions
diff --git a/app/Main.hs b/app/Main.hs index 3bb9d9f..ba0e306 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -11,6 +11,7 @@ import qualified Data.Text as T import Numeric (showHex) import Prelude hiding (FilePath) import Shelly +import Test.QuickCheck (Gen) import qualified Test.QuickCheck as QC import VeriFuzz import qualified VeriFuzz.Graph.RandomAlt as V @@ -56,24 +57,27 @@ onFailure t _ = do cd ".." cp_r (fromText t) $ fromText (t <> "_failed") -runEquivalence :: Text -> Int -> IO () -runEquivalence t i = do - gr <- QC.generate $ rDups <$> QC.resize 100 (randomDAG :: QC.Gen (G.Gr Gate ())) - let circ = - initMod - . head - $ (nestUpTo 5 . generateAST $ Circuit gr) - ^.. getVerilogSrc - . traverse - . getDescription +random :: [Identifier] -> (Expr -> ContAssign) -> Gen ModItem +random ctx fun = do + expr <- QC.sized (exprWithContext ctx) + return . ModCA $ fun expr + +randomAssigns :: [Identifier] -> [Gen ModItem] +randomAssigns ids = random ids . ContAssign <$> ids + +runEquivalence :: IO ModDecl -> Text -> Int -> IO () +runEquivalence gm t i = do + m <- gm shellyFailDir $ do mkdir_p (fromText "equiv" </> fromText n) curr <- toTextIgnore <$> pwd setenv "VERIFUZZ_ROOT" curr cd (fromText "equiv" </> fromText n) - catch_sh (runEquiv defaultYosys defaultYosys (Just defaultXst) circ >> echoP "OK") $ onFailure n + catch_sh (runEquiv defaultYosys defaultYosys + (Just defaultXst) m >> echoP "OK") $ + onFailure n cd ".." - when (i < 5) (runEquivalence t $ i+1) + when (i < 5) (runEquivalence gm t $ i+1) where n = t <> "_" <> T.pack (show i) diff --git a/src/VeriFuzz/Graph/ASTGen.hs b/src/VeriFuzz/Circuit/ASTGen.hs index 745d849..41f905d 100644 --- a/src/VeriFuzz/Graph/ASTGen.hs +++ b/src/VeriFuzz/Circuit/ASTGen.hs @@ -1,5 +1,5 @@ {-| -Module : VeriFuzz.Graph.ASTGen +Module : VeriFuzz.Circuit.ASTGen Description : Generates the AST from the graph directly. Copyright : (c) 2018-2019, Yann Herklotz Grave License : BSD-3 @@ -10,7 +10,7 @@ Portability : POSIX Generates the AST from the graph directly. -} -module VeriFuzz.Graph.ASTGen where +module VeriFuzz.Circuit.ASTGen where import Control.Lens ((^..)) import Data.Foldable (fold) diff --git a/src/VeriFuzz/Graph/CodeGen.hs b/src/VeriFuzz/Circuit/CodeGen.hs index 20c354a..91da48c 100644 --- a/src/VeriFuzz/Graph/CodeGen.hs +++ b/src/VeriFuzz/Circuit/CodeGen.hs @@ -1,5 +1,5 @@ {-| -Module : VeriFuzz.Graph.Random +Module : VeriFuzz.Circuit.Random Description : Code generation directly from DAG. Copyright : (c) 2018-2019, Yann Herklotz Grave License : BSD-3 @@ -10,7 +10,7 @@ Portability : POSIX Define the code generation directly from the random DAG. -} -module VeriFuzz.Graph.CodeGen +module VeriFuzz.Circuit.CodeGen ( generate ) where diff --git a/src/VeriFuzz/Graph/Random.hs b/src/VeriFuzz/Circuit/Random.hs index f5a8d6f..7989b49 100644 --- a/src/VeriFuzz/Graph/Random.hs +++ b/src/VeriFuzz/Circuit/Random.hs @@ -1,5 +1,5 @@ {-| -Module : VeriFuzz.Graph.Random +Module : VeriFuzz.Circuit.Random Description : Random generation for DAG Copyright : (c) 2018-2019, Yann Herklotz Grave License : BSD-3 @@ -10,7 +10,7 @@ Portability : POSIX Define the random generation for the directed acyclic graph. -} -module VeriFuzz.Graph.Random where +module VeriFuzz.Circuit.Random where import Data.Graph.Inductive (Context, LEdge) import qualified Data.Graph.Inductive as G diff --git a/src/VeriFuzz/Graph/RandomAlt.hs b/src/VeriFuzz/Circuit/RandomAlt.hs index e6d16bb..93a50e9 100644 --- a/src/VeriFuzz/Graph/RandomAlt.hs +++ b/src/VeriFuzz/Circuit/RandomAlt.hs @@ -1,5 +1,5 @@ {-|p -Module : VeriFuzz.Graph.RandomAlt +Module : VeriFuzz.Circuit.RandomAlt Description : RandomAlt generation for DAG Copyright : (c) 2018-2019, Yann Herklotz Grave License : BSD-3 @@ -10,7 +10,7 @@ Portability : POSIX Define the random generation for the directed acyclic graph. -} -module VeriFuzz.Graph.RandomAlt where +module VeriFuzz.Circuit.RandomAlt where import qualified Data.Graph.Inductive.Arbitrary as G import Data.Graph.Inductive.PatriciaTree (Gr) diff --git a/src/VeriFuzz/Gen.hs b/src/VeriFuzz/Gen.hs new file mode 100644 index 0000000..d3e356d --- /dev/null +++ b/src/VeriFuzz/Gen.hs @@ -0,0 +1,35 @@ +{-| +Module : VeriFuzz.Verilog.Gen +Description : Various useful generators. +Copyright : (c) 2019, Yann Herklotz Grave +License : GPL-3 +Maintainer : ymherklotz [at] gmail [dot] com +Stability : experimental +Portability : POSIX + +Various useful generators. +-} + +module VeriFuzz.Verilog.Gen where + +import qualified Data.Text as T +import Test.QuickCheck (Arbitrary, Gen, arbitrary) +import qualified Test.QuickCheck as QC +import VeriFuzz.Circuit +import VeriFuzz.Verilog + +randomMod :: Gen ModDecl +randomMod = do + let ids = Identifier . ("w"<>) . T.pack . show <$> [1..100] + moditems <- sequence $ randomAssigns ids + return $ ModDecl "" [] [] [] + +fromGraph :: Gen ModDecl +fromGraph = do + gr <- QC.generate $ rDups <$> QC.resize 100 (randomCircuit) + return $ initMod + . head + $ (nestUpTo 5 . generateAST $ Circuit gr) + ^.. getVerilogSrc + . traverse + . getDescription diff --git a/src/VeriFuzz/Internal/Shared.hs b/src/VeriFuzz/Internal.hs index c7d2760..1adbc84 100644 --- a/src/VeriFuzz/Internal/Shared.hs +++ b/src/VeriFuzz/Internal.hs @@ -1,5 +1,5 @@ {-| -Module : VeriFuzz.Internal.Shared +Module : VeriFuzz.Internal Description : Shared high level code used in the other modules internally. Copyright : (c) 2018-2019, Yann Herklotz Grave License : BSD-3 @@ -10,7 +10,7 @@ Portability : POSIX Shared high level code used in the other modules internally. -} -module VeriFuzz.Internal.Shared where +module VeriFuzz.Internal where -- | Converts unsafe list functions in the Prelude to a safe version. safe :: ([a] -> b) -> [a] -> Maybe b diff --git a/src/VeriFuzz/Internal/Gen.hs b/src/VeriFuzz/Internal/Circuit.hs index d2e4e3c..0634f01 100644 --- a/src/VeriFuzz/Internal/Gen.hs +++ b/src/VeriFuzz/Internal/Circuit.hs @@ -1,5 +1,5 @@ {-| -Module : VeriFuzz.Internal.Gen +Module : VeriFuzz.Internal.Circuit Description : Internal helpers for generation. Copyright : (c) 2018-2019, Yann Herklotz Grave License : BSD-3 @@ -10,7 +10,7 @@ Portability : POSIX Internal helpers for generation. -} -module VeriFuzz.Internal.Gen where +module VeriFuzz.Internal.Circuit where import Data.Graph.Inductive (Graph, Node) import qualified Data.Graph.Inductive as G diff --git a/src/VeriFuzz/Simulator/Internal/Template.hs b/src/VeriFuzz/Internal/Simulator.hs index 109c679..4f8fd5a 100644 --- a/src/VeriFuzz/Simulator/Internal/Template.hs +++ b/src/VeriFuzz/Internal/Simulator.hs @@ -1,5 +1,5 @@ {-| -Module : VeriFuzz.Simulator.Internal.Template +Module : VeriFuzz.Internal.Simulator Description : Template file for different configuration files Copyright : (c) 2019, Yann Herklotz Grave License : GPL-3 @@ -12,7 +12,7 @@ Template file for different configuration files. {-# LANGUAGE QuasiQuotes #-} -module VeriFuzz.Simulator.Internal.Template where +module VeriFuzz.Internal.Simulator where import Data.Text (Text) import qualified Data.Text as T |