aboutsummaryrefslogtreecommitdiffstats
path: root/src/VeriFuzz/Simulator
diff options
context:
space:
mode:
Diffstat (limited to 'src/VeriFuzz/Simulator')
-rw-r--r--src/VeriFuzz/Simulator/General.hs50
-rw-r--r--src/VeriFuzz/Simulator/Icarus.hs66
-rw-r--r--src/VeriFuzz/Simulator/Xst.hs58
-rw-r--r--src/VeriFuzz/Simulator/Yosys.hs94
4 files changed, 268 insertions, 0 deletions
diff --git a/src/VeriFuzz/Simulator/General.hs b/src/VeriFuzz/Simulator/General.hs
new file mode 100644
index 0000000..a024029
--- /dev/null
+++ b/src/VeriFuzz/Simulator/General.hs
@@ -0,0 +1,50 @@
+{-|
+Module : VeriFuzz.Simulator.General
+Description : Class of the simulator.
+Copyright : (c) 2018-2019, Yann Herklotz Grave
+License : BSD-3
+Maintainer : ymherklotz [at] gmail [dot] com
+Stability : experimental
+Portability : POSIX
+
+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 Shelly
+import VeriFuzz.Verilog.AST
+
+-- | Simulator class.
+class Simulator a where
+ toText :: a -> Text
+
+-- | Simulation type class.
+class (Simulator a) => Simulate a where
+ runSim :: a -- ^ Simulator instance
+ -> ModDecl -- ^ Module to simulate
+ -> [ByteString] -- ^ Inputs to simulate
+ -> Sh Int -- ^ Returns the value of the hash at the output of the testbench.
+
+-- | Synthesize type class.
+class (Simulator a) => Synthesize a where
+ runSynth :: a -- ^ Synthesize tool instance
+ -> ModDecl -- ^ Module to synthesize
+ -> FilePath -- ^ Output verilog file for the module
+ -> Sh () -- ^ does not return any values
+
+timeout :: FilePath -> [Text] -> Sh Text
+timeout = command1 "timeout" ["180"] . toTextIgnore
+
+timeout_ :: FilePath -> [Text] -> Sh ()
+timeout_ = command1_ "timeout" ["180"] . toTextIgnore
+
+-- | Helper function to convert bytestrings to integers
+bsToI :: ByteString -> Integer
+bsToI = B.foldl' (\i b -> (i `shiftL` 8) + fromIntegral b) 0
+{-# INLINE bsToI #-}
diff --git a/src/VeriFuzz/Simulator/Icarus.hs b/src/VeriFuzz/Simulator/Icarus.hs
new file mode 100644
index 0000000..744deb8
--- /dev/null
+++ b/src/VeriFuzz/Simulator/Icarus.hs
@@ -0,0 +1,66 @@
+{-|
+Module : VeriFuzz.Simulator.Icarus
+Description : Icarus verilog module.
+Copyright : (c) 2018-2019, Yann Herklotz Grave
+License : BSD-3
+Maintainer : ymherklotz [at] gmail [dot] com
+Stability : experimental
+Portability : POSIX
+
+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.Hashable
+import Data.List (transpose)
+import Data.Text (Text)
+import qualified Data.Text as T
+import Prelude hiding (FilePath)
+import Shelly
+import Text.Shakespeare.Text (st)
+import VeriFuzz.Simulator.General
+import VeriFuzz.Verilog
+
+data Icarus = Icarus { icarusPath :: FilePath
+ , vvpPath :: FilePath
+ }
+
+instance Simulator Icarus where
+ toText _ = "iverilog"
+
+instance Simulate Icarus where
+ runSim = runSimIcarus
+
+defaultIcarus :: Icarus
+defaultIcarus = Icarus "iverilog" "vvp"
+
+addDisplay :: [Stmnt] -> [Stmnt]
+addDisplay s =
+ concat $ transpose [s, replicate l $ TimeCtrl 1 Nothing
+ , replicate l . SysTaskEnable $ Task "display" ["%h", Id "y"]]
+ where
+ l = length s
+
+assignFunc :: [Port] -> ByteString -> Stmnt
+assignFunc inp bs =
+ NonBlockAssign . Assign conc Nothing . Number (B.length bs * 4) $ bsToI bs
+ where
+ conc = RegConcat (portToExpr <$> inp)
+
+runSimIcarus :: Icarus -> ModDecl -> [ByteString] -> Sh Int
+runSimIcarus sim m bss = do
+ let tb = ModDecl "main" [] []
+ [ Initial $
+ fold (addDisplay $ assignFunc (m ^. modInPorts) <$> bss)
+ <> (SysTaskEnable $ Task "finish" [])
+ ]
+ let newtb = instantiateMod m tb
+ let modWithTb = VerilogSrc $ Description <$> [newtb, m]
+ writefile "main.v" $ genSource modWithTb
+ run_ (icarusPath sim) ["-o", "main", "main.v"]
+ hash <$> run (vvpPath sim) ["main"]
diff --git a/src/VeriFuzz/Simulator/Xst.hs b/src/VeriFuzz/Simulator/Xst.hs
new file mode 100644
index 0000000..902b244
--- /dev/null
+++ b/src/VeriFuzz/Simulator/Xst.hs
@@ -0,0 +1,58 @@
+{-|
+Module : VeriFuzz.Simulator.Xst
+Description : Xst (ise) simulator implementation.
+Copyright : (c) 2018-2019, Yann Herklotz Grave
+License : BSD-3
+Maintainer : ymherklotz [at] gmail [dot] com
+Stability : experimental
+Portability : POSIX
+
+Xst (ise) simulator implementation.
+-}
+
+{-# LANGUAGE QuasiQuotes #-}
+
+module VeriFuzz.Simulator.Xst where
+
+import Control.Lens hiding ((<.>))
+import Data.Text (Text)
+import qualified Data.Text as T
+import Prelude hiding (FilePath)
+import Shelly
+import Text.Shakespeare.Text (st)
+import VeriFuzz.Simulator.General
+import VeriFuzz.Verilog.AST
+import VeriFuzz.Verilog.CodeGen
+
+data Xst = Xst { xstPath :: FilePath
+ , netgenPath :: FilePath
+ }
+
+instance Simulator Xst where
+ toText _ = "xst"
+
+instance Synthesize Xst where
+ runSynth = runSynthXst
+
+defaultXst :: Xst
+defaultXst = Xst "/opt/Xilinx/14.7/ISE_DS/ISE/bin/lin64/xst" "/opt/Xilinx/14.7/ISE_DS/ISE/bin/lin64/netgen"
+
+runSynthXst :: Xst -> ModDecl -> FilePath -> Sh ()
+runSynthXst sim mod outf = do
+ writefile xstFile [st|run
+-ifn #{modName}.prj -ofn #{modName} -p artix7 -top #{modName}
+-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"
+|]
+ writefile prjFile [st|verilog work "rtl.v"|]
+ writefile "rtl.v" $ genSource mod
+ timeout_ (xstPath sim) ["-ifn", toTextIgnore xstFile]
+ run_ (netgenPath sim) ["-w", "-ofmt", "verilog", toTextIgnore $ modFile <.> "ngc", toTextIgnore outf]
+ run_ "sed" ["-i", "/^`ifndef/,/^`endif/ d; s/ *Timestamp: .*//;", toTextIgnore outf]
+ where
+ modName = mod ^. moduleId . getIdentifier
+ modFile = fromText modName
+ xstFile = modFile <.> "xst"
+ prjFile = modFile <.> "prj"
+ vFile = modFile <.> "v"
diff --git a/src/VeriFuzz/Simulator/Yosys.hs b/src/VeriFuzz/Simulator/Yosys.hs
new file mode 100644
index 0000000..3ac732d
--- /dev/null
+++ b/src/VeriFuzz/Simulator/Yosys.hs
@@ -0,0 +1,94 @@
+{-|
+Module : VeriFuzz.Simulator.Yosys
+Description : Yosys simulator implementation.
+Copyright : (c) 2018-2019, Yann Herklotz Grave
+License : BSD-3
+Maintainer : ymherklotz [at] gmail [dot] com
+Stability : experimental
+Portability : POSIX
+
+Yosys simulator implementation.
+-}
+
+{-# LANGUAGE QuasiQuotes #-}
+
+module VeriFuzz.Simulator.Yosys where
+
+import Control.Lens
+import Data.ByteString (ByteString)
+import qualified Data.ByteString as B
+import Data.Maybe (fromMaybe)
+import Data.Text (Text)
+import qualified Data.Text as T
+import Prelude hiding (FilePath)
+import Shelly
+import Text.Shakespeare.Text (st)
+import VeriFuzz.Simulator.General
+import VeriFuzz.Verilog
+
+newtype Yosys = Yosys { yosysPath :: FilePath }
+
+instance Simulator Yosys where
+ toText _ = "yosys"
+
+instance Simulate Yosys where
+ runSim = runSimYosys
+
+instance Synthesize Yosys where
+ runSynth = runSynthYosys
+
+defaultYosys :: Yosys
+defaultYosys = Yosys "/usr/bin/yosys"
+
+writeSimFile :: Yosys -- ^ Simulator instance
+ -> ModDecl -- ^ Current module
+ -> FilePath -- ^ Output sim file
+ -> Sh ()
+writeSimFile sim m file = do
+ writefile "rtl.v" $ genSource m
+ writefile file [st|read_verilog rtl.v; proc;;
+rename mod mod_rtl
+|]
+
+runSimYosys :: Yosys -> ModDecl -> [ByteString] -> Sh Int
+runSimYosys sim ver tb = return 0
+
+runSynthYosys :: Yosys -> ModDecl -> FilePath -> Sh ()
+runSynthYosys sim m outf = do
+ writefile inpf $ genSource m
+ run_ (yosysPath sim) ["-q", "-b", "verilog -noattr", "-o", out, "-S", inp]
+ where
+ inpf = "rtl.v"
+ inp = toTextIgnore inpf
+ out = toTextIgnore outf
+
+writeSatFile :: (Synthesize a, Synthesize b) => Text -> a -> Maybe b -> ModDecl -> Sh ()
+writeSatFile checkFile sim1 sim2 m =
+ writefile (fromText checkFile) [st|read_verilog syn_#{toText sim1}.v
+rename #{modName} #{modName}_1
+read_verilog syn_#{idSim2}.v
+rename #{modName} #{modName}_2
+read_verilog top.v
+proc; opt_clean
+flatten #{modName}
+! touch test.#{toText sim1}.#{idSim2}.input_ok
+sat -timeout 20 -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 #{modName}
+|]
+ where
+ idSim2 = maybe "rtl" toText sim2
+ modName = m ^. moduleId . getIdentifier
+ ids = T.intercalate "," $ allVars m ^.. traverse . getIdentifier
+
+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
+
+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
+ writeSatFile checkFile sim1 sim2 m
+ 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|]
generated by cgit (git 2.34.1) at 2024-07-07 21:18:19 +0000