From fd4b0b5152f94cd406f2e5de86ce7ed0a4d2cbd0 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 2 Apr 2019 19:47:32 +0100 Subject: Large refactor with passing tests --- src/VeriFuzz/Sim/Yosys.hs | 106 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 106 insertions(+) create mode 100644 src/VeriFuzz/Sim/Yosys.hs (limited to 'src/VeriFuzz/Sim/Yosys.hs') diff --git a/src/VeriFuzz/Sim/Yosys.hs b/src/VeriFuzz/Sim/Yosys.hs new file mode 100644 index 0000000..0d0c98b --- /dev/null +++ b/src/VeriFuzz/Sim/Yosys.hs @@ -0,0 +1,106 @@ +{-| +Module : VeriFuzz.Sim.Yosys +Description : Yosys simulator implementation. +Copyright : (c) 2018-2019, Yann Herklotz +License : BSD-3 +Maintainer : ymherklotz [at] gmail [dot] com +Stability : experimental +Portability : POSIX + +Yosys simulator implementation. +-} + +{-# LANGUAGE QuasiQuotes #-} + +module VeriFuzz.Sim.Yosys + ( Yosys(..) + , defaultYosys + , runEquiv + , runEquivYosys + ) +where + +import Control.Lens +import Prelude hiding (FilePath) +import Shelly +import Text.Shakespeare.Text (st) +import VeriFuzz.Sim.Internal +import VeriFuzz.Sim.Template +import VeriFuzz.Verilog.CodeGen +import VeriFuzz.Verilog.Mutate + +newtype Yosys = Yosys { yosysPath :: FilePath } + deriving (Eq, Show) + +instance Tool Yosys where + toText _ = "yosys" + +instance Synthesisor Yosys where + runSynth = runSynthYosys + +defaultYosys :: Yosys +defaultYosys = Yosys "yosys" + +runSynthYosys :: Yosys -> SourceInfo -> FilePath -> Sh () +runSynthYosys sim (SourceInfo _ src) outf = do + dir <- pwd + writefile inpf $ genSource src + echoP "Yosys: synthesis" + _ <- logger dir "yosys" + $ timeout + (yosysPath sim) + ["-b", "verilog -noattr", "-o", out, "-S", inp] + echoP "Yosys: synthesis done" + where + inpf = "rtl.v" + inp = toTextIgnore inpf + out = toTextIgnore outf + +runMaybeSynth :: (Synthesisor a) => Maybe a -> SourceInfo -> Sh () +runMaybeSynth (Just sim) srcInfo = + runSynth sim srcInfo $ fromText [st|syn_#{toText sim}.v|] +runMaybeSynth Nothing (SourceInfo _ src) = + writefile "syn_rtl.v" $ genSource src + +runEquivYosys + :: (Synthesisor a, Synthesisor b) + => Yosys + -> a + -> Maybe b + -> SourceInfo + -> Sh () +runEquivYosys yosys sim1 sim2 srcInfo = do + writefile "top.v" . genSource . initMod . makeTop 2 $ srcInfo ^. mainModule + writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo + runSynth sim1 srcInfo $ fromText [st|syn_#{toText sim1}.v|] + runMaybeSynth sim2 srcInfo + echoP "Yosys: equivalence check" + run_ (yosysPath yosys) [toTextIgnore checkFile] + echoP "Yosys: equivalence done" + where + checkFile = + fromText [st|test.#{toText sim1}.#{maybe "rtl" toText sim2}.ys|] + +runEquiv + :: (Synthesisor a, Synthesisor b) + => Yosys + -> a + -> Maybe b + -> SourceInfo + -> Sh () +runEquiv _ sim1 sim2 srcInfo = do + root <- rootPath + dir <- pwd + echoP "SymbiYosys: setup" + writefile "top.v" + . genSource + . initMod + . makeTopAssert + $ srcInfo + ^. mainModule + writefile "test.sby" $ sbyConfig root sim1 sim2 srcInfo + runSynth sim1 srcInfo $ fromText [st|syn_#{toText sim1}.v|] + runMaybeSynth sim2 srcInfo + echoP "SymbiYosys: run" + _ <- logger dir "symbiyosys" $ run "sby" ["-f", "test.sby"] + echoP "SymbiYosys: done" -- cgit