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/Yosys.hs | 109 -------------------------------------------------- 1 file changed, 109 deletions(-) delete mode 100644 src/VeriFuzz/Yosys.hs (limited to 'src/VeriFuzz/Yosys.hs') diff --git a/src/VeriFuzz/Yosys.hs b/src/VeriFuzz/Yosys.hs deleted file mode 100644 index ef2bc11..0000000 --- a/src/VeriFuzz/Yosys.hs +++ /dev/null @@ -1,109 +0,0 @@ -{-| -Module : VeriFuzz.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.Yosys where - -import Control.Lens -import Prelude hiding (FilePath) -import Shelly -import Text.Shakespeare.Text (st) -import VeriFuzz.AST -import VeriFuzz.CodeGen -import VeriFuzz.Internal -import VeriFuzz.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" - -writeSimFile - :: Yosys -- ^ Simulator instance - -> Verilog -- ^ Current Verilog source - -> FilePath -- ^ Output sim file - -> Sh () -writeSimFile _ src file = do - writefile "rtl.v" $ genSource src - writefile file yosysSimConfig - -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