From a38289ca9d96e97bc4e65b67c50f5805d56a3d86 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 1 Feb 2019 19:34:44 +0000 Subject: Structure changes --- src/VeriFuzz/Circuit/ASTGen.hs | 82 ++++++++++++++++++++++++++ src/VeriFuzz/Circuit/CodeGen.hs | 62 ++++++++++++++++++++ src/VeriFuzz/Circuit/Random.hs | 54 +++++++++++++++++ src/VeriFuzz/Circuit/RandomAlt.hs | 25 ++++++++ src/VeriFuzz/Gen.hs | 35 +++++++++++ src/VeriFuzz/Graph/ASTGen.hs | 82 -------------------------- src/VeriFuzz/Graph/CodeGen.hs | 62 -------------------- src/VeriFuzz/Graph/Random.hs | 54 ----------------- src/VeriFuzz/Graph/RandomAlt.hs | 25 -------- src/VeriFuzz/Internal.hs | 18 ++++++ src/VeriFuzz/Internal/Circuit.hs | 32 ++++++++++ src/VeriFuzz/Internal/Gen.hs | 32 ---------- src/VeriFuzz/Internal/Shared.hs | 18 ------ src/VeriFuzz/Internal/Simulator.hs | 90 +++++++++++++++++++++++++++++ src/VeriFuzz/Simulator/Internal/Template.hs | 90 ----------------------------- 15 files changed, 398 insertions(+), 363 deletions(-) create mode 100644 src/VeriFuzz/Circuit/ASTGen.hs create mode 100644 src/VeriFuzz/Circuit/CodeGen.hs create mode 100644 src/VeriFuzz/Circuit/Random.hs create mode 100644 src/VeriFuzz/Circuit/RandomAlt.hs create mode 100644 src/VeriFuzz/Gen.hs delete mode 100644 src/VeriFuzz/Graph/ASTGen.hs delete mode 100644 src/VeriFuzz/Graph/CodeGen.hs delete mode 100644 src/VeriFuzz/Graph/Random.hs delete mode 100644 src/VeriFuzz/Graph/RandomAlt.hs create mode 100644 src/VeriFuzz/Internal.hs create mode 100644 src/VeriFuzz/Internal/Circuit.hs delete mode 100644 src/VeriFuzz/Internal/Gen.hs delete mode 100644 src/VeriFuzz/Internal/Shared.hs create mode 100644 src/VeriFuzz/Internal/Simulator.hs delete mode 100644 src/VeriFuzz/Simulator/Internal/Template.hs (limited to 'src') diff --git a/src/VeriFuzz/Circuit/ASTGen.hs b/src/VeriFuzz/Circuit/ASTGen.hs new file mode 100644 index 0000000..41f905d --- /dev/null +++ b/src/VeriFuzz/Circuit/ASTGen.hs @@ -0,0 +1,82 @@ +{-| +Module : VeriFuzz.Circuit.ASTGen +Description : Generates the AST from the graph directly. +Copyright : (c) 2018-2019, Yann Herklotz Grave +License : BSD-3 +Maintainer : ymherklotz [at] gmail [dot] com +Stability : experimental +Portability : POSIX + +Generates the AST from the graph directly. +-} + +module VeriFuzz.Circuit.ASTGen where + +import Control.Lens ((^..)) +import Data.Foldable (fold) +import Data.Graph.Inductive (LNode, Node) +import qualified Data.Graph.Inductive as G +import Data.Maybe (catMaybes) +import VeriFuzz.Circuit +import VeriFuzz.Internal.Gen +import VeriFuzz.Verilog.AST +import VeriFuzz.Verilog.Helpers + +-- | Converts a 'CNode' to an 'Identifier'. +frNode :: Node -> Identifier +frNode = Identifier . fromNode + +-- | Converts a 'Gate' to a 'BinaryOperator', which should be a bijective +-- mapping. +fromGate :: Gate -> BinaryOperator +fromGate And = BinAnd +fromGate Or = BinOr +fromGate Xor = BinXor + +inputsC :: Circuit -> [Node] +inputsC c = inputs (getCircuit c) + +outputsC :: Circuit -> [Node] +outputsC c = outputs (getCircuit c) + +genPortsAST :: (Circuit -> [Node]) -> Circuit -> [Port] +genPortsAST f c = port . frNode <$> f c where port = Port Wire 4 + +-- | Generates the nested expression AST, so that it can then generate the +-- assignment expressions. +genAssignExpr :: Gate -> [Node] -> Maybe Expr +genAssignExpr _ [] = Nothing +genAssignExpr _ [n ] = Just . Id $ frNode n +genAssignExpr g (n : ns) = BinOp wire op <$> genAssignExpr g ns + where + wire = Id $ frNode n + op = fromGate g + +-- | Generate the continuous assignment AST for a particular node. If it does +-- not have any nodes that link to it then return 'Nothing', as that means that +-- the assignment will just be empty. +genContAssignAST :: Circuit -> LNode Gate -> Maybe ModItem +genContAssignAST c (n, g) = ModCA . ContAssign name <$> genAssignExpr g nodes + where + gr = getCircuit c + nodes = G.pre gr n + name = frNode n + +genAssignAST :: Circuit -> [ModItem] +genAssignAST c = catMaybes $ genContAssignAST c <$> nodes + where + gr = getCircuit c + nodes = G.labNodes gr + +genModuleDeclAST :: Circuit -> ModDecl +genModuleDeclAST c = ModDecl i output ports items + where + i = Identifier "gen_module" + ports = genPortsAST inputsC c + output = [Port Wire 90 "y"] + a = genAssignAST c + items = a ++ [ModCA . ContAssign "y" . fold $ Id <$> assigns] + assigns = a ^.. traverse . _ModCA . contAssignNetLVal + +generateAST :: Circuit -> VerilogSrc +generateAST c = VerilogSrc [Description $ genModuleDeclAST c] diff --git a/src/VeriFuzz/Circuit/CodeGen.hs b/src/VeriFuzz/Circuit/CodeGen.hs new file mode 100644 index 0000000..91da48c --- /dev/null +++ b/src/VeriFuzz/Circuit/CodeGen.hs @@ -0,0 +1,62 @@ +{-| +Module : VeriFuzz.Circuit.Random +Description : Code generation directly from DAG. +Copyright : (c) 2018-2019, Yann Herklotz Grave +License : BSD-3 +Maintainer : ymherklotz [at] gmail [dot] com +Stability : experimental +Portability : POSIX + +Define the code generation directly from the random DAG. +-} + +module VeriFuzz.Circuit.CodeGen + ( generate + ) +where + +import Data.Foldable (fold) +import Data.Graph.Inductive (Graph, LNode, Node, labNodes, pre) +import Data.Maybe (fromMaybe) +import Data.Text (Text) +import qualified Data.Text as T +import VeriFuzz.Circuit +import VeriFuzz.Internal.Gen +import VeriFuzz.Internal.Shared + +toOperator :: Gate -> Text +toOperator And = " & " +toOperator Or = " | " +toOperator Xor = " ^ " + +statList :: Gate -> [Node] -> Maybe Text +statList g n = toStr <$> safe tail n where toStr = fold . fmap ((<> toOperator g) . fromNode) + +lastEl :: [Node] -> Maybe Text +lastEl n = fromNode <$> safe head n + +toStmnt :: (Graph gr) => gr Gate e -> LNode Gate -> Text +toStmnt graph (n, g) = + fromMaybe T.empty + $ Just " assign " + <> Just (fromNode n) + <> Just " = " + <> statList g nodeL + <> lastEl nodeL + <> Just ";\n" + where nodeL = pre graph n + +generate :: (Graph gr) => gr Gate e -> Text +generate graph = + "module generated_module(\n" + <> fold (imap " input wire " ",\n" inp) + <> T.intercalate ",\n" (imap " output wire " "" out) + <> ");\n" + <> fold (toStmnt graph <$> labNodes graph) + <> "endmodule\n\nmodule main;\n initial\n begin\n " + <> "$display(\"Hello, world\");\n $finish;\n " + <> "end\nendmodule" + where + inp = inputs graph + out = outputs graph + imap b e = fmap ((\s -> b <> s <> e) . fromNode) diff --git a/src/VeriFuzz/Circuit/Random.hs b/src/VeriFuzz/Circuit/Random.hs new file mode 100644 index 0000000..7989b49 --- /dev/null +++ b/src/VeriFuzz/Circuit/Random.hs @@ -0,0 +1,54 @@ +{-| +Module : VeriFuzz.Circuit.Random +Description : Random generation for DAG +Copyright : (c) 2018-2019, Yann Herklotz Grave +License : BSD-3 +Maintainer : ymherklotz [at] gmail [dot] com +Stability : experimental +Portability : POSIX + +Define the random generation for the directed acyclic graph. +-} + +module VeriFuzz.Circuit.Random where + +import Data.Graph.Inductive (Context, LEdge) +import qualified Data.Graph.Inductive as G +import Data.Graph.Inductive.PatriciaTree (Gr) +import Data.List (nub) +import Test.QuickCheck (Arbitrary, Gen) +import qualified Test.QuickCheck as QC + +dupFolder :: (Eq a, Eq b) => Context a b -> [Context a b] -> [Context a b] +dupFolder cont ns = unique cont : ns + where unique (a, b, c, d) = (nub a, b, c, nub d) + +-- | Remove duplicates. +rDups :: (Eq a, Eq b) => Gr a b -> Gr a b +rDups g = G.buildGr $ G.ufold dupFolder [] g + +-- | 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) +arbitraryEdge n = do + x <- with $ \a -> a < n && a > 0 && a /= n - 1 + y <- with $ \a -> x < a && a < n && a > 0 + z <- QC.arbitrary + return (x, y, z) + where + with = QC.suchThat $ QC.resize n QC.arbitrary + +-- | Gen instance for a random acyclic DAG. +randomDAG :: (Arbitrary l, Arbitrary e, Eq l, Eq e) => Gen (Gr l e) -- ^ The generated graph. It uses Arbitrary to + -- generate random instances of each node +randomDAG = do + list <- QC.infiniteListOf QC.arbitrary + l <- QC.infiniteListOf aE + QC.sized (\n -> return . G.mkGraph (nodes list n) $ take (10 * n) l) + where + nodes l n = zip [0 .. n] $ take n l + aE = QC.sized arbitraryEdge + +-- | 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 diff --git a/src/VeriFuzz/Circuit/RandomAlt.hs b/src/VeriFuzz/Circuit/RandomAlt.hs new file mode 100644 index 0000000..93a50e9 --- /dev/null +++ b/src/VeriFuzz/Circuit/RandomAlt.hs @@ -0,0 +1,25 @@ +{-|p +Module : VeriFuzz.Circuit.RandomAlt +Description : RandomAlt generation for DAG +Copyright : (c) 2018-2019, Yann Herklotz Grave +License : BSD-3 +Maintainer : ymherklotz [at] gmail [dot] com +Stability : experimental +Portability : POSIX + +Define the random generation for the directed acyclic graph. +-} + +module VeriFuzz.Circuit.RandomAlt where + +import qualified Data.Graph.Inductive.Arbitrary as G +import Data.Graph.Inductive.PatriciaTree (Gr) +import Test.QuickCheck (Arbitrary, Gen) +import qualified Test.QuickCheck as QC + +randomDAG :: (Arbitrary l, Arbitrary e) => Gen (Gr l e) +randomDAG = G.looplessGraph <$> QC.arbitrary + +-- | Generate a random acyclic DAG with an IO instance. +genRandomDAG :: (Arbitrary l, Arbitrary e) => IO (Gr l e) +genRandomDAG = QC.generate randomDAG 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/Graph/ASTGen.hs b/src/VeriFuzz/Graph/ASTGen.hs deleted file mode 100644 index 745d849..0000000 --- a/src/VeriFuzz/Graph/ASTGen.hs +++ /dev/null @@ -1,82 +0,0 @@ -{-| -Module : VeriFuzz.Graph.ASTGen -Description : Generates the AST from the graph directly. -Copyright : (c) 2018-2019, Yann Herklotz Grave -License : BSD-3 -Maintainer : ymherklotz [at] gmail [dot] com -Stability : experimental -Portability : POSIX - -Generates the AST from the graph directly. --} - -module VeriFuzz.Graph.ASTGen where - -import Control.Lens ((^..)) -import Data.Foldable (fold) -import Data.Graph.Inductive (LNode, Node) -import qualified Data.Graph.Inductive as G -import Data.Maybe (catMaybes) -import VeriFuzz.Circuit -import VeriFuzz.Internal.Gen -import VeriFuzz.Verilog.AST -import VeriFuzz.Verilog.Helpers - --- | Converts a 'CNode' to an 'Identifier'. -frNode :: Node -> Identifier -frNode = Identifier . fromNode - --- | Converts a 'Gate' to a 'BinaryOperator', which should be a bijective --- mapping. -fromGate :: Gate -> BinaryOperator -fromGate And = BinAnd -fromGate Or = BinOr -fromGate Xor = BinXor - -inputsC :: Circuit -> [Node] -inputsC c = inputs (getCircuit c) - -outputsC :: Circuit -> [Node] -outputsC c = outputs (getCircuit c) - -genPortsAST :: (Circuit -> [Node]) -> Circuit -> [Port] -genPortsAST f c = port . frNode <$> f c where port = Port Wire 4 - --- | Generates the nested expression AST, so that it can then generate the --- assignment expressions. -genAssignExpr :: Gate -> [Node] -> Maybe Expr -genAssignExpr _ [] = Nothing -genAssignExpr _ [n ] = Just . Id $ frNode n -genAssignExpr g (n : ns) = BinOp wire op <$> genAssignExpr g ns - where - wire = Id $ frNode n - op = fromGate g - --- | Generate the continuous assignment AST for a particular node. If it does --- not have any nodes that link to it then return 'Nothing', as that means that --- the assignment will just be empty. -genContAssignAST :: Circuit -> LNode Gate -> Maybe ModItem -genContAssignAST c (n, g) = ModCA . ContAssign name <$> genAssignExpr g nodes - where - gr = getCircuit c - nodes = G.pre gr n - name = frNode n - -genAssignAST :: Circuit -> [ModItem] -genAssignAST c = catMaybes $ genContAssignAST c <$> nodes - where - gr = getCircuit c - nodes = G.labNodes gr - -genModuleDeclAST :: Circuit -> ModDecl -genModuleDeclAST c = ModDecl i output ports items - where - i = Identifier "gen_module" - ports = genPortsAST inputsC c - output = [Port Wire 90 "y"] - a = genAssignAST c - items = a ++ [ModCA . ContAssign "y" . fold $ Id <$> assigns] - assigns = a ^.. traverse . _ModCA . contAssignNetLVal - -generateAST :: Circuit -> VerilogSrc -generateAST c = VerilogSrc [Description $ genModuleDeclAST c] diff --git a/src/VeriFuzz/Graph/CodeGen.hs b/src/VeriFuzz/Graph/CodeGen.hs deleted file mode 100644 index 20c354a..0000000 --- a/src/VeriFuzz/Graph/CodeGen.hs +++ /dev/null @@ -1,62 +0,0 @@ -{-| -Module : VeriFuzz.Graph.Random -Description : Code generation directly from DAG. -Copyright : (c) 2018-2019, Yann Herklotz Grave -License : BSD-3 -Maintainer : ymherklotz [at] gmail [dot] com -Stability : experimental -Portability : POSIX - -Define the code generation directly from the random DAG. --} - -module VeriFuzz.Graph.CodeGen - ( generate - ) -where - -import Data.Foldable (fold) -import Data.Graph.Inductive (Graph, LNode, Node, labNodes, pre) -import Data.Maybe (fromMaybe) -import Data.Text (Text) -import qualified Data.Text as T -import VeriFuzz.Circuit -import VeriFuzz.Internal.Gen -import VeriFuzz.Internal.Shared - -toOperator :: Gate -> Text -toOperator And = " & " -toOperator Or = " | " -toOperator Xor = " ^ " - -statList :: Gate -> [Node] -> Maybe Text -statList g n = toStr <$> safe tail n where toStr = fold . fmap ((<> toOperator g) . fromNode) - -lastEl :: [Node] -> Maybe Text -lastEl n = fromNode <$> safe head n - -toStmnt :: (Graph gr) => gr Gate e -> LNode Gate -> Text -toStmnt graph (n, g) = - fromMaybe T.empty - $ Just " assign " - <> Just (fromNode n) - <> Just " = " - <> statList g nodeL - <> lastEl nodeL - <> Just ";\n" - where nodeL = pre graph n - -generate :: (Graph gr) => gr Gate e -> Text -generate graph = - "module generated_module(\n" - <> fold (imap " input wire " ",\n" inp) - <> T.intercalate ",\n" (imap " output wire " "" out) - <> ");\n" - <> fold (toStmnt graph <$> labNodes graph) - <> "endmodule\n\nmodule main;\n initial\n begin\n " - <> "$display(\"Hello, world\");\n $finish;\n " - <> "end\nendmodule" - where - inp = inputs graph - out = outputs graph - imap b e = fmap ((\s -> b <> s <> e) . fromNode) diff --git a/src/VeriFuzz/Graph/Random.hs b/src/VeriFuzz/Graph/Random.hs deleted file mode 100644 index f5a8d6f..0000000 --- a/src/VeriFuzz/Graph/Random.hs +++ /dev/null @@ -1,54 +0,0 @@ -{-| -Module : VeriFuzz.Graph.Random -Description : Random generation for DAG -Copyright : (c) 2018-2019, Yann Herklotz Grave -License : BSD-3 -Maintainer : ymherklotz [at] gmail [dot] com -Stability : experimental -Portability : POSIX - -Define the random generation for the directed acyclic graph. --} - -module VeriFuzz.Graph.Random where - -import Data.Graph.Inductive (Context, LEdge) -import qualified Data.Graph.Inductive as G -import Data.Graph.Inductive.PatriciaTree (Gr) -import Data.List (nub) -import Test.QuickCheck (Arbitrary, Gen) -import qualified Test.QuickCheck as QC - -dupFolder :: (Eq a, Eq b) => Context a b -> [Context a b] -> [Context a b] -dupFolder cont ns = unique cont : ns - where unique (a, b, c, d) = (nub a, b, c, nub d) - --- | Remove duplicates. -rDups :: (Eq a, Eq b) => Gr a b -> Gr a b -rDups g = G.buildGr $ G.ufold dupFolder [] g - --- | 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) -arbitraryEdge n = do - x <- with $ \a -> a < n && a > 0 && a /= n - 1 - y <- with $ \a -> x < a && a < n && a > 0 - z <- QC.arbitrary - return (x, y, z) - where - with = QC.suchThat $ QC.resize n QC.arbitrary - --- | Gen instance for a random acyclic DAG. -randomDAG :: (Arbitrary l, Arbitrary e, Eq l, Eq e) => Gen (Gr l e) -- ^ The generated graph. It uses Arbitrary to - -- generate random instances of each node -randomDAG = do - list <- QC.infiniteListOf QC.arbitrary - l <- QC.infiniteListOf aE - QC.sized (\n -> return . G.mkGraph (nodes list n) $ take (10 * n) l) - where - nodes l n = zip [0 .. n] $ take n l - aE = QC.sized arbitraryEdge - --- | 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 diff --git a/src/VeriFuzz/Graph/RandomAlt.hs b/src/VeriFuzz/Graph/RandomAlt.hs deleted file mode 100644 index e6d16bb..0000000 --- a/src/VeriFuzz/Graph/RandomAlt.hs +++ /dev/null @@ -1,25 +0,0 @@ -{-|p -Module : VeriFuzz.Graph.RandomAlt -Description : RandomAlt generation for DAG -Copyright : (c) 2018-2019, Yann Herklotz Grave -License : BSD-3 -Maintainer : ymherklotz [at] gmail [dot] com -Stability : experimental -Portability : POSIX - -Define the random generation for the directed acyclic graph. --} - -module VeriFuzz.Graph.RandomAlt where - -import qualified Data.Graph.Inductive.Arbitrary as G -import Data.Graph.Inductive.PatriciaTree (Gr) -import Test.QuickCheck (Arbitrary, Gen) -import qualified Test.QuickCheck as QC - -randomDAG :: (Arbitrary l, Arbitrary e) => Gen (Gr l e) -randomDAG = G.looplessGraph <$> QC.arbitrary - --- | Generate a random acyclic DAG with an IO instance. -genRandomDAG :: (Arbitrary l, Arbitrary e) => IO (Gr l e) -genRandomDAG = QC.generate randomDAG diff --git a/src/VeriFuzz/Internal.hs b/src/VeriFuzz/Internal.hs new file mode 100644 index 0000000..1adbc84 --- /dev/null +++ b/src/VeriFuzz/Internal.hs @@ -0,0 +1,18 @@ +{-| +Module : VeriFuzz.Internal +Description : Shared high level code used in the other modules internally. +Copyright : (c) 2018-2019, Yann Herklotz Grave +License : BSD-3 +Maintainer : ymherklotz [at] gmail [dot] com +Stability : experimental +Portability : POSIX + +Shared high level code used in the other modules internally. +-} + +module VeriFuzz.Internal where + +-- | Converts unsafe list functions in the Prelude to a safe version. +safe :: ([a] -> b) -> [a] -> Maybe b +safe _ [] = Nothing +safe f l = Just $ f l diff --git a/src/VeriFuzz/Internal/Circuit.hs b/src/VeriFuzz/Internal/Circuit.hs new file mode 100644 index 0000000..0634f01 --- /dev/null +++ b/src/VeriFuzz/Internal/Circuit.hs @@ -0,0 +1,32 @@ +{-| +Module : VeriFuzz.Internal.Circuit +Description : Internal helpers for generation. +Copyright : (c) 2018-2019, Yann Herklotz Grave +License : BSD-3 +Maintainer : ymherklotz [at] gmail [dot] com +Stability : experimental +Portability : POSIX + +Internal helpers for generation. +-} + +module VeriFuzz.Internal.Circuit where + +import Data.Graph.Inductive (Graph, Node) +import qualified Data.Graph.Inductive as G +import qualified Data.Text as T + +fromNode :: Int -> T.Text +fromNode node = T.pack $ "w" <> show node + +filterGr :: (Graph gr) => gr n e -> (Node -> Bool) -> [Node] +filterGr graph f = filter f $ G.nodes graph + +only :: (Graph gr) => gr n e -> (gr n e -> Node -> Int) -> (gr n e -> Node -> Int) -> Node -> Bool +only graph fun1 fun2 n = fun1 graph n == 0 && fun2 graph n /= 0 + +inputs :: (Graph gr) => gr n e -> [Node] +inputs graph = filterGr graph $ only graph G.indeg G.outdeg + +outputs :: (Graph gr) => gr n e -> [Node] +outputs graph = filterGr graph $ only graph G.outdeg G.indeg diff --git a/src/VeriFuzz/Internal/Gen.hs b/src/VeriFuzz/Internal/Gen.hs deleted file mode 100644 index d2e4e3c..0000000 --- a/src/VeriFuzz/Internal/Gen.hs +++ /dev/null @@ -1,32 +0,0 @@ -{-| -Module : VeriFuzz.Internal.Gen -Description : Internal helpers for generation. -Copyright : (c) 2018-2019, Yann Herklotz Grave -License : BSD-3 -Maintainer : ymherklotz [at] gmail [dot] com -Stability : experimental -Portability : POSIX - -Internal helpers for generation. --} - -module VeriFuzz.Internal.Gen where - -import Data.Graph.Inductive (Graph, Node) -import qualified Data.Graph.Inductive as G -import qualified Data.Text as T - -fromNode :: Int -> T.Text -fromNode node = T.pack $ "w" <> show node - -filterGr :: (Graph gr) => gr n e -> (Node -> Bool) -> [Node] -filterGr graph f = filter f $ G.nodes graph - -only :: (Graph gr) => gr n e -> (gr n e -> Node -> Int) -> (gr n e -> Node -> Int) -> Node -> Bool -only graph fun1 fun2 n = fun1 graph n == 0 && fun2 graph n /= 0 - -inputs :: (Graph gr) => gr n e -> [Node] -inputs graph = filterGr graph $ only graph G.indeg G.outdeg - -outputs :: (Graph gr) => gr n e -> [Node] -outputs graph = filterGr graph $ only graph G.outdeg G.indeg diff --git a/src/VeriFuzz/Internal/Shared.hs b/src/VeriFuzz/Internal/Shared.hs deleted file mode 100644 index c7d2760..0000000 --- a/src/VeriFuzz/Internal/Shared.hs +++ /dev/null @@ -1,18 +0,0 @@ -{-| -Module : VeriFuzz.Internal.Shared -Description : Shared high level code used in the other modules internally. -Copyright : (c) 2018-2019, Yann Herklotz Grave -License : BSD-3 -Maintainer : ymherklotz [at] gmail [dot] com -Stability : experimental -Portability : POSIX - -Shared high level code used in the other modules internally. --} - -module VeriFuzz.Internal.Shared where - --- | Converts unsafe list functions in the Prelude to a safe version. -safe :: ([a] -> b) -> [a] -> Maybe b -safe _ [] = Nothing -safe f l = Just $ f l diff --git a/src/VeriFuzz/Internal/Simulator.hs b/src/VeriFuzz/Internal/Simulator.hs new file mode 100644 index 0000000..4f8fd5a --- /dev/null +++ b/src/VeriFuzz/Internal/Simulator.hs @@ -0,0 +1,90 @@ +{-| +Module : VeriFuzz.Internal.Simulator +Description : Template file for different configuration files +Copyright : (c) 2019, Yann Herklotz Grave +License : GPL-3 +Maintainer : ymherklotz [at] gmail [dot] com +Stability : experimental +Portability : POSIX + +Template file for different configuration files. +-} + +{-# LANGUAGE QuasiQuotes #-} + +module VeriFuzz.Internal.Simulator where + +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 + +-- brittany-disable-next-binding +yosysSatConfig :: (Simulator a, Simulator b) => a -> Maybe b -> ModDecl -> Text +yosysSatConfig sim1 sim2 m = [st|read_verilog syn_#{toText sim1}.v +rename #{mi} #{mi}_1 +read_verilog syn_#{idSim2}.v +rename #{mi} #{mi}_2 +read_verilog top.v +proc; opt_clean +flatten #{mi} +! touch test.#{toText sim1}.#{idSim2}.input_ok +sat -timeout 20 -show-all -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 #{mi} +|] + where + idSim2 = maybe "rtl" toText sim2 + mi = modName m + +-- brittany-disable-next-binding +yosysSimConfig :: Text +yosysSimConfig = [st|read_verilog rtl.v; proc;; +rename mod mod_rtl +|] + +-- brittany-disable-next-binding +xstSynthConfig :: ModDecl -> Text +xstSynthConfig m = [st|run +-ifn #{mi}.prj -ofn #{mi} -p artix7 -top #{mi} +-iobuf NO -ram_extract NO -rom_extract NO -use_dsp48 NO +-fsm_extract YES -fsm_encoding Auto +-change_error_to_warning "HDLCompiler:226 HDLCompiler:1832" +|] + where + mi = modName m + +-- brittany-disable-next-binding +sbyConfig :: (Simulator a, Simulator b) => FilePath -> a -> Maybe b -> ModDecl -> Text +sbyConfig bd sim1 sim2 m = [st|[options] +mode prove + +[engines] +smtbmc + +[script] +#{readL} +read -formal syn_#{toText sim1}.v +rename #{mi} #{mi}_1 +read -formal syn_#{maybe "rtl" toText sim2}.v +rename #{mi} #{mi}_2 +read -formal top.v +prep -top #{mi} + +[files] +#{depList} +syn_#{maybe "rtl" toText sim2}.v +syn_#{toText sim1}.v +top.v +|] + where + mi = modName m + deps = ["cells_cmos.v", "cells_cyclone_v.v", "cells_verific.v", "cells_xilinx_7.v"] + depList = + T.intercalate "\n" + $ toTextIgnore + . ((bd fromText "data") ) + . fromText + <$> deps + readL = T.intercalate "\n" $ mappend "read -formal " <$> deps diff --git a/src/VeriFuzz/Simulator/Internal/Template.hs b/src/VeriFuzz/Simulator/Internal/Template.hs deleted file mode 100644 index 109c679..0000000 --- a/src/VeriFuzz/Simulator/Internal/Template.hs +++ /dev/null @@ -1,90 +0,0 @@ -{-| -Module : VeriFuzz.Simulator.Internal.Template -Description : Template file for different configuration files -Copyright : (c) 2019, Yann Herklotz Grave -License : GPL-3 -Maintainer : ymherklotz [at] gmail [dot] com -Stability : experimental -Portability : POSIX - -Template file for different configuration files. --} - -{-# LANGUAGE QuasiQuotes #-} - -module VeriFuzz.Simulator.Internal.Template where - -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 - --- brittany-disable-next-binding -yosysSatConfig :: (Simulator a, Simulator b) => a -> Maybe b -> ModDecl -> Text -yosysSatConfig sim1 sim2 m = [st|read_verilog syn_#{toText sim1}.v -rename #{mi} #{mi}_1 -read_verilog syn_#{idSim2}.v -rename #{mi} #{mi}_2 -read_verilog top.v -proc; opt_clean -flatten #{mi} -! touch test.#{toText sim1}.#{idSim2}.input_ok -sat -timeout 20 -show-all -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 #{mi} -|] - where - idSim2 = maybe "rtl" toText sim2 - mi = modName m - --- brittany-disable-next-binding -yosysSimConfig :: Text -yosysSimConfig = [st|read_verilog rtl.v; proc;; -rename mod mod_rtl -|] - --- brittany-disable-next-binding -xstSynthConfig :: ModDecl -> Text -xstSynthConfig m = [st|run --ifn #{mi}.prj -ofn #{mi} -p artix7 -top #{mi} --iobuf NO -ram_extract NO -rom_extract NO -use_dsp48 NO --fsm_extract YES -fsm_encoding Auto --change_error_to_warning "HDLCompiler:226 HDLCompiler:1832" -|] - where - mi = modName m - --- brittany-disable-next-binding -sbyConfig :: (Simulator a, Simulator b) => FilePath -> a -> Maybe b -> ModDecl -> Text -sbyConfig bd sim1 sim2 m = [st|[options] -mode prove - -[engines] -smtbmc - -[script] -#{readL} -read -formal syn_#{toText sim1}.v -rename #{mi} #{mi}_1 -read -formal syn_#{maybe "rtl" toText sim2}.v -rename #{mi} #{mi}_2 -read -formal top.v -prep -top #{mi} - -[files] -#{depList} -syn_#{maybe "rtl" toText sim2}.v -syn_#{toText sim1}.v -top.v -|] - where - mi = modName m - deps = ["cells_cmos.v", "cells_cyclone_v.v", "cells_verific.v", "cells_xilinx_7.v"] - depList = - T.intercalate "\n" - $ toTextIgnore - . ((bd fromText "data") ) - . fromText - <$> deps - readL = T.intercalate "\n" $ mappend "read -formal " <$> deps -- cgit