{-# LANGUAGE QuasiQuotes #-}

-- |
-- Module      : Verismith.Tool.Template
-- Description : Template file for different configuration files
-- Copyright   : (c) 2019, Yann Herklotz
-- License     : GPL-3
-- Maintainer  : yann [at] yannherklotz [dot] com
-- Stability   : experimental
-- Portability : POSIX
--
-- Template file for different configuration files.
module Verismith.Tool.Template
  ( yosysSynthConfigStd,
    yosysSatConfig,
    yosysSimConfig,
    quartusLightSynthConfig,
    quartusSynthConfig,
    xstSynthConfig,
    vivadoSynthConfig,
    sbyConfig,
    icarusTestbench,
  )
where

import Control.Lens ((^..))
import Data.Maybe (fromMaybe)
import Data.Text (Text)
import qualified Data.Text as T
import Shelly
import Verismith.Tool.Internal
import Verismith.Verilog.AST
import Verismith.Verilog.CodeGen
import Prelude hiding (FilePath)

rename :: Text -> [Text] -> Text
rename :: Text -> [Text] -> Text
rename Text
end [Text]
entries =
  Text -> [Text] -> Text
T.intercalate Text
"\n" ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$
    (Text -> Text -> Text) -> Text -> Text -> Text
forall a b c. (a -> b -> c) -> b -> a -> c
flip Text -> Text -> Text
forall a. Monoid a => a -> a -> a
mappend Text
end
      (Text -> Text) -> (Text -> Text) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text -> Text
forall a. Monoid a => a -> a -> a
mappend Text
"rename "
      (Text -> Text) -> (Text -> Text) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text
doubleName
      (Text -> Text) -> [Text] -> [Text]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Text]
entries
{-# INLINE rename #-}

doubleName :: Text -> Text
doubleName :: Text -> Text
doubleName Text
n = Text
n Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
n
{-# INLINE doubleName #-}

outputText :: (Synthesiser a) => a -> Text
outputText :: forall a. Synthesiser a => a -> Text
outputText = FilePath -> Text
toTextIgnore (FilePath -> Text) -> (a -> FilePath) -> a -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> FilePath
forall a. Synthesiser a => a -> FilePath
synthOutput

yosysSynthConfig :: (Synthesiser a) => Text -> a -> FilePath -> Text
yosysSynthConfig :: forall a. Synthesiser a => Text -> a -> FilePath -> Text
yosysSynthConfig Text
t a
a FilePath
fp =
  [Text] -> Text
T.unlines
    [ Text
"read_verilog " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
toTextIgnore FilePath
fp,
      Text
t,
      Text
"write_verilog " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> a -> Text
forall a. Synthesiser a => a -> Text
outputText a
a
    ]

yosysSynthConfigStd :: (Synthesiser a) => a -> FilePath -> Text
yosysSynthConfigStd :: forall a. Synthesiser a => a -> FilePath -> Text
yosysSynthConfigStd = Text -> a -> FilePath -> Text
forall a. Synthesiser a => Text -> a -> FilePath -> Text
yosysSynthConfig Text
"synth"

yosysSatConfig :: (Synthesiser a, Synthesiser b) => a -> b -> (SourceInfo ann) -> Text
yosysSatConfig :: forall a b ann.
(Synthesiser a, Synthesiser b) =>
a -> b -> SourceInfo ann -> Text
yosysSatConfig a
sim1 b
sim2 (SourceInfo Text
top Verilog ann
src) =
  [Text] -> Text
T.unlines
    [ Text
"read_verilog " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> a -> Text
forall a. Synthesiser a => a -> Text
outputText a
sim1,
      Text -> [Text] -> Text
rename Text
"_1" [Text]
mis,
      Text
"read_verilog syn_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> b -> Text
forall a. Synthesiser a => a -> Text
outputText b
sim2 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
".v",
      Text -> [Text] -> Text
rename Text
"_2" [Text]
mis,
      Text
"read_verilog " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
top Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
".v",
      Text
"proc; opt_clean",
      Text
"flatten " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
top,
      Text
"sat -timeout 20 -show-all -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
top
    ]
  where
    mis :: [Text]
mis = Verilog ann
src Verilog ann -> Getting (Endo [Text]) (Verilog ann) Text -> [Text]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. Getting (Endo [Text]) (Verilog ann) Text
forall a (f :: * -> *).
Applicative f =>
(Text -> f Text) -> Verilog a -> f (Verilog a)
getSourceId

yosysSimConfig :: Text
yosysSimConfig :: Text
yosysSimConfig = Text
"read_verilog rtl.v; proc;;\nrename mod mod_rtl"

quartusLightSynthConfig :: (Synthesiser a) => a -> FilePath -> Text -> FilePath -> Text
quartusLightSynthConfig :: forall a.
Synthesiser a =>
a -> FilePath -> Text -> FilePath -> Text
quartusLightSynthConfig a
q FilePath
sdc Text
top FilePath
fp =
  [Text] -> Text
T.unlines
    [ Text
"load_package flow",
      Text
"",
      Text
"project_new -overwrite " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
top,
      Text
"",
      Text
"set_global_assignment -name FAMILY \"Cyclone V\"",
      Text
"set_global_assignment -name SYSTEMVERILOG_FILE " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
toTextIgnore FilePath
fp,
      Text
"set_global_assignment -name TOP_LEVEL_ENTITY " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
top,
      Text
"set_global_assignment -name SDC_FILE " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
toTextIgnore FilePath
sdc,
      Text
"set_global_assignment -name INI_VARS \"qatm_force_vqm=on;\"",
      Text
"set_global_assignment -name NUM_PARALLEL_PROCESSORS 2",
      Text
"set_instance_assignment -name VIRTUAL_PIN ON -to *",
      Text
"",
      Text
"execute_module -tool map",
      Text
"execute_module -tool fit",
      Text
"execute_module -tool sta -args \"--mode=implement\"",
      Text
"execute_module -tool eda -args \"--simulation --tool=vcs\"",
      Text
"",
      Text
"project_close"
    ]

quartusSynthConfig :: (Synthesiser a) => a -> FilePath -> Text -> FilePath -> Text
quartusSynthConfig :: forall a.
Synthesiser a =>
a -> FilePath -> Text -> FilePath -> Text
quartusSynthConfig a
q FilePath
sdc Text
top FilePath
fp =
  [Text] -> Text
T.unlines
    [ Text
"load_package flow",
      Text
"",
      Text
"project_new -overwrite " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
top,
      Text
"",
      Text
"set_global_assignment -name FAMILY \"Cyclone 10 GX\"",
      Text
"set_global_assignment -name SYSTEMVERILOG_FILE " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
toTextIgnore FilePath
fp,
      Text
"set_global_assignment -name TOP_LEVEL_ENTITY " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
top,
      Text
"set_global_assignment -name SDC_FILE " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
toTextIgnore FilePath
sdc,
      Text
"set_global_assignment -name INI_VARS \"qatm_force_vqm=on;\"",
      Text
"set_global_assignment -name NUM_PARALLEL_PROCESSORS 2",
      Text
"set_instance_assignment -name VIRTUAL_PIN ON -to *",
      Text
"",
      Text
"execute_module -tool syn",
      Text
"execute_module -tool eda -args \"--simulation --tool=vcs\"",
      Text
"",
      Text
"project_close"
    ]

xstSynthConfig :: Text -> Text
xstSynthConfig :: Text -> Text
xstSynthConfig Text
top =
  [Text] -> Text
T.unlines
    [ Text
"run",
      Text
"-ifn " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
top Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
".prj -ofn " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
top Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" -p artix7 -top " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
top,
      Text
"-iobuf NO -ram_extract NO -rom_extract NO -use_dsp48 NO",
      Text
"-fsm_extract YES -fsm_encoding Auto",
      Text
"-change_error_to_warning \"HDLCompiler:226 HDLCompiler:1832\""
    ]

vivadoSynthConfig :: Text -> Text -> Text
vivadoSynthConfig :: Text -> Text -> Text
vivadoSynthConfig Text
top Text
outf =
  [Text] -> Text
T.unlines
    [ Text
"# CRITICAL WARNING: [Synth 8-5821] Potential divide by zero",
      Text
"set_msg_config -id {Synth 8-5821} -new_severity {WARNING}",
      Text
"",
      Text
"read_verilog rtl.v",
      Text
"synth_design -part xc7k70t -top " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
top,
      Text
"write_verilog -force " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
outf
    ]

sbyConfig :: (Synthesiser a, Synthesiser b) => Maybe Text -> FilePath -> a -> b -> (SourceInfo ann) -> Text
sbyConfig :: forall a b ann.
(Synthesiser a, Synthesiser b) =>
Maybe Text -> FilePath -> a -> b -> SourceInfo ann -> Text
sbyConfig Maybe Text
mt FilePath
datadir a
sim1 b
sim2 (SourceInfo Text
top Verilog ann
_) =
  [Text] -> Text
T.unlines
    [ Text
"[options]",
      Text
"multiclock on",
      Text
"mode prove",
      Text
"aigsmt " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> Maybe Text -> Text
forall a. a -> Maybe a -> a
fromMaybe Text
"none" Maybe Text
mt,
      Text
"",
      Text
"[engines]",
      Text
"abc pdr",
      Text
"",
      Text
"[script]",
      Text
readL,
      Text
"read -formal " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> a -> Text
forall a. Synthesiser a => a -> Text
outputText a
sim1,
      Text
"read -formal " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> b -> Text
forall a. Synthesiser a => a -> Text
outputText b
sim2,
      Text
"read -formal top.v",
      Text
"prep -top " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
top,
      Text
"",
      Text
"[files]",
      Text
depList,
      b -> Text
forall a. Synthesiser a => a -> Text
outputText b
sim2,
      a -> Text
forall a. Synthesiser a => a -> Text
outputText a
sim1,
      Text
"top.v"
    ]
  where
    deps :: [Text]
deps = [Text
"cells_cmos.v", Text
"cells_cyclone_v.v", Text
"cells_verific.v", Text
"cells_xilinx_7.v", Text
"cells_yosys.v"]
    depList :: Text
depList =
      Text -> [Text] -> Text
T.intercalate Text
"\n" ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$
        FilePath -> Text
toTextIgnore
          (FilePath -> Text) -> (Text -> FilePath) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FilePath
datadir FilePath -> FilePath -> FilePath
forall filepath1 filepath2.
(ToFilePath filepath1, ToFilePath filepath2) =>
filepath1 -> filepath2 -> FilePath
</> Text -> FilePath
fromText Text
"data" FilePath -> FilePath -> FilePath
forall filepath1 filepath2.
(ToFilePath filepath1, ToFilePath filepath2) =>
filepath1 -> filepath2 -> FilePath
</>)
          (FilePath -> FilePath) -> (Text -> FilePath) -> Text -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
fromText
          (Text -> Text) -> [Text] -> [Text]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Text]
deps
    readL :: Text
readL = Text -> [Text] -> Text
T.intercalate Text
"\n" ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ Text -> Text -> Text
forall a. Monoid a => a -> a -> a
mappend Text
"read -formal " (Text -> Text) -> [Text] -> [Text]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Text]
deps

icarusTestbench :: (Synthesiser a, Show ann) => FilePath -> (Verilog ann) -> a -> Text
icarusTestbench :: forall a ann.
(Synthesiser a, Show ann) =>
FilePath -> Verilog ann -> a -> Text
icarusTestbench FilePath
datadir Verilog ann
t a
synth1 =
  [Text] -> Text
T.unlines
    [ Text
"`include \"" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
ddir Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"/data/cells_cmos.v\"",
      Text
"`include \"" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
ddir Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"/data/cells_cyclone_v.v\"",
      Text
"`include \"" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
ddir Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"/data/cells_verific.v\"",
      Text
"`include \"" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
ddir Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"/data/cells_xilinx_7.v\"",
      Text
"`include \"" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
ddir Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"/data/cells_yosys.v\"",
      Text
"`include \"" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
toTextIgnore (a -> FilePath
forall a. Synthesiser a => a -> FilePath
synthOutput a
synth1) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\"",
      Text
"",
      Verilog ann -> Text
forall a. Source a => a -> Text
genSource Verilog ann
t
    ]
  where
    ddir :: Text
ddir = FilePath -> Text
toTextIgnore FilePath
datadir