diff options
-rw-r--r-- | app/Main.hs | 41 | ||||
-rw-r--r-- | src/VeriFuzz/Circuit.hs | 4 | ||||
-rw-r--r-- | src/VeriFuzz/Graph/ASTGen.hs | 10 | ||||
-rw-r--r-- | src/VeriFuzz/Graph/CodeGen.hs | 15 | ||||
-rw-r--r-- | src/VeriFuzz/Graph/Random.hs | 17 | ||||
-rw-r--r-- | src/VeriFuzz/Graph/RandomAlt.hs | 12 | ||||
-rw-r--r-- | src/VeriFuzz/Internal/Gen.hs | 8 | ||||
-rw-r--r-- | src/VeriFuzz/Simulator.hs | 9 | ||||
-rw-r--r-- | src/VeriFuzz/Simulator/General.hs | 10 | ||||
-rw-r--r-- | src/VeriFuzz/Simulator/Icarus.hs | 10 | ||||
-rw-r--r-- | src/VeriFuzz/Simulator/Xst.hs | 6 | ||||
-rw-r--r-- | src/VeriFuzz/Simulator/Yosys.hs | 18 | ||||
-rw-r--r-- | src/VeriFuzz/Verilog/AST.hs | 18 | ||||
-rw-r--r-- | src/VeriFuzz/Verilog/CodeGen.hs | 14 | ||||
-rw-r--r-- | src/VeriFuzz/Verilog/Helpers.hs | 2 | ||||
-rw-r--r-- | src/VeriFuzz/Verilog/Mutate.hs | 4 | ||||
-rw-r--r-- | verifuzz.cabal | 1 |
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 |