From 64a0ae3600073f486462b1d056409954634b0084 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 19 Jan 2019 23:12:25 +0000 Subject: Reformat with stylish-haskell --- src/VeriFuzz/Circuit.hs | 4 +--- src/VeriFuzz/Graph/ASTGen.hs | 10 ++++------ src/VeriFuzz/Graph/CodeGen.hs | 15 +++++---------- src/VeriFuzz/Graph/Random.hs | 17 ++++++----------- src/VeriFuzz/Graph/RandomAlt.hs | 12 ++++-------- src/VeriFuzz/Internal/Gen.hs | 8 +++----- src/VeriFuzz/Simulator.hs | 9 +++++++++ src/VeriFuzz/Simulator/General.hs | 10 +++++----- src/VeriFuzz/Simulator/Icarus.hs | 10 +++++----- src/VeriFuzz/Simulator/Xst.hs | 6 +++--- src/VeriFuzz/Simulator/Yosys.hs | 18 ++++++++++-------- src/VeriFuzz/Verilog/AST.hs | 18 +++++++----------- src/VeriFuzz/Verilog/CodeGen.hs | 14 ++++++-------- src/VeriFuzz/Verilog/Helpers.hs | 2 +- src/VeriFuzz/Verilog/Mutate.hs | 4 +--- 15 files changed, 70 insertions(+), 87 deletions(-) (limited to 'src/VeriFuzz') 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 -- cgit