aboutsummaryrefslogtreecommitdiffstats
path: root/src/VeriFuzz/Circuit
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2019-10-29 12:06:05 +0000
committerYann Herklotz <git@yannherklotz.com>2019-10-29 12:06:05 +0000
commit4ee6646b8a78d4c20fe0b89d95f23d382e1c47fc (patch)
tree9b02e1b92f8abf0baf3dc108ab7f4fb8f33e753a /src/VeriFuzz/Circuit
parent1aaff80235237507572e0fb4be86f34cb1829b68 (diff)
parent01c2ab3f6a58d416528efce3057e2cf2f1604489 (diff)
downloadverismith-feature/nondeterminism.tar.gz
verismith-feature/nondeterminism.zip
Merge branch 'master' into HEADfeature/nondeterminism
Diffstat (limited to 'src/VeriFuzz/Circuit')
-rw-r--r--src/VeriFuzz/Circuit/Base.hs44
-rw-r--r--src/VeriFuzz/Circuit/Gen.hs79
-rw-r--r--src/VeriFuzz/Circuit/Internal.hs55
-rw-r--r--src/VeriFuzz/Circuit/Random.hs67
4 files changed, 0 insertions, 245 deletions
diff --git a/src/VeriFuzz/Circuit/Base.hs b/src/VeriFuzz/Circuit/Base.hs
deleted file mode 100644
index 0bcdf39..0000000
--- a/src/VeriFuzz/Circuit/Base.hs
+++ /dev/null
@@ -1,44 +0,0 @@
-{-|
-Module : VeriFuzz.Circuit.Base
-Description : Base types for the circuit module.
-Copyright : (c) 2019, Yann Herklotz Grave
-License : GPL-3
-Maintainer : yann [at] yannherklotz [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 for a node in the circuit, which is an 'LNode Gate'.
-newtype CNode = CNode { getCNode :: LNode Gate }
-
--- | Newtype for a named edge which is empty, as it does not need a label.
-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
deleted file mode 100644
index eb7cb97..0000000
--- a/src/VeriFuzz/Circuit/Gen.hs
+++ /dev/null
@@ -1,79 +0,0 @@
-{-|
-Module : Verilog.Circuit.Gen
-Description : Generate verilog from circuit.
-Copyright : (c) 2019, Yann Herklotz Grave
-License : GPL-3
-Maintainer : yann [at] yannherklotz [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 [genModuleDeclAST c]
diff --git a/src/VeriFuzz/Circuit/Internal.hs b/src/VeriFuzz/Circuit/Internal.hs
deleted file mode 100644
index 17e1586..0000000
--- a/src/VeriFuzz/Circuit/Internal.hs
+++ /dev/null
@@ -1,55 +0,0 @@
-{-|
-Module : VeriFuzz.Circuit.Internal
-Description : Internal helpers for generation.
-Copyright : (c) 2018-2019, Yann Herklotz
-License : BSD-3
-Maintainer : yann [at] yannherklotz [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
-
--- | Convert an integer into a label.
---
--- >>> fromNode 5
--- "w5"
-fromNode :: Int -> T.Text
-fromNode node = T.pack $ "w" <> show node
-
--- | General function which runs 'filter' over a graph.
-filterGr :: (Graph gr) => gr n e -> (Node -> Bool) -> [Node]
-filterGr graph f = filter f $ G.nodes graph
-
--- | Takes two functions that return an 'Int', and compares there results to 0
--- and not 0 respectively. This result is returned.
-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
-
--- | Returns all the input nodes to a graph, which means nodes that do not have
--- an input themselves.
-inputs :: (Graph gr) => gr n e -> [Node]
-inputs graph = filterGr graph $ only graph G.indeg G.outdeg
-
--- | Returns all the output nodes to a graph, similar to the 'inputs' function.
-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
deleted file mode 100644
index fdb5253..0000000
--- a/src/VeriFuzz/Circuit/Random.hs
+++ /dev/null
@@ -1,67 +0,0 @@
-{-|
-Module : VeriFuzz.Circuit.Random
-Description : Random generation for DAG
-Copyright : (c) 2018-2019, Yann Herklotz
-License : BSD-3
-Maintainer : yann [at] yannherklotz [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