diff options
Diffstat (limited to 'src/VeriFuzz/Internal')
-rw-r--r-- | src/VeriFuzz/Internal/AST.hs | 83 | ||||
-rw-r--r-- | src/VeriFuzz/Internal/Circuit.hs | 38 | ||||
-rw-r--r-- | src/VeriFuzz/Internal/Simulator.hs | 98 | ||||
-rw-r--r-- | src/VeriFuzz/Internal/Template.hs | 102 |
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 |