diff options
-rw-r--r-- | app/Main.hs | 16 | ||||
-rw-r--r-- | src/VeriFuzz.hs | 4 | ||||
-rw-r--r-- | src/VeriFuzz/ASTGen.hs | 1 | ||||
-rw-r--r-- | src/VeriFuzz/Env.hs | 4 | ||||
-rw-r--r-- | src/VeriFuzz/Gen.hs | 27 | ||||
-rw-r--r-- | src/VeriFuzz/Icarus.hs | 13 | ||||
-rw-r--r-- | src/VeriFuzz/Internal.hs | 5 | ||||
-rw-r--r-- | src/VeriFuzz/Internal/AST.hs (renamed from src/VeriFuzz/Helpers.hs) | 4 | ||||
-rw-r--r-- | src/VeriFuzz/Internal/Simulator.hs | 13 | ||||
-rw-r--r-- | src/VeriFuzz/Random.hs | 9 | ||||
-rw-r--r-- | src/VeriFuzz/XST.hs | 16 | ||||
-rw-r--r-- | src/VeriFuzz/Yosys.hs | 17 | ||||
-rw-r--r-- | test/Property.hs | 2 | ||||
-rw-r--r-- | verifuzz.cabal | 5 |
14 files changed, 74 insertions, 62 deletions
diff --git a/app/Main.hs b/app/Main.hs index ba0e306..d1b6bb2 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -14,7 +14,7 @@ import Shelly import Test.QuickCheck (Gen) import qualified Test.QuickCheck as QC import VeriFuzz -import qualified VeriFuzz.Graph.RandomAlt as V +import qualified VeriFuzz.RandomAlt as V myForkIO :: IO () -> IO (MVar ()) myForkIO io = do @@ -57,17 +57,9 @@ onFailure t _ = do cd ".." cp_r (fromText t) $ fromText (t <> "_failed") -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 :: Gen ModDecl -> Text -> Int -> IO () runEquivalence gm t i = do - m <- gm + m <- QC.generate gm shellyFailDir $ do mkdir_p (fromText "equiv" </> fromText n) curr <- toTextIgnore <$> pwd @@ -86,5 +78,5 @@ main :: IO () main = do num <- getNumCapabilities vars <- sequence $ (\x -> myForkIO $ - runEquivalence ("test_" <> T.pack (show x)) 0) <$> [1..num] + runEquivalence fromGraph ("test_" <> T.pack (show x)) 0) <$> [1..num] sequence_ $ takeMVar <$> vars diff --git a/src/VeriFuzz.hs b/src/VeriFuzz.hs index edf561b..d700d6d 100644 --- a/src/VeriFuzz.hs +++ b/src/VeriFuzz.hs @@ -16,12 +16,10 @@ module VeriFuzz , module VeriFuzz.Env , module VeriFuzz.Gen , module VeriFuzz.General - , module VeriFuzz.Helpers , module VeriFuzz.Icarus , module VeriFuzz.Internal , module VeriFuzz.Mutate , module VeriFuzz.Random - , module VeriFuzz.RandomAlt , module VeriFuzz.XST , module VeriFuzz.Yosys ) where @@ -33,11 +31,9 @@ import VeriFuzz.CodeGen import VeriFuzz.Env import VeriFuzz.Gen import VeriFuzz.General -import VeriFuzz.Helpers import VeriFuzz.Icarus import VeriFuzz.Internal import VeriFuzz.Mutate import VeriFuzz.Random -import VeriFuzz.RandomAlt import VeriFuzz.XST import VeriFuzz.Yosys diff --git a/src/VeriFuzz/ASTGen.hs b/src/VeriFuzz/ASTGen.hs index 5730f50..5d4d8bc 100644 --- a/src/VeriFuzz/ASTGen.hs +++ b/src/VeriFuzz/ASTGen.hs @@ -19,7 +19,6 @@ import qualified Data.Graph.Inductive as G import Data.Maybe (catMaybes) import VeriFuzz.AST import VeriFuzz.Circuit -import VeriFuzz.Helpers import VeriFuzz.Internal.Circuit -- | Converts a 'CNode' to an 'Identifier'. diff --git a/src/VeriFuzz/Env.hs b/src/VeriFuzz/Env.hs index a20fd2d..0bbd290 100644 --- a/src/VeriFuzz/Env.hs +++ b/src/VeriFuzz/Env.hs @@ -13,6 +13,8 @@ Environment to run the simulator and synthesisers in a matrix. module VeriFuzz.Env where import Control.Monad.Trans.Reader +import Prelude hiding (FilePath) +import Shelly import VeriFuzz.Icarus import VeriFuzz.XST import VeriFuzz.Yosys @@ -27,5 +29,5 @@ type SimEnv = ReaderT SimMatrix IO runAll :: SimEnv () runAll = do - val <- asks xst + _ <- asks xst shelly $ run_ "echo" ["Hello World"] diff --git a/src/VeriFuzz/Gen.hs b/src/VeriFuzz/Gen.hs index 90c42a9..56d48bf 100644 --- a/src/VeriFuzz/Gen.hs +++ b/src/VeriFuzz/Gen.hs @@ -12,24 +12,35 @@ Various useful generators. module VeriFuzz.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 +import Control.Lens +import qualified Data.Text as T +import Test.QuickCheck (Gen) +import qualified Test.QuickCheck as QC +import VeriFuzz.AST +import VeriFuzz.ASTGen +import VeriFuzz.Mutate +import VeriFuzz.Random + +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 randomMod :: Gen ModDecl randomMod = do let ids = Identifier . ("w"<>) . T.pack . show <$> [1..100] - moditems <- sequence $ randomAssigns ids + _ <- sequence $ randomAssigns ids return $ ModDecl "" [] [] [] fromGraph :: Gen ModDecl fromGraph = do - gr <- QC.generate $ rDups <$> QC.resize 100 (randomCircuit) + gr <- rDupsCirc <$> QC.resize 100 randomCircuit return $ initMod . head - $ (nestUpTo 5 . generateAST $ Circuit gr) + $ nestUpTo 5 (generateAST gr) ^.. getVerilogSrc . traverse . getDescription diff --git a/src/VeriFuzz/Icarus.hs b/src/VeriFuzz/Icarus.hs index fbcb657..8aa4698 100644 --- a/src/VeriFuzz/Icarus.hs +++ b/src/VeriFuzz/Icarus.hs @@ -13,15 +13,18 @@ Icarus verilog module. module VeriFuzz.Icarus where import Control.Lens -import Data.ByteString (ByteString) -import qualified Data.ByteString as B -import Data.Foldable (fold) +import Data.ByteString (ByteString) +import qualified Data.ByteString as B +import Data.Foldable (fold) import Data.Hashable -import Data.List (transpose) -import Prelude hiding (FilePath) +import Data.List (transpose) +import Prelude hiding (FilePath) import Shelly import VeriFuzz.AST +import VeriFuzz.CodeGen import VeriFuzz.General +import VeriFuzz.Internal.AST +import VeriFuzz.Mutate data Icarus = Icarus { icarusPath :: FilePath , vvpPath :: FilePath diff --git a/src/VeriFuzz/Internal.hs b/src/VeriFuzz/Internal.hs index 9136aba..6a880ee 100644 --- a/src/VeriFuzz/Internal.hs +++ b/src/VeriFuzz/Internal.hs @@ -13,12 +13,13 @@ Shared high level code used in the other modules internally. module VeriFuzz.Internal ( -- * Useful functions safe - -- * Circuit modules + -- * Module Specific Internals , module VeriFuzz.Internal.Circuit - -- * Simulator Internals , module VeriFuzz.Internal.Simulator + , module VeriFuzz.Internal.AST ) where +import VeriFuzz.Internal.AST import VeriFuzz.Internal.Circuit import VeriFuzz.Internal.Simulator diff --git a/src/VeriFuzz/Helpers.hs b/src/VeriFuzz/Internal/AST.hs index 09bb7dd..b8f569b 100644 --- a/src/VeriFuzz/Helpers.hs +++ b/src/VeriFuzz/Internal/AST.hs @@ -1,5 +1,5 @@ {-| -Module : VeriFuzz.Helpers +Module : VeriFuzz.Internal.AST Description : Defaults and common functions. Copyright : (c) 2018-2019, Yann Herklotz Grave License : BSD-3 @@ -10,7 +10,7 @@ Portability : POSIX Defaults and common functions. -} -module VeriFuzz.Helpers where +module VeriFuzz.Internal.AST where import Control.Lens import Data.Text (Text) diff --git a/src/VeriFuzz/Internal/Simulator.hs b/src/VeriFuzz/Internal/Simulator.hs index 4f8fd5a..0abdf8f 100644 --- a/src/VeriFuzz/Internal/Simulator.hs +++ b/src/VeriFuzz/Internal/Simulator.hs @@ -14,13 +14,14 @@ Template file for different configuration files. module VeriFuzz.Internal.Simulator where -import Data.Text (Text) -import qualified Data.Text as T -import Prelude hiding (FilePath) +import Data.Text (Text) +import qualified Data.Text as T +import Prelude hiding (FilePath) import Shelly -import Text.Shakespeare.Text (st) -import VeriFuzz.Simulator.General -import VeriFuzz.Verilog +import Text.Shakespeare.Text (st) +import VeriFuzz.AST +import VeriFuzz.General +import VeriFuzz.Internal.AST -- brittany-disable-next-binding yosysSatConfig :: (Simulator a, Simulator b) => a -> Maybe b -> ModDecl -> Text diff --git a/src/VeriFuzz/Random.hs b/src/VeriFuzz/Random.hs index a6684dd..9cfb570 100644 --- a/src/VeriFuzz/Random.hs +++ b/src/VeriFuzz/Random.hs @@ -18,6 +18,7 @@ import Data.Graph.Inductive.PatriciaTree (Gr) import Data.List (nub) import Test.QuickCheck (Arbitrary, Gen) import qualified Test.QuickCheck as QC +import VeriFuzz.Circuit dupFolder :: (Eq a, Eq b) => Context a b -> [Context a b] -> [Context a b] dupFolder cont ns = unique cont : ns @@ -27,6 +28,10 @@ dupFolder cont ns = unique cont : ns rDups :: (Eq a, Eq b) => Gr a b -> Gr a b rDups g = G.buildGr $ G.ufold dupFolder [] g +-- | Remove duplicates. +rDupsCirc :: Circuit -> Circuit +rDupsCirc = Circuit . rDups . getCircuit + -- | Gen instance to create an arbitrary edge, where the edges are limited by -- `n` that is passed to it. arbitraryEdge :: (Arbitrary e) => Int -> Gen (LEdge e) @@ -52,3 +57,7 @@ randomDAG = do -- | Generate a random acyclic DAG with an IO instance. genRandomDAG :: (Arbitrary l, Arbitrary e, Eq l, Eq e) => IO (Gr l e) genRandomDAG = QC.generate randomDAG + +-- | Generate a random circuit instead of a random graph +randomCircuit :: Gen Circuit +randomCircuit = Circuit <$> randomDAG diff --git a/src/VeriFuzz/XST.hs b/src/VeriFuzz/XST.hs index 2690882..3d745fe 100644 --- a/src/VeriFuzz/XST.hs +++ b/src/VeriFuzz/XST.hs @@ -14,16 +14,14 @@ Xst (ise) simulator implementation. module VeriFuzz.XST where -import Control.Lens hiding ((<.>)) -import qualified Data.Text as T -import Prelude hiding (FilePath) +import Prelude hiding (FilePath) import Shelly -import System.FilePath.Posix (takeBaseName) -import Text.Shakespeare.Text (st) -import VeriFuzz.Simulator.General -import VeriFuzz.Simulator.Internal.Template -import VeriFuzz.Verilog -import VeriFuzz.Verilog +import Text.Shakespeare.Text (st) +import VeriFuzz.AST +import VeriFuzz.CodeGen +import VeriFuzz.General +import VeriFuzz.Internal.AST +import VeriFuzz.Internal.Simulator data Xst = Xst { xstPath :: FilePath , netgenPath :: FilePath diff --git a/src/VeriFuzz/Yosys.hs b/src/VeriFuzz/Yosys.hs index c0eecb5..676e1b0 100644 --- a/src/VeriFuzz/Yosys.hs +++ b/src/VeriFuzz/Yosys.hs @@ -14,15 +14,14 @@ Yosys simulator implementation. module VeriFuzz.Yosys where -import Data.Maybe (fromMaybe) -import Data.Text (Text) -import qualified Data.Text as T -import Prelude hiding (FilePath) +import Prelude hiding (FilePath) import Shelly -import Text.Shakespeare.Text (st) -import VeriFuzz.Simulator.General -import VeriFuzz.Simulator.Internal.Template -import VeriFuzz.Verilog +import Text.Shakespeare.Text (st) +import VeriFuzz.AST +import VeriFuzz.CodeGen +import VeriFuzz.General +import VeriFuzz.Internal.Simulator +import VeriFuzz.Mutate newtype Yosys = Yosys { yosysPath :: FilePath } @@ -71,7 +70,7 @@ runEquivYosys yosys sim1 sim2 m = do checkFile = fromText [st|test.#{toText sim1}.#{maybe "rtl" toText sim2}.ys|] runEquiv :: (Synthesize a, Synthesize b) => Yosys -> a -> Maybe b -> ModDecl -> Sh () -runEquiv yosys sim1 sim2 m = do +runEquiv _ sim1 sim2 m = do root <- rootPath writefile "top.v" . genSource . initMod $ makeTopAssert m writefile "test.sby" $ sbyConfig root sim1 sim2 m diff --git a/test/Property.hs b/test/Property.hs index c6ca390..2c8abc9 100644 --- a/test/Property.hs +++ b/test/Property.hs @@ -8,7 +8,7 @@ import Data.Graph.Inductive.PatriciaTree (Gr) import Test.Tasty import qualified Test.Tasty.QuickCheck as QC import VeriFuzz -import qualified VeriFuzz.Graph.RandomAlt as V +import qualified VeriFuzz.RandomAlt as V newtype TestGraph = TestGraph { getGraph :: Gr Gate () } deriving (Show) diff --git a/verifuzz.cabal b/verifuzz.cabal index f99faaa..470ee5d 100644 --- a/verifuzz.cabal +++ b/verifuzz.cabal @@ -24,14 +24,15 @@ library other-modules: VeriFuzz.Internal , VeriFuzz.Internal.Circuit , VeriFuzz.Internal.Simulator - exposed-modules: VeriFuzz.ASTGen + , VeriFuzz.Internal.AST + exposed-modules: VeriFuzz + , VeriFuzz.ASTGen , VeriFuzz.AST , VeriFuzz.Circuit , VeriFuzz.CodeGen , VeriFuzz.Env , VeriFuzz.General , VeriFuzz.Gen - , VeriFuzz.Helpers , VeriFuzz.Icarus , VeriFuzz.Mutate , VeriFuzz.RandomAlt |