Large refactor with passing tests

4 files changed, 0 insertions, 321 deletions

diff --git a/src/VeriFuzz/Internal/AST.hs b/src/VeriFuzz/Internal/AST.hs
deleted file mode 100644
index 49e1d30..0000000
--- a/src/VeriFuzz/Internal/AST.hs
+++ /dev/null
@@ -1,83 +0,0 @@
-{-|
-Module      : VeriFuzz.Internal.AST
-Description : Defaults and common functions.
-Copyright   : (c) 2018-2019, Yann Herklotz
-License     : BSD-3
-Maintainer  : ymherklotz [at] gmail [dot] com
-Stability   : experimental
-Portability : POSIX
-
-Defaults and common functions.
--}
-
-module VeriFuzz.Internal.AST where
-
-import           Control.Lens
-import           Data.Text    (Text)
-import           VeriFuzz.AST
-
-regDecl :: Identifier -> ModItem
-regDecl = Decl Nothing . Port Reg False 1
-
-wireDecl :: Identifier -> ModItem
-wireDecl = Decl Nothing . Port Wire False 1
-
--- | Create an empty module.
-emptyMod :: ModDecl
-emptyMod = ModDecl "" [] [] []
-
--- | Set a module name for a module declaration.
-setModName :: Text -> ModDecl -> ModDecl
-setModName str = modId .~ Identifier str
-
--- | Add a input port to the module declaration.
-addModPort :: Port -> ModDecl -> ModDecl
-addModPort port = modInPorts %~ (:) port
-
-addDescription :: Description -> Verilog -> Verilog
-addDescription desc = getVerilog %~ (:) desc
-
-testBench :: ModDecl
-testBench = ModDecl
-    "main"
-    []
-    []
-    [ regDecl "a"
-    , regDecl "b"
-    , wireDecl "c"
-    , ModInst "and"
-              "and_gate"
-              [ModConn $ Id "c", ModConn $ Id "a", ModConn $ Id "b"]
-    , Initial $ SeqBlock
-        [ BlockAssign . Assign (RegId "a") Nothing $ Number 1 1
-        , BlockAssign . Assign (RegId "b") Nothing $ Number 1 1
-    -- , TimeCtrl (Delay 1) . Just . SysTaskEnable $ Task "display"
-    --   [ Str "%d & %d = %d"
-    --   , PrimExpr $ PrimId "a"
-    --   , PrimExpr $ PrimId "b"
-    --   , PrimExpr $ PrimId "c"
-    --   ]
-    -- , SysTaskEnable $ Task "finish" []
-        ]
-    ]
-
-addTestBench :: Verilog -> Verilog
-addTestBench = addDescription $ Description testBench
-
-defaultPort :: Identifier -> Port
-defaultPort = Port Wire False 1
-
-portToExpr :: Port -> Expr
-portToExpr (Port _ _ _ i) = Id i
-
-modName :: ModDecl -> Text
-modName = view $ modId . getIdentifier
-
-yPort :: Identifier -> Port
-yPort = Port Wire False 90
-
-wire :: Int -> Identifier -> Port
-wire = Port Wire False
-
-reg :: Int -> Identifier -> Port
-reg = Port Reg False
diff --git a/src/VeriFuzz/Internal/Circuit.hs b/src/VeriFuzz/Internal/Circuit.hs
deleted file mode 100644
index 832d0a4..0000000
--- a/src/VeriFuzz/Internal/Circuit.hs
+++ /dev/null
@@ -1,38 +0,0 @@
-{-|
-Module      : VeriFuzz.Internal.Circuit
-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.Internal.Circuit 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/Internal/Simulator.hs b/src/VeriFuzz/Internal/Simulator.hs
deleted file mode 100644
index 4c21864..0000000
--- a/src/VeriFuzz/Internal/Simulator.hs
+++ /dev/null
@@ -1,98 +0,0 @@
-{-|
-Module      : VeriFuzz.Internal.Simulator
-Description : Class of the simulator.
-Copyright   : (c) 2018-2019, Yann Herklotz
-License     : BSD-3
-Maintainer  : ymherklotz [at] gmail [dot] com
-Stability   : experimental
-Portability : POSIX
-
-Class of the simulator and the synthesize tool.
--}
-
-module VeriFuzz.Internal.Simulator where
-
-import           Control.Lens
-import           Data.Bits             (shiftL)
-import           Data.ByteString       (ByteString)
-import qualified Data.ByteString       as B
-import           Data.Text             (Text)
-import qualified Data.Text             as T
-import           Prelude               hiding (FilePath)
-import           Shelly
-import           System.FilePath.Posix (takeBaseName)
-import           VeriFuzz.AST
-
--- | Tool class.
-class Tool a where
-  toText :: a -> Text
-
--- | Simulation type class.
-class (Tool a) => Simulator a where
-  runSim :: a             -- ^ Simulator instance
-         -> SourceInfo       -- ^ Run information
-         -> [ByteString]  -- ^ Inputs to simulate
-         -> Sh ByteString -- ^ Returns the value of the hash at the output of the testbench.
-  runSimWithFile :: a
-                 -> FilePath
-                 -> [ByteString]
-                 -> Sh ByteString
-
--- | Synthesisor type class.
-class (Tool a) => Synthesisor a where
-  runSynth :: a        -- ^ Synthesisor tool instance
-           -> SourceInfo  -- ^ Run information
-           -> FilePath -- ^ Output verilog file for the module
-           -> Sh ()    -- ^ does not return any values
-
-data SourceInfo = SourceInfo { runMainModule :: {-# UNPACK #-} !Text
-                             , runSource     :: !Verilog
-                             }
-                  deriving (Eq, Show)
-
--- | May need to change this to Traversal to be safe. For now it will fail when
--- the main has not been properly set with.
-mainModule :: Lens' SourceInfo ModDecl
-mainModule = lens get_ set_
-  where
-    set_ (SourceInfo top main) v =
-        SourceInfo top (main & getModule %~ update top v)
-    update top v m@(ModDecl (Identifier i) _ _ _) | i == top  = v
-                                                  | otherwise = m
-    get_ (SourceInfo top main) = head . filter (f top) $ main ^.. getModule
-    f top (ModDecl (Identifier i) _ _ _) = i == top
-
-rootPath :: Sh FilePath
-rootPath = do
-    current <- pwd
-    maybe current fromText <$> get_env "VERIFUZZ_ROOT"
-
-timeout :: FilePath -> [Text] -> Sh Text
-timeout = command1 "timeout" ["300"] . toTextIgnore
-{-# INLINE timeout #-}
-
-timeout_ :: FilePath -> [Text] -> Sh ()
-timeout_ = command1_ "timeout" ["300"] . toTextIgnore
-{-# INLINE timeout_ #-}
-
--- | Helper function to convert bytestrings to integers
-bsToI :: ByteString -> Integer
-bsToI = B.foldl' (\i b -> (i `shiftL` 8) + fromIntegral b) 0
-{-# INLINE bsToI #-}
-
-noPrint :: Sh a -> Sh a
-noPrint = print_stdout False . print_stderr False
-{-# INLINE noPrint #-}
-
-echoP :: Text -> Sh ()
-echoP t = do
-    fn <- pwd
-    echo $ bname fn <> " - " <> t
-    where bname = T.pack . takeBaseName . T.unpack . toTextIgnore
-
-logger :: FilePath -> Text -> Sh a -> Sh a
-logger fp name = log_stderr_with (l "_log.stderr.txt")
-    . log_stdout_with (l "_log.txt")
-  where
-    l s t = appendFile (file s) (T.unpack t) >> appendFile (file s) "\n"
-    file s = T.unpack (toTextIgnore $ fp </> fromText name) <> s
diff --git a/src/VeriFuzz/Internal/Template.hs b/src/VeriFuzz/Internal/Template.hs
deleted file mode 100644
index 1b0e241..0000000
--- a/src/VeriFuzz/Internal/Template.hs
+++ /dev/null
@@ -1,102 +0,0 @@
-{-|
-Module      : VeriFuzz.Internal.Template
-Description : Template file for different configuration files
-Copyright   : (c) 2019, Yann Herklotz
-License     : GPL-3
-Maintainer  : ymherklotz [at] gmail [dot] com
-Stability   : experimental
-Portability : POSIX
-
-Template file for different configuration files.
--}
-
-{-# LANGUAGE QuasiQuotes #-}
-
-module VeriFuzz.Internal.Template where
-
-import           Control.Lens                ((^..))
-import           Data.Text                   (Text)
-import qualified Data.Text                   as T
-import           Prelude                     hiding (FilePath)
-import           Shelly
-import           Text.Shakespeare.Text       (st)
-import           VeriFuzz.AST
-import           VeriFuzz.Internal.Simulator
-
-rename :: Text -> [Text] -> Text
-rename end entries =
-    T.intercalate "\n"
-        $   flip mappend end
-        .   mappend "rename "
-        .   doubleName
-        <$> entries
-{-# INLINE rename #-}
-
-doubleName :: Text -> Text
-doubleName n = n <> " " <> n
-{-# INLINE doubleName #-}
-
--- brittany-disable-next-binding
-yosysSatConfig :: (Tool a, Tool b) => a -> Maybe b -> SourceInfo -> Text
-yosysSatConfig sim1 sim2 (SourceInfo top src) = [st|read_verilog syn_#{toText sim1}.v
-#{rename "_1" mis}
-read_verilog syn_#{idSim2}.v
-#{rename "_2" mis}
-read_verilog #{top}.v
-proc; opt_clean
-flatten #{top}
-! touch test.#{toText sim1}.#{idSim2}.input_ok
-sat -timeout 20 -show-all -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 #{top}
-|]
-  where
-    idSim2 = maybe "rtl" toText sim2
-    mis = src ^.. getSourceId
-
--- brittany-disable-next-binding
-yosysSimConfig :: Text
-yosysSimConfig = [st|read_verilog rtl.v; proc;;
-rename mod mod_rtl
-|]
-
--- brittany-disable-next-binding
-xstSynthConfig :: Text -> Text
-xstSynthConfig top = [st|run
--ifn #{top}.prj -ofn #{top} -p artix7 -top #{top}
--iobuf NO -ram_extract NO -rom_extract NO -use_dsp48 NO
--fsm_extract YES -fsm_encoding Auto
--change_error_to_warning "HDLCompiler:226 HDLCompiler:1832"
-|]
-
--- brittany-disable-next-binding
-sbyConfig :: (Tool a, Tool b) => FilePath -> a -> Maybe b -> SourceInfo -> Text
-sbyConfig bd sim1 sim2 (SourceInfo top src) = [st|[options]
-mode prove
-
-[engines]
-smtbmc
-
-[script]
-#{readL}
-read -formal syn_#{toText sim1}.v
-#{rename "_1" mis}
-read -formal syn_#{maybe "rtl" toText sim2}.v
-#{rename "_2" mis}
-read -formal top.v
-prep -top #{top}
-
-[files]
-#{depList}
-syn_#{maybe "rtl" toText sim2}.v
-syn_#{toText sim1}.v
-top.v
-|]
-  where
-    mis = src ^.. getSourceId
-    deps = ["cells_cmos.v", "cells_cyclone_v.v", "cells_verific.v", "cells_xilinx_7.v"]
-    depList =
-      T.intercalate "\n"
-        $   toTextIgnore
-        .   ((bd </> fromText "data") </>)
-        .   fromText
-        <$> deps
-    readL = T.intercalate "\n" $ mappend "read -formal " <$> deps