diff options
author | Yann Herklotz <ymherklotz@gmail.com> | 2019-02-01 19:34:44 +0000 |
---|---|---|
committer | Yann Herklotz <ymherklotz@gmail.com> | 2019-02-01 19:34:44 +0000 |
commit | a38289ca9d96e97bc4e65b67c50f5805d56a3d86 (patch) | |
tree | 8bd1793ab02c3efe5cf668c045c82d77d61d8510 /src/VeriFuzz/Internal | |
parent | afc9287534bc04ae139fa1d16c80ac0fc55e8767 (diff) | |
download | verismith-a38289ca9d96e97bc4e65b67c50f5805d56a3d86.tar.gz verismith-a38289ca9d96e97bc4e65b67c50f5805d56a3d86.zip |
Structure changes
Diffstat (limited to 'src/VeriFuzz/Internal')
-rw-r--r-- | src/VeriFuzz/Internal/Circuit.hs (renamed from src/VeriFuzz/Internal/Gen.hs) | 4 | ||||
-rw-r--r-- | src/VeriFuzz/Internal/Shared.hs | 18 | ||||
-rw-r--r-- | src/VeriFuzz/Internal/Simulator.hs | 90 |
3 files changed, 92 insertions, 20 deletions
diff --git a/src/VeriFuzz/Internal/Gen.hs b/src/VeriFuzz/Internal/Circuit.hs index d2e4e3c..0634f01 100644 --- a/src/VeriFuzz/Internal/Gen.hs +++ b/src/VeriFuzz/Internal/Circuit.hs @@ -1,5 +1,5 @@ {-| -Module : VeriFuzz.Internal.Gen +Module : VeriFuzz.Internal.Circuit Description : Internal helpers for generation. Copyright : (c) 2018-2019, Yann Herklotz Grave License : BSD-3 @@ -10,7 +10,7 @@ Portability : POSIX Internal helpers for generation. -} -module VeriFuzz.Internal.Gen where +module VeriFuzz.Internal.Circuit where import Data.Graph.Inductive (Graph, Node) import qualified Data.Graph.Inductive as G diff --git a/src/VeriFuzz/Internal/Shared.hs b/src/VeriFuzz/Internal/Shared.hs deleted file mode 100644 index c7d2760..0000000 --- a/src/VeriFuzz/Internal/Shared.hs +++ /dev/null @@ -1,18 +0,0 @@ -{-| -Module : VeriFuzz.Internal.Shared -Description : Shared high level code used in the other modules internally. -Copyright : (c) 2018-2019, Yann Herklotz Grave -License : BSD-3 -Maintainer : ymherklotz [at] gmail [dot] com -Stability : experimental -Portability : POSIX - -Shared high level code used in the other modules internally. --} - -module VeriFuzz.Internal.Shared where - --- | Converts unsafe list functions in the Prelude to a safe version. -safe :: ([a] -> b) -> [a] -> Maybe b -safe _ [] = Nothing -safe f l = Just $ f l diff --git a/src/VeriFuzz/Internal/Simulator.hs b/src/VeriFuzz/Internal/Simulator.hs new file mode 100644 index 0000000..4f8fd5a --- /dev/null +++ b/src/VeriFuzz/Internal/Simulator.hs @@ -0,0 +1,90 @@ +{-| +Module : VeriFuzz.Internal.Simulator +Description : Template file for different configuration files +Copyright : (c) 2019, Yann Herklotz Grave +License : GPL-3 +Maintainer : ymherklotz [at] gmail [dot] com +Stability : experimental +Portability : POSIX + +Template file for different configuration files. +-} + +{-# LANGUAGE QuasiQuotes #-} + +module VeriFuzz.Internal.Simulator where + +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 + +-- brittany-disable-next-binding +yosysSatConfig :: (Simulator a, Simulator b) => a -> Maybe b -> ModDecl -> Text +yosysSatConfig sim1 sim2 m = [st|read_verilog syn_#{toText sim1}.v +rename #{mi} #{mi}_1 +read_verilog syn_#{idSim2}.v +rename #{mi} #{mi}_2 +read_verilog top.v +proc; opt_clean +flatten #{mi} +! touch test.#{toText sim1}.#{idSim2}.input_ok +sat -timeout 20 -show-all -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 #{mi} +|] + where + idSim2 = maybe "rtl" toText sim2 + mi = modName m + +-- brittany-disable-next-binding +yosysSimConfig :: Text +yosysSimConfig = [st|read_verilog rtl.v; proc;; +rename mod mod_rtl +|] + +-- brittany-disable-next-binding +xstSynthConfig :: ModDecl -> Text +xstSynthConfig m = [st|run +-ifn #{mi}.prj -ofn #{mi} -p artix7 -top #{mi} +-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" +|] + where + mi = modName m + +-- brittany-disable-next-binding +sbyConfig :: (Simulator a, Simulator b) => FilePath -> a -> Maybe b -> ModDecl -> Text +sbyConfig bd sim1 sim2 m = [st|[options] +mode prove + +[engines] +smtbmc + +[script] +#{readL} +read -formal syn_#{toText sim1}.v +rename #{mi} #{mi}_1 +read -formal syn_#{maybe "rtl" toText sim2}.v +rename #{mi} #{mi}_2 +read -formal top.v +prep -top #{mi} + +[files] +#{depList} +syn_#{maybe "rtl" toText sim2}.v +syn_#{toText sim1}.v +top.v +|] + where + mi = modName m + 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 |