diff options
author | Yann Herklotz <ymherklotz@gmail.com> | 2019-02-01 19:34:44 +0000 |
---|---|---|
committer | Yann Herklotz <ymherklotz@gmail.com> | 2019-02-01 19:34:44 +0000 |
commit | a38289ca9d96e97bc4e65b67c50f5805d56a3d86 (patch) | |
tree | 8bd1793ab02c3efe5cf668c045c82d77d61d8510 /src/VeriFuzz/Circuit | |
parent | afc9287534bc04ae139fa1d16c80ac0fc55e8767 (diff) | |
download | verismith-a38289ca9d96e97bc4e65b67c50f5805d56a3d86.tar.gz verismith-a38289ca9d96e97bc4e65b67c50f5805d56a3d86.zip |
Structure changes
Diffstat (limited to 'src/VeriFuzz/Circuit')
-rw-r--r-- | src/VeriFuzz/Circuit/ASTGen.hs | 82 | ||||
-rw-r--r-- | src/VeriFuzz/Circuit/CodeGen.hs | 62 | ||||
-rw-r--r-- | src/VeriFuzz/Circuit/Random.hs | 54 | ||||
-rw-r--r-- | src/VeriFuzz/Circuit/RandomAlt.hs | 25 |
4 files changed, 223 insertions, 0 deletions
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 |