diff options
author | Yann Herklotz <ymherklotz@gmail.com> | 2019-01-20 17:46:05 +0000 |
---|---|---|
committer | Yann Herklotz <ymherklotz@gmail.com> | 2019-01-20 17:46:05 +0000 |
commit | 8a70b3fa892aaa095aa423609bfadaecea44c655 (patch) | |
tree | 0b9200ea197f57b69a3e367681865edd20f8dba6 /src/VeriFuzz | |
parent | 22182aebc734832f64d324f1635b7e9a45bd4d21 (diff) | |
download | verismith-8a70b3fa892aaa095aa423609bfadaecea44c655.tar.gz verismith-8a70b3fa892aaa095aa423609bfadaecea44c655.zip |
[Fix #26] Add support for SymbiYosys
Diffstat (limited to 'src/VeriFuzz')
-rw-r--r-- | src/VeriFuzz/Simulator/Internal/Template.hs | 6 | ||||
-rw-r--r-- | src/VeriFuzz/Simulator/Yosys.hs | 8 |
2 files changed, 10 insertions, 4 deletions
diff --git a/src/VeriFuzz/Simulator/Internal/Template.hs b/src/VeriFuzz/Simulator/Internal/Template.hs index 4b9cc4e..109c679 100644 --- a/src/VeriFuzz/Simulator/Internal/Template.hs +++ b/src/VeriFuzz/Simulator/Internal/Template.hs @@ -65,9 +65,9 @@ smtbmc [script] #{readL} -read syn_#{toText sim1}.v +read -formal syn_#{toText sim1}.v rename #{mi} #{mi}_1 -read syn_#{maybe "rtl" toText sim2}.v +read -formal syn_#{maybe "rtl" toText sim2}.v rename #{mi} #{mi}_2 read -formal top.v prep -top #{mi} @@ -87,4 +87,4 @@ top.v . ((bd </> fromText "data") </>) . fromText <$> deps - readL = T.intercalate "\n" $ mappend "read " <$> deps + readL = T.intercalate "\n" $ mappend "read -formal " <$> deps diff --git a/src/VeriFuzz/Simulator/Yosys.hs b/src/VeriFuzz/Simulator/Yosys.hs index ec5a284..286a132 100644 --- a/src/VeriFuzz/Simulator/Yosys.hs +++ b/src/VeriFuzz/Simulator/Yosys.hs @@ -65,8 +65,14 @@ runEquivYosys yosys sim1 sim2 m = do runSynth sim1 m $ fromText [st|syn_#{toText sim1}.v|] runMaybeSynth sim2 m run_ (yosysPath yosys) [toTextIgnore checkFile] - where checkFile = fromText [st|test.#{toText sim1}.#{maybe "rtl" toText sim2}.ys|] + where + checkFile = fromText [st|test.#{toText sim1}.#{maybe "rtl" toText sim2}.ys|] runEquiv :: (Synthesize a, Synthesize b) => Yosys -> a -> Maybe b -> ModDecl -> Sh () runEquiv yosys sim1 sim2 m = do + root <- rootPath writefile "top.v" . genSource . initMod $ makeTopAssert m + writefile "test.sby" $ sbyConfig root sim1 sim2 m + runSynth sim1 m $ fromText [st|syn_#{toText sim1}.v|] + runMaybeSynth sim2 m + run_ "sby" ["test.sby"] |