diff options
author | Yann Herklotz <ymherklotz@gmail.com> | 2019-01-19 23:12:25 +0000 |
---|---|---|
committer | Yann Herklotz <ymherklotz@gmail.com> | 2019-01-19 23:12:25 +0000 |
commit | 64a0ae3600073f486462b1d056409954634b0084 (patch) | |
tree | a2315f2f075a2c91b88b0cb3bfaa581d702e2e48 /src/VeriFuzz/Simulator/Yosys.hs | |
parent | 771ff2ccb2f07f5c60d4af260d236ee148de667f (diff) | |
download | verismith-64a0ae3600073f486462b1d056409954634b0084.tar.gz verismith-64a0ae3600073f486462b1d056409954634b0084.zip |
Reformat with stylish-haskell
Diffstat (limited to 'src/VeriFuzz/Simulator/Yosys.hs')
-rw-r--r-- | src/VeriFuzz/Simulator/Yosys.hs | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/src/VeriFuzz/Simulator/Yosys.hs b/src/VeriFuzz/Simulator/Yosys.hs index 028fbb2..8f40ea9 100644 --- a/src/VeriFuzz/Simulator/Yosys.hs +++ b/src/VeriFuzz/Simulator/Yosys.hs @@ -15,10 +15,10 @@ Yosys simulator implementation. module VeriFuzz.Simulator.Yosys where import Control.Lens -import Data.Text ( Text ) -import Prelude hiding ( FilePath ) +import Data.Text (Text) +import Prelude hiding (FilePath) import Shelly -import Text.Shakespeare.Text ( st ) +import Text.Shakespeare.Text (st) import VeriFuzz.Simulator.General import VeriFuzz.Verilog @@ -71,12 +71,10 @@ sat -timeout 20 -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 #{modName} modName = m ^. moduleId . getIdentifier -- ids = T.intercalate "," $ allVars m ^.. traverse . getIdentifier --- brittany-disable-next-binding runOtherSynth :: (Synthesize a) => Maybe a -> ModDecl -> Sh () runOtherSynth (Just sim) m = runSynth sim m $ fromText [st|syn_#{toText sim}.v|] -runOtherSynth Nothing m = writefile "syn_rtl.v" $ genSource m +runOtherSynth Nothing m = writefile "syn_rtl.v" $ genSource m --- brittany-disable-next-binding runEquiv :: (Synthesize a, Synthesize b) => Yosys -> a -> Maybe b -> ModDecl -> Sh () runEquiv yosys sim1 sim2 m = do writefile "top.v" . genSource . initMod $ makeTop 2 m @@ -84,5 +82,9 @@ runEquiv yosys sim1 sim2 m = do runSynth sim1 m $ fromText [st|syn_#{toText sim1}.v|] runOtherSynth sim2 m run_ (yosysPath yosys) [checkFile] - where - checkFile = [st|test.#{toText sim1}.#{maybe "rtl" toText sim2}.ys|] + where checkFile = [st|test.#{toText sim1}.#{maybe "rtl" toText sim2}.ys|] + +-- | Generate @.il@ files for Yosys equivalence checking using the SAT solver. +genIl :: (Synthesize a) => Yosys -> a -> ModDecl -> Sh () +genIl yosys sim m = do + return |