From 72ca7b273a8adf421d481e0caa97caa8a565187a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 18 Apr 2019 23:42:48 +0100 Subject: Add output information to Type --- src/VeriFuzz/Sim/Internal.hs | 1 - src/VeriFuzz/Sim/Quartus.hs | 10 +++++----- src/VeriFuzz/Sim/Template.hs | 18 ++++++++++-------- src/VeriFuzz/Sim/Vivado.hs | 10 +++++----- src/VeriFuzz/Sim/XST.hs | 12 ++++++------ src/VeriFuzz/Sim/Yosys.hs | 21 ++++++++++----------- 6 files changed, 36 insertions(+), 36 deletions(-) (limited to 'src/VeriFuzz/Sim') diff --git a/src/VeriFuzz/Sim/Internal.hs b/src/VeriFuzz/Sim/Internal.hs index 2d06819..6e02482 100644 --- a/src/VeriFuzz/Sim/Internal.hs +++ b/src/VeriFuzz/Sim/Internal.hs @@ -80,7 +80,6 @@ instance Monoid Failed where class Tool a => Synthesiser a where runSynth :: a -- ^ Synthesiser tool instance -> SourceInfo -- ^ Run information - -> FilePath -- ^ Output verilog file for the module -> ResultSh () -- ^ does not return any values synthOutput :: a -> FilePath setSynthOutput :: a -> FilePath -> a diff --git a/src/VeriFuzz/Sim/Quartus.hs b/src/VeriFuzz/Sim/Quartus.hs index beb7f10..5bda0be 100644 --- a/src/VeriFuzz/Sim/Quartus.hs +++ b/src/VeriFuzz/Sim/Quartus.hs @@ -37,13 +37,13 @@ instance Tool Quartus where instance Synthesiser Quartus where runSynth = runSynthQuartus synthOutput = quartusOutput - setSynthOutput (Quartus a _) f = Quartus a f + setSynthOutput (Quartus a _) = Quartus a defaultQuartus :: Quartus -defaultQuartus = Quartus Nothing "quartus/syn_quartus.v" +defaultQuartus = Quartus Nothing "syn_quartus.v" -runSynthQuartus :: Quartus -> SourceInfo -> FilePath -> ResultSh () -runSynthQuartus sim (SourceInfo top src) outf = do +runSynthQuartus :: Quartus -> SourceInfo -> ResultSh () +runSynthQuartus sim (SourceInfo top src) = do dir <- liftSh pwd let ex = execute_ SynthFail dir "quartus" liftSh $ do @@ -54,7 +54,7 @@ runSynthQuartus sim (SourceInfo top src) outf = do ex (exec "quartus_fit") [top, "--part=5CGXFC7D6F31C6"] ex (exec "quartus_eda") [top, "--simulation", "--tool=vcs"] liftSh $ do - cp (fromText "simulation/vcs" fromText top <.> "vo") outf + cp (fromText "simulation/vcs" fromText top <.> "vo") $ synthOutput sim echoP "Quartus synthesis done" where inpf = "rtl.v" diff --git a/src/VeriFuzz/Sim/Template.hs b/src/VeriFuzz/Sim/Template.hs index f630ea6..93f24a3 100644 --- a/src/VeriFuzz/Sim/Template.hs +++ b/src/VeriFuzz/Sim/Template.hs @@ -43,16 +43,18 @@ doubleName :: Text -> Text doubleName n = n <> " " <> n {-# INLINE doubleName #-} +outputText :: Synthesiser a => a -> Text +outputText = toTextIgnore . synthOutput + -- 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 +yosysSatConfig :: (Synthesiser a, Synthesiser b) => a -> Maybe b -> SourceInfo -> Text +yosysSatConfig sim1 sim2 (SourceInfo top src) = [st|read_verilog #{outputText sim1} #{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 @@ -86,7 +88,7 @@ write_verilog -force #{outf} |] -- brittany-disable-next-binding -sbyConfig :: (Tool a, Tool b) => FilePath -> a -> Maybe b -> SourceInfo -> Text +sbyConfig :: (Synthesiser a, Synthesiser b) => FilePath -> a -> Maybe b -> SourceInfo -> Text sbyConfig bd sim1 sim2 (SourceInfo top src) = [st|[options] mode prove @@ -95,17 +97,17 @@ smtbmc z3 [script] #{readL} -read -formal syn_#{toText sim1}.v +read -formal #{outputText sim1} #{rename "_1" mis} -read -formal syn_#{maybe "rtl" toText sim2}.v +read -formal #{maybe "rtl.v" outputText sim2} #{rename "_2" mis} read -formal top.v prep -top #{top} [files] #{depList} -syn_#{maybe "rtl" toText sim2}.v -syn_#{toText sim1}.v +#{maybe "rtl.v" outputText sim2} +#{outputText sim1} top.v |] where diff --git a/src/VeriFuzz/Sim/Vivado.hs b/src/VeriFuzz/Sim/Vivado.hs index 7cf6d4b..d213a12 100644 --- a/src/VeriFuzz/Sim/Vivado.hs +++ b/src/VeriFuzz/Sim/Vivado.hs @@ -38,16 +38,16 @@ instance Tool Vivado where instance Synthesiser Vivado where runSynth = runSynthVivado synthOutput = vivadoOutput - setSynthOutput (Vivado a _) f = Vivado a f + setSynthOutput (Vivado a _) = Vivado a defaultVivado :: Vivado -defaultVivado = Vivado "vivado" "vivado/syn_vivado.v" +defaultVivado = Vivado "vivado" "syn_vivado.v" -runSynthVivado :: Vivado -> SourceInfo -> FilePath -> ResultSh () -runSynthVivado sim (SourceInfo top src) outf = do +runSynthVivado :: Vivado -> SourceInfo -> ResultSh () +runSynthVivado sim (SourceInfo top src) = do dir <- liftSh pwd liftSh $ do - writefile vivadoTcl . vivadoSynthConfig top $ toTextIgnore outf + writefile vivadoTcl . vivadoSynthConfig top . toTextIgnore $ synthOutput sim writefile "rtl.v" $ genSource src run_ "sed" ["s/^module/(* use_dsp48=\"no\" *) module/;", "-i", "rtl.v"] echoP "Vivado: run" diff --git a/src/VeriFuzz/Sim/XST.hs b/src/VeriFuzz/Sim/XST.hs index b5b1b8b..e5e3e06 100644 --- a/src/VeriFuzz/Sim/XST.hs +++ b/src/VeriFuzz/Sim/XST.hs @@ -42,13 +42,13 @@ instance Tool XST where instance Synthesiser XST where runSynth = runSynthXST synthOutput = xstOutput - setSynthOutput (XST a b _) f = XST a b f + setSynthOutput (XST a b _) = XST a b defaultXST :: XST -defaultXST = XST "xst" "netgen" "xst/syn_xst.v" +defaultXST = XST "xst" "netgen" "syn_xst.v" -runSynthXST :: XST -> SourceInfo -> FilePath -> ResultSh () -runSynthXST sim (SourceInfo top src) outf = do +runSynthXST :: XST -> SourceInfo -> ResultSh () +runSynthXST sim (SourceInfo top src) = do dir <- liftSh pwd let exec = execute_ SynthFail dir "xst" liftSh $ do @@ -64,7 +64,7 @@ runSynthXST sim (SourceInfo top src) outf = do , "-ofmt" , "verilog" , toTextIgnore $ modFile <.> "ngc" - , toTextIgnore outf + , toTextIgnore $ synthOutput sim ] liftSh $ do echoP "XST: clean" @@ -72,7 +72,7 @@ runSynthXST sim (SourceInfo top src) outf = do "sed" [ "-i" , "/^`ifndef/,/^`endif/ d; s/ *Timestamp: .*//;" - , toTextIgnore outf + , toTextIgnore $ synthOutput sim ] echoP "XST: done" where diff --git a/src/VeriFuzz/Sim/Yosys.hs b/src/VeriFuzz/Sim/Yosys.hs index 98244a6..f219e01 100644 --- a/src/VeriFuzz/Sim/Yosys.hs +++ b/src/VeriFuzz/Sim/Yosys.hs @@ -42,16 +42,16 @@ instance Tool Yosys where instance Synthesiser Yosys where runSynth = runSynthYosys synthOutput = yosysOutput - setSynthOutput (Yosys a _) f = Yosys a f + setSynthOutput (Yosys a _) = Yosys a instance Show Yosys where show _ = "yosys" defaultYosys :: Yosys -defaultYosys = Yosys "yosys" "yosys/syn_yosys.v" +defaultYosys = Yosys "yosys" "syn_yosys.v" -runSynthYosys :: Yosys -> SourceInfo -> FilePath -> ResultSh () -runSynthYosys sim (SourceInfo _ src) outf = ( SynthFail) . liftSh $ do +runSynthYosys :: Yosys -> SourceInfo -> ResultSh () +runSynthYosys sim (SourceInfo _ src) = ( SynthFail) . liftSh $ do dir <- pwd writefile inpf $ genSource src echoP "Yosys: synthesis" @@ -63,13 +63,13 @@ runSynthYosys sim (SourceInfo _ src) outf = ( SynthFail) . liftSh $ do where inpf = "rtl.v" inp = toTextIgnore inpf - out = toTextIgnore outf + out = toTextIgnore $ synthOutput sim runMaybeSynth :: (Synthesiser a) => Maybe a -> SourceInfo -> ResultSh () runMaybeSynth (Just sim) srcInfo = - runSynth sim srcInfo $ fromText [st|syn_#{toText sim}.v|] + runSynth sim srcInfo runMaybeSynth Nothing (SourceInfo _ src) = - liftSh . writefile "syn_rtl.v" $ genSource src + liftSh . writefile "rtl.v" $ genSource src runEquivYosys :: (Synthesiser a, Synthesiser b) @@ -87,7 +87,7 @@ runEquivYosys yosys sim1 sim2 srcInfo = do $ srcInfo ^. mainModule writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo - runSynth sim1 srcInfo $ fromText [st|syn_#{toText sim1}.v|] + runSynth sim1 srcInfo runMaybeSynth sim2 srcInfo liftSh $ do echoP "Yosys: equivalence check" @@ -108,7 +108,6 @@ runEquiv _ sim1 sim2 srcInfo = do root <- liftSh rootPath dir <- liftSh pwd liftSh $ do - echoP "SymbiYosys: setup" writefile "top.v" . genSource . initMod @@ -116,6 +115,6 @@ runEquiv _ sim1 sim2 srcInfo = do $ srcInfo ^. mainModule writefile "test.sby" $ sbyConfig root sim1 sim2 srcInfo - liftSh $ echoP "SymbiYosys: run" + liftSh $ echoP "Running SymbiYosys" execute_ EquivFail dir "symbiyosys" "sby" ["-f", "test.sby"] - liftSh $ echoP "SymbiYosys: done" + liftSh $ echoP "SymbiYosys equivalence check passed" -- cgit