aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--app/Main.hs41
-rw-r--r--src/VeriFuzz/Circuit.hs4
-rw-r--r--src/VeriFuzz/Graph/ASTGen.hs10
-rw-r--r--src/VeriFuzz/Graph/CodeGen.hs15
-rw-r--r--src/VeriFuzz/Graph/Random.hs17
-rw-r--r--src/VeriFuzz/Graph/RandomAlt.hs12
-rw-r--r--src/VeriFuzz/Internal/Gen.hs8
-rw-r--r--src/VeriFuzz/Simulator.hs9
-rw-r--r--src/VeriFuzz/Simulator/General.hs10
-rw-r--r--src/VeriFuzz/Simulator/Icarus.hs10
-rw-r--r--src/VeriFuzz/Simulator/Xst.hs6
-rw-r--r--src/VeriFuzz/Simulator/Yosys.hs18
-rw-r--r--src/VeriFuzz/Verilog/AST.hs18
-rw-r--r--src/VeriFuzz/Verilog/CodeGen.hs14
-rw-r--r--src/VeriFuzz/Verilog/Helpers.hs2
-rw-r--r--src/VeriFuzz/Verilog/Mutate.hs4
-rw-r--r--verifuzz.cabal1
17 files changed, 90 insertions, 109 deletions
diff --git a/app/Main.hs b/app/Main.hs
index efa61e6..632e0f1 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -1,28 +1,18 @@
module Main where
import Control.Lens
-import qualified Crypto.Random.DRBG as C
-import Data.ByteString (ByteString)
-import qualified Data.ByteString as B
-import qualified Data.Graph.Inductive as G
-import qualified Data.Graph.Inductive.Arbitrary as G
-import qualified Data.Graph.Inductive.Dot as G
-import qualified Data.Graph.Inductive.PatriciaTree as G
-import qualified Data.Text.IO as T
-import qualified Data.Text.Lazy as T
-import Numeric (showHex)
-import Numeric.Natural (Natural)
+import qualified Crypto.Random.DRBG as C
+import Data.ByteString (ByteString)
+import qualified Data.Graph.Inductive as G
+import Numeric (showHex)
import Shelly
-import qualified Test.QuickCheck as QC
+import qualified Test.QuickCheck as QC
import VeriFuzz
-import qualified VeriFuzz.Graph.RandomAlt as V
genRand :: C.CtrDRBG -> Int -> [ByteString] -> [ByteString]
-genRand gen n bytes
- | n == 0 = ranBytes : bytes
- | otherwise = genRand newGen (n-1) $ ranBytes : bytes
- where
- Right (ranBytes, newGen) = C.genBytes 32 gen
+genRand gen n bytes | n == 0 = ranBytes : bytes
+ | otherwise = genRand newGen (n - 1) $ ranBytes : bytes
+ where Right (ranBytes, newGen) = C.genBytes 32 gen
genRandom :: Int -> IO [ByteString]
genRandom n = do
@@ -35,15 +25,22 @@ runSimulation = do
-- let dot = G.showDot . G.fglToDotString $ G.nemap show (const "") gr
-- writeFile "file.dot" dot
-- shelly $ run_ "dot" ["-Tpng", "-o", "file.png", "file.dot"]
- let circ = head $ (nestUpTo 5 . generateAST $ Circuit gr) ^.. getVerilogSrc . traverse . getDescription
+ let circ =
+ head $ (nestUpTo 5 . generateAST $ Circuit gr) ^.. getVerilogSrc . traverse . getDescription
rand <- genRandom 20
- val <- shelly $ runSim defaultIcarus (initMod circ) rand
+ val <- shelly $ runSim defaultIcarus (initMod circ) rand
putStrLn $ showHex (abs val) ""
-runEquivalence:: IO ()
+runEquivalence :: IO ()
runEquivalence = do
gr <- QC.generate $ rDups <$> QC.resize 100 (randomDAG :: QC.Gen (G.Gr Gate ()))
- let circ = initMod . head $ (nestUpTo 5 . generateAST $ Circuit gr) ^.. getVerilogSrc . traverse . getDescription
+ let circ =
+ initMod
+ . head
+ $ (nestUpTo 5 . generateAST $ Circuit gr)
+ ^.. getVerilogSrc
+ . traverse
+ . getDescription
shelly . verbosely $ runEquiv defaultYosys defaultYosys (Just defaultXst) circ
main :: IO ()
diff --git a/src/VeriFuzz/Circuit.hs b/src/VeriFuzz/Circuit.hs
index 1891ff9..7958f6a 100644
--- a/src/VeriFuzz/Circuit.hs
+++ b/src/VeriFuzz/Circuit.hs
@@ -12,9 +12,7 @@ Definition of the circuit graph.
module VeriFuzz.Circuit where
-import Data.Graph.Inductive ( Gr
- , LNode
- )
+import Data.Graph.Inductive (Gr, LNode)
import System.Random
import Test.QuickCheck
diff --git a/src/VeriFuzz/Graph/ASTGen.hs b/src/VeriFuzz/Graph/ASTGen.hs
index ad7dd50..30dee04 100644
--- a/src/VeriFuzz/Graph/ASTGen.hs
+++ b/src/VeriFuzz/Graph/ASTGen.hs
@@ -12,12 +12,10 @@ Generates the AST from the graph directly.
module VeriFuzz.Graph.ASTGen where
-import Data.Foldable ( fold )
-import Data.Graph.Inductive ( LNode
- , Node
- )
-import qualified Data.Graph.Inductive as G
-import Data.Maybe ( catMaybes )
+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
diff --git a/src/VeriFuzz/Graph/CodeGen.hs b/src/VeriFuzz/Graph/CodeGen.hs
index 56b28aa..20c354a 100644
--- a/src/VeriFuzz/Graph/CodeGen.hs
+++ b/src/VeriFuzz/Graph/CodeGen.hs
@@ -15,16 +15,11 @@ module VeriFuzz.Graph.CodeGen
)
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 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
diff --git a/src/VeriFuzz/Graph/Random.hs b/src/VeriFuzz/Graph/Random.hs
index 573c179..4b72b95 100644
--- a/src/VeriFuzz/Graph/Random.hs
+++ b/src/VeriFuzz/Graph/Random.hs
@@ -12,17 +12,12 @@ 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
+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)
diff --git a/src/VeriFuzz/Graph/RandomAlt.hs b/src/VeriFuzz/Graph/RandomAlt.hs
index c5fad9e..e6d16bb 100644
--- a/src/VeriFuzz/Graph/RandomAlt.hs
+++ b/src/VeriFuzz/Graph/RandomAlt.hs
@@ -12,14 +12,10 @@ 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
+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
diff --git a/src/VeriFuzz/Internal/Gen.hs b/src/VeriFuzz/Internal/Gen.hs
index d821cd7..d2e4e3c 100644
--- a/src/VeriFuzz/Internal/Gen.hs
+++ b/src/VeriFuzz/Internal/Gen.hs
@@ -12,11 +12,9 @@ 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
+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
diff --git a/src/VeriFuzz/Simulator.hs b/src/VeriFuzz/Simulator.hs
index 0692c31..24365fd 100644
--- a/src/VeriFuzz/Simulator.hs
+++ b/src/VeriFuzz/Simulator.hs
@@ -18,7 +18,16 @@ module VeriFuzz.Simulator
)
where
+import Control.Monad.Trans.Reader (ReaderT)
+import Shelly
import VeriFuzz.Simulator.General
import VeriFuzz.Simulator.Icarus
import VeriFuzz.Simulator.Xst
import VeriFuzz.Simulator.Yosys
+
+data SimMatrix = SimMatrix { yosys :: Yosys
+ , xst :: Maybe Xst
+ , icarus :: Maybe Icarus
+ }
+
+type SimEnv = ReaderT SimMatrix Sh
diff --git a/src/VeriFuzz/Simulator/General.hs b/src/VeriFuzz/Simulator/General.hs
index 9001bf9..3615d3a 100644
--- a/src/VeriFuzz/Simulator/General.hs
+++ b/src/VeriFuzz/Simulator/General.hs
@@ -12,11 +12,11 @@ Class of the simulator and the synthesize tool.
module VeriFuzz.Simulator.General where
-import Data.Bits ( shiftL )
-import Data.ByteString ( ByteString )
-import qualified Data.ByteString as B
-import Data.Text ( Text )
-import Prelude hiding ( FilePath )
+import Data.Bits (shiftL)
+import Data.ByteString (ByteString)
+import qualified Data.ByteString as B
+import Data.Text (Text)
+import Prelude hiding (FilePath)
import Shelly
import VeriFuzz.Verilog.AST
diff --git a/src/VeriFuzz/Simulator/Icarus.hs b/src/VeriFuzz/Simulator/Icarus.hs
index fdb1ad6..4782585 100644
--- a/src/VeriFuzz/Simulator/Icarus.hs
+++ b/src/VeriFuzz/Simulator/Icarus.hs
@@ -13,12 +13,12 @@ Icarus verilog module.
module VeriFuzz.Simulator.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.Simulator.General
import VeriFuzz.Verilog
diff --git a/src/VeriFuzz/Simulator/Xst.hs b/src/VeriFuzz/Simulator/Xst.hs
index 1a0763c..29d1e4a 100644
--- a/src/VeriFuzz/Simulator/Xst.hs
+++ b/src/VeriFuzz/Simulator/Xst.hs
@@ -14,10 +14,10 @@ Xst (ise) simulator implementation.
module VeriFuzz.Simulator.Xst where
-import Control.Lens hiding ( (<.>) )
-import Prelude hiding ( FilePath )
+import Control.Lens hiding ((<.>))
+import Prelude hiding (FilePath)
import Shelly
-import Text.Shakespeare.Text ( st )
+import Text.Shakespeare.Text (st)
import VeriFuzz.Simulator.General
import VeriFuzz.Verilog.AST
import VeriFuzz.Verilog.CodeGen
diff --git a/src/VeriFuzz/Simulator/Yosys.hs b/src/VeriFuzz/Simulator/Yosys.hs
index 028fbb2..8f40ea9 100644
--- a/src/VeriFuzz/Simulator/Yosys.hs
+++ b/src/VeriFuzz/Simulator/Yosys.hs
@@ -15,10 +15,10 @@ Yosys simulator implementation.
module VeriFuzz.Simulator.Yosys where
import Control.Lens
-import Data.Text ( Text )
-import Prelude hiding ( FilePath )
+import Data.Text (Text)
+import Prelude hiding (FilePath)
import Shelly
-import Text.Shakespeare.Text ( st )
+import Text.Shakespeare.Text (st)
import VeriFuzz.Simulator.General
import VeriFuzz.Verilog
@@ -71,12 +71,10 @@ sat -timeout 20 -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 #{modName}
modName = m ^. moduleId . getIdentifier
-- ids = T.intercalate "," $ allVars m ^.. traverse . getIdentifier
--- brittany-disable-next-binding
runOtherSynth :: (Synthesize a) => Maybe a -> ModDecl -> Sh ()
runOtherSynth (Just sim) m = runSynth sim m $ fromText [st|syn_#{toText sim}.v|]
-runOtherSynth Nothing m = writefile "syn_rtl.v" $ genSource m
+runOtherSynth Nothing m = writefile "syn_rtl.v" $ genSource m
--- brittany-disable-next-binding
runEquiv :: (Synthesize a, Synthesize b) => Yosys -> a -> Maybe b -> ModDecl -> Sh ()
runEquiv yosys sim1 sim2 m = do
writefile "top.v" . genSource . initMod $ makeTop 2 m
@@ -84,5 +82,9 @@ runEquiv yosys sim1 sim2 m = do
runSynth sim1 m $ fromText [st|syn_#{toText sim1}.v|]
runOtherSynth sim2 m
run_ (yosysPath yosys) [checkFile]
- where
- checkFile = [st|test.#{toText sim1}.#{maybe "rtl" toText sim2}.ys|]
+ where checkFile = [st|test.#{toText sim1}.#{maybe "rtl" toText sim2}.ys|]
+
+-- | Generate @.il@ files for Yosys equivalence checking using the SAT solver.
+genIl :: (Synthesize a) => Yosys -> a -> ModDecl -> Sh ()
+genIl yosys sim m = do
+ return
diff --git a/src/VeriFuzz/Verilog/AST.hs b/src/VeriFuzz/Verilog/AST.hs
index 9db4999..b3754ec 100644
--- a/src/VeriFuzz/Verilog/AST.hs
+++ b/src/VeriFuzz/Verilog/AST.hs
@@ -107,17 +107,13 @@ module VeriFuzz.Verilog.AST
)
where
-import Control.Lens ( makeLenses
- , makePrisms
- )
-import Control.Monad ( replicateM )
-import Data.String ( IsString
- , fromString
- )
-import Data.Text ( Text )
-import qualified Data.Text as T
-import Data.Traversable ( sequenceA )
-import qualified Test.QuickCheck as QC
+import Control.Lens (makeLenses, makePrisms)
+import Control.Monad (replicateM)
+import Data.String (IsString, fromString)
+import Data.Text (Text)
+import qualified Data.Text as T
+import Data.Traversable (sequenceA)
+import qualified Test.QuickCheck as QC
positiveArb :: (QC.Arbitrary a, Ord a, Num a) => QC.Gen a
positiveArb = QC.suchThat QC.arbitrary (> 0)
diff --git a/src/VeriFuzz/Verilog/CodeGen.hs b/src/VeriFuzz/Verilog/CodeGen.hs
index 1551c1d..956472f 100644
--- a/src/VeriFuzz/Verilog/CodeGen.hs
+++ b/src/VeriFuzz/Verilog/CodeGen.hs
@@ -15,14 +15,12 @@ This module generates the code from the Verilog AST defined in
module VeriFuzz.Verilog.CodeGen where
-import Control.Lens ( view
- , (^.)
- )
-import Data.Foldable ( fold )
-import Data.Text ( Text )
-import qualified Data.Text as T
-import qualified Data.Text.IO as T
-import Numeric ( showHex )
+import Control.Lens (view, (^.))
+import Data.Foldable (fold)
+import Data.Text (Text)
+import qualified Data.Text as T
+import qualified Data.Text.IO as T
+import Numeric (showHex)
import VeriFuzz.Verilog.AST
-- | 'Source' class which determines that source code is able to be generated
diff --git a/src/VeriFuzz/Verilog/Helpers.hs b/src/VeriFuzz/Verilog/Helpers.hs
index f910924..4771329 100644
--- a/src/VeriFuzz/Verilog/Helpers.hs
+++ b/src/VeriFuzz/Verilog/Helpers.hs
@@ -13,7 +13,7 @@ Defaults and common functions.
module VeriFuzz.Verilog.Helpers where
import Control.Lens
-import Data.Text ( Text )
+import Data.Text (Text)
import VeriFuzz.Verilog.AST
regDecl :: Identifier -> ModItem
diff --git a/src/VeriFuzz/Verilog/Mutate.hs b/src/VeriFuzz/Verilog/Mutate.hs
index 3052598..82d3db9 100644
--- a/src/VeriFuzz/Verilog/Mutate.hs
+++ b/src/VeriFuzz/Verilog/Mutate.hs
@@ -14,9 +14,7 @@ more random patterns, such as nesting wires instead of creating new ones.
module VeriFuzz.Verilog.Mutate where
import Control.Lens
-import Data.Maybe ( catMaybes
- , fromMaybe
- )
+import Data.Maybe (catMaybes, fromMaybe)
import VeriFuzz.Internal.Gen
import VeriFuzz.Internal.Shared
import VeriFuzz.Verilog.AST
diff --git a/verifuzz.cabal b/verifuzz.cabal
index 6d01049..7ea2d2c 100644
--- a/verifuzz.cabal
+++ b/verifuzz.cabal
@@ -49,6 +49,7 @@ library
, text
, bytestring
, hashable
+ , transformers
default-extensions: OverloadedStrings
executable verifuzz
generated by cgit (git 2.34.1) at 2024-06-28 21:49:56 +0000