diff options
author | Yann Herklotz <ymherklotz@gmail.com> | 2019-01-20 15:33:13 +0000 |
---|---|---|
committer | Yann Herklotz <ymherklotz@gmail.com> | 2019-01-20 15:33:17 +0000 |
commit | 99fe59abc997ba6f65896a2377881409e257faf9 (patch) | |
tree | b83a36efac0fd0fcdd3838f3321428d6bd2de6e3 /src/VeriFuzz/Simulator/Yosys.hs | |
parent | 64a0ae3600073f486462b1d056409954634b0084 (diff) | |
download | verismith-99fe59abc997ba6f65896a2377881409e257faf9.tar.gz verismith-99fe59abc997ba6f65896a2377881409e257faf9.zip |
Rename moduleId to modId
Diffstat (limited to 'src/VeriFuzz/Simulator/Yosys.hs')
-rw-r--r-- | src/VeriFuzz/Simulator/Yosys.hs | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/src/VeriFuzz/Simulator/Yosys.hs b/src/VeriFuzz/Simulator/Yosys.hs index 8f40ea9..90c40bf 100644 --- a/src/VeriFuzz/Simulator/Yosys.hs +++ b/src/VeriFuzz/Simulator/Yosys.hs @@ -14,8 +14,9 @@ Yosys simulator implementation. module VeriFuzz.Simulator.Yosys where -import Control.Lens +import Data.Maybe (fromMaybe) import Data.Text (Text) +import qualified Data.Text as T import Prelude hiding (FilePath) import Shelly import Text.Shakespeare.Text (st) @@ -54,21 +55,20 @@ runSynthYosys sim m outf = do out = toTextIgnore outf -- brittany-disable-next-binding -writeSatFile :: (Synthesize a, Synthesize b) => Text -> a -> Maybe b -> ModDecl -> Sh () +writeSatFile :: (Synthesize a, Synthesize b) => FilePath -> a -> Maybe b -> ModDecl -> Sh () writeSatFile checkFile sim1 sim2 m = - writefile (fromText checkFile) [st|read_verilog syn_#{toText sim1}.v -rename #{modName} #{modName}_1 -read_verilog syn_#{idSim2}.v -rename #{modName} #{modName}_2 + writefile checkFile [st|read_ilang syn_#{toText sim1}.il +rename #{modName m} #{modName m}_1 +read_ilang syn_#{idSim2}.il +rename #{modName m} #{modName m}_2 read_verilog top.v proc; opt_clean -flatten #{modName} +flatten #{modName m} ! touch test.#{toText sim1}.#{idSim2}.input_ok -sat -timeout 20 -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 #{modName} +sat -timeout 20 -show-all -verify-no-timeout -ignore_div_by_zero -prove y_1 y_2 #{modName m} |] where idSim2 = maybe "rtl" toText sim2 - modName = m ^. moduleId . getIdentifier -- ids = T.intercalate "," $ allVars m ^.. traverse . getIdentifier runOtherSynth :: (Synthesize a) => Maybe a -> ModDecl -> Sh () |