diff options
Diffstat (limited to 'src/VeriFuzz/Sim/Yosys.hs')
| -rw-r--r-- | src/VeriFuzz/Sim/Yosys.hs | 26 |
1 files changed, 10 insertions, 16 deletions
diff --git a/src/VeriFuzz/Sim/Yosys.hs b/src/VeriFuzz/Sim/Yosys.hs index c432afe..07125df 100644 --- a/src/VeriFuzz/Sim/Yosys.hs +++ b/src/VeriFuzz/Sim/Yosys.hs @@ -75,16 +75,11 @@ runSynthYosys sim (SourceInfo _ src) = (<?> SynthFail) . liftSh $ do inp = toTextIgnore inpf out = toTextIgnore $ synthOutput sim -runMaybeSynth :: (Synthesiser a) => Maybe a -> SourceInfo -> ResultSh () -runMaybeSynth (Just sim) srcInfo = runSynth sim srcInfo -runMaybeSynth Nothing (SourceInfo _ src) = - liftSh . writefile "rtl.v" $ genSource src - runEquivYosys :: (Synthesiser a, Synthesiser b) => Yosys -> a - -> Maybe b + -> b -> SourceInfo -> ResultSh () runEquivYosys yosys sim1 sim2 srcInfo = do @@ -97,21 +92,20 @@ runEquivYosys yosys sim1 sim2 srcInfo = do ^. mainModule writefile checkFile $ yosysSatConfig sim1 sim2 srcInfo runSynth sim1 srcInfo - runMaybeSynth sim2 srcInfo + runSynth sim2 srcInfo liftSh $ do logger "Yosys: equivalence check" run_ (yosysPath yosys) [toTextIgnore checkFile] logger "Yosys: equivalence done" where checkFile = - fromText [st|test.#{toText sim1}.#{maybe "rtl" toText sim2}.ys|] + fromText [st|test.#{toText sim1}.#{toText sim2}.ys|] -runEquiv - :: (Synthesiser a, Synthesiser b) - => a - -> Maybe b - -> SourceInfo - -> ResultSh () +runEquiv :: (Synthesiser a, Synthesiser b) + => a + -> b + -> SourceInfo + -> ResultSh () runEquiv sim1 sim2 srcInfo = do dir <- liftSh pwd liftSh $ do @@ -121,8 +115,8 @@ runEquiv sim1 sim2 srcInfo = do . makeTopAssert $ srcInfo ^. mainModule - replaceMods (synthOutput sim1) "_1" srcInfo - replaceMods (maybe "rtl.v" synthOutput sim2) "_2" srcInfo + replaceMods (synthOutput sim1) "_1" srcInfo + replaceMods (synthOutput sim2) "_2" srcInfo writefile "proof.sby" $ sbyConfig sim1 sim2 srcInfo liftSh $ logger "Running SymbiYosys" execute_ EquivFail dir "symbiyosys" "sby" ["proof.sby"] |