aboutsummaryrefslogtreecommitdiffstats
path: root/src/VeriFuzz/Circuit
diff options
context:
space:
mode:
authorYann Herklotz <git@ymhg.org>2019-04-02 19:47:32 +0100
committerYann Herklotz <git@ymhg.org>2019-04-02 19:47:32 +0100
commitfd4b0b5152f94cd406f2e5de86ce7ed0a4d2cbd0 (patch)
tree673439d49fa095bf3ae9b7bbbca5f30d7ff20838 /src/VeriFuzz/Circuit
parentc0c799ab3f79c370e4c33b8f824489ce8b1c96ec (diff)
downloadverismith-fd4b0b5152f94cd406f2e5de86ce7ed0a4d2cbd0.tar.gz
verismith-fd4b0b5152f94cd406f2e5de86ce7ed0a4d2cbd0.zip
Large refactor with passing tests
Diffstat (limited to 'src/VeriFuzz/Circuit')
-rw-r--r--src/VeriFuzz/Circuit/Base.hs42
-rw-r--r--src/VeriFuzz/Circuit/Gen.hs79
-rw-r--r--src/VeriFuzz/Circuit/Internal.hs45
-rw-r--r--src/VeriFuzz/Circuit/Random.hs67
4 files changed, 233 insertions, 0 deletions
diff --git a/src/VeriFuzz/Circuit/Base.hs b/src/VeriFuzz/Circuit/Base.hs
new file mode 100644
index 0000000..6b9f725
--- /dev/null
+++ b/src/VeriFuzz/Circuit/Base.hs
@@ -0,0 +1,42 @@
+{-|
+Module : VeriFuzz.Circuit.Base
+Description : Base types for the circuit module.
+Copyright : (c) 2019, Yann Herklotz Grave
+License : GPL-3
+Maintainer : ymherklotz [at] gmail [dot] com
+Stability : experimental
+Portability : POSIX
+
+Base types for the circuit module.
+-}
+
+module VeriFuzz.Circuit.Base
+ ( Gate(..)
+ , Circuit(..)
+ , CNode(..)
+ , CEdge(..)
+ )
+where
+
+import Data.Graph.Inductive (Gr, LEdge, LNode)
+import System.Random
+
+-- | The types for all the gates.
+data Gate = And
+ | Or
+ | Xor
+ deriving (Show, Eq, Enum, Bounded, Ord)
+
+-- | Newtype for the Circuit which implements a Graph from fgl.
+newtype Circuit = Circuit { getCircuit :: Gr Gate () }
+
+newtype CNode = CNode { getCNode :: LNode Gate }
+
+newtype CEdge = CEdge { getCEdge :: LEdge () }
+
+instance Random Gate where
+ randomR (a, b) g =
+ case randomR (fromEnum a, fromEnum b) g of
+ (x, g') -> (toEnum x, g')
+
+ random = randomR (minBound, maxBound)
diff --git a/src/VeriFuzz/Circuit/Gen.hs b/src/VeriFuzz/Circuit/Gen.hs
new file mode 100644
index 0000000..817d2f8
--- /dev/null
+++ b/src/VeriFuzz/Circuit/Gen.hs
@@ -0,0 +1,79 @@
+{-|
+Module : Verilog.Circuit.Gen
+Description : Generate verilog from circuit.
+Copyright : (c) 2019, Yann Herklotz Grave
+License : GPL-3
+Maintainer : ymherklotz [at] gmail [dot] com
+Stability : experimental
+Portability : POSIX
+
+Generate verilog from circuit.
+-}
+
+module VeriFuzz.Circuit.Gen
+ ( generateAST
+ )
+where
+
+import Data.Graph.Inductive (LNode, Node)
+import qualified Data.Graph.Inductive as G
+import Data.Maybe (catMaybes)
+import VeriFuzz.Circuit.Base
+import VeriFuzz.Circuit.Internal
+import VeriFuzz.Verilog.AST
+import VeriFuzz.Verilog.Mutate
+
+-- | 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)
+
+genPortsAST :: (Circuit -> [Node]) -> Circuit -> [Port]
+genPortsAST f c = port . frNode <$> f c where port = Port Wire False 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 oper <$> genAssignExpr g ns
+ where
+ wire = Id $ frNode n
+ oper = 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 $ combineAssigns yPort a
+ where
+ i = Identifier "gen_module"
+ ports = genPortsAST inputsC c
+ output = []
+ a = genAssignAST c
+ yPort = Port Wire False 90 "y"
+
+generateAST :: Circuit -> Verilog
+generateAST c = Verilog [Description $ genModuleDeclAST c]
diff --git a/src/VeriFuzz/Circuit/Internal.hs b/src/VeriFuzz/Circuit/Internal.hs
new file mode 100644
index 0000000..8a4cf4a
--- /dev/null
+++ b/src/VeriFuzz/Circuit/Internal.hs
@@ -0,0 +1,45 @@
+{-|
+Module : VeriFuzz.Circuit.Internal
+Description : Internal helpers for generation.
+Copyright : (c) 2018-2019, Yann Herklotz
+License : BSD-3
+Maintainer : ymherklotz [at] gmail [dot] com
+Stability : experimental
+Portability : POSIX
+
+Internal helpers for generation.
+-}
+
+module VeriFuzz.Circuit.Internal
+ ( fromNode
+ , filterGr
+ , only
+ , inputs
+ , outputs
+ )
+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/Circuit/Random.hs b/src/VeriFuzz/Circuit/Random.hs
new file mode 100644
index 0000000..58e855c
--- /dev/null
+++ b/src/VeriFuzz/Circuit/Random.hs
@@ -0,0 +1,67 @@
+{-|
+Module : VeriFuzz.Circuit.Random
+Description : Random generation for DAG
+Copyright : (c) 2018-2019, Yann Herklotz
+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
+ ( rDups
+ , rDupsCirc
+ , randomDAG
+ , genRandomDAG
+ )
+where
+
+import Data.Graph.Inductive (Context)
+import qualified Data.Graph.Inductive as G
+import Data.Graph.Inductive.PatriciaTree (Gr)
+import Data.List (nub)
+import Hedgehog (Gen)
+import qualified Hedgehog.Gen as Hog
+import qualified Hedgehog.Range as Hog
+import VeriFuzz.Circuit.Base
+
+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
+
+-- | 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 :: Hog.Size -> Gen CEdge
+arbitraryEdge n = do
+ x <- with $ \a -> a < n && a > 0 && a /= n - 1
+ y <- with $ \a -> x < a && a < n && a > 0
+ return $ CEdge (fromIntegral x, fromIntegral y, ())
+ where
+ with = flip Hog.filter $ fromIntegral <$> Hog.resize
+ n
+ (Hog.int (Hog.linear 0 100))
+
+-- | Gen instance for a random acyclic DAG.
+randomDAG :: Gen Circuit -- ^ The generated graph. It uses Arbitrary to generate
+ -- random instances of each node
+randomDAG = do
+ list <- Hog.list (Hog.linear 1 100) $ Hog.enum minBound maxBound
+ l <- Hog.list (Hog.linear 10 1000) aE
+ return . Circuit $ G.mkGraph (nodes list) l
+ where
+ nodes l = zip [0 .. length l - 1] l
+ aE = getCEdge <$> Hog.sized arbitraryEdge
+
+-- | Generate a random acyclic DAG with an IO instance.
+genRandomDAG :: IO Circuit
+genRandomDAG = Hog.sample randomDAG