From 01c2ab3f6a58d416528efce3057e2cf2f1604489 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 29 Oct 2019 11:53:43 +0000
Subject: Add data-file installation path

This removes the need to recursively copy the data directory which will also
save on space.
---
 src/Verismith/Tool/Icarus.hs   | 11 +++++++----
 src/Verismith/Tool/Template.hs | 22 ++++++++++++----------
 src/Verismith/Tool/Yosys.hs    |  6 +++---
 3 files changed, 22 insertions(+), 17 deletions(-)

(limited to 'src/Verismith/Tool')

diff --git a/src/Verismith/Tool/Icarus.hs b/src/Verismith/Tool/Icarus.hs
index b783033..9d4281f 100644
--- a/src/Verismith/Tool/Icarus.hs
+++ b/src/Verismith/Tool/Icarus.hs
@@ -133,15 +133,16 @@ fromBytes = B.foldl' f 0 where f a b = a `shiftL` 8 .|. fromIntegral b
 
 runSimIc
     :: (Synthesiser b)
-    => Icarus
+    => FilePath
+    -> Icarus
     -> b
     -> SourceInfo
     -> [ByteString]
     -> ResultSh ByteString
-runSimIc sim1 synth1 srcInfo bss = do
+runSimIc datadir sim1 synth1 srcInfo bss = do
     dir <- liftSh pwd
     let top      = srcInfo ^. mainModule
-    let inConcat = (RegConcat (Id . fromPort <$> (top ^. modInPorts)))
+    let inConcat = (RegConcat . filter filterClk $ (Id . fromPort <$> (top ^. modInPorts)))
     let
         tb = instantiateMod top $ ModDecl
             "testbench"
@@ -170,7 +171,7 @@ runSimIc sim1 synth1 srcInfo bss = do
             ]
             []
 
-    liftSh . writefile "testbench.v" $ icarusTestbench (Verilog [tb]) synth1
+    liftSh . writefile "testbench.v" $ icarusTestbench datadir (Verilog [tb]) synth1
     liftSh $ exe dir "icarus" "iverilog" ["-o", "main", "testbench.v"]
     liftSh
         $   B.take 8
@@ -186,3 +187,5 @@ runSimIc sim1 synth1 srcInfo bss = do
                 )
   where
     exe dir name e = void . errExit False . logCommand dir name . timeout e
+    filterClk (Id "clk") = False
+    filterClk (Id _)     = True
diff --git a/src/Verismith/Tool/Template.hs b/src/Verismith/Tool/Template.hs
index c0cbfe1..d02daf8 100644
--- a/src/Verismith/Tool/Template.hs
+++ b/src/Verismith/Tool/Template.hs
@@ -89,8 +89,8 @@ write_verilog -force #{outf}
 |]
 
 -- brittany-disable-next-binding
-sbyConfig :: (Synthesiser a, Synthesiser b) => a -> b -> SourceInfo -> Text
-sbyConfig sim1 sim2 (SourceInfo top _) = [st|[options]
+sbyConfig :: (Synthesiser a, Synthesiser b) => FilePath -> a -> b -> SourceInfo -> Text
+sbyConfig datadir sim1 sim2 (SourceInfo top _) = [st|[options]
 multiclock on
 mode prove
 
@@ -115,19 +115,21 @@ top.v
     depList =
       T.intercalate "\n"
         $   toTextIgnore
-        .   (fromText "data" </>)
+        .   (datadir </> fromText "data" </>)
         .   fromText
         <$> deps
     readL = T.intercalate "\n" $ mappend "read -formal " <$> deps
 
-icarusTestbench :: (Synthesiser a) => Verilog -> a -> Text
-icarusTestbench t synth1 = [st|
-`include "data/cells_cmos.v"
-`include "data/cells_cyclone_v.v"
-`include "data/cells_verific.v"
-`include "data/cells_xilinx_7.v"
-`include "data/cells_yosys.v"
+icarusTestbench :: (Synthesiser a) => FilePath -> Verilog -> a -> Text
+icarusTestbench datadir t synth1 = [st|
+`include "#{ddir}/data/cells_cmos.v"
+`include "#{ddir}/data/cells_cyclone_v.v"
+`include "#{ddir}/data/cells_verific.v"
+`include "#{ddir}/data/cells_xilinx_7.v"
+`include "#{ddir}/data/cells_yosys.v"
 `include "#{toTextIgnore $ synthOutput synth1}"
 
 #{genSource t}
 |]
+  where
+    ddir = toTextIgnore datadir
diff --git a/src/Verismith/Tool/Yosys.hs b/src/Verismith/Tool/Yosys.hs
index 9c0a864..afbffe9 100644
--- a/src/Verismith/Tool/Yosys.hs
+++ b/src/Verismith/Tool/Yosys.hs
@@ -102,8 +102,8 @@ runEquivYosys yosys sim1 sim2 srcInfo = do
     where checkFile = fromText [st|test.#{toText sim1}.#{toText sim2}.ys|]
 
 runEquiv
-    :: (Synthesiser a, Synthesiser b) => a -> b -> SourceInfo -> ResultSh ()
-runEquiv sim1 sim2 srcInfo = do
+    :: (Synthesiser a, Synthesiser b) => FilePath -> a -> b -> SourceInfo -> ResultSh ()
+runEquiv datadir sim1 sim2 srcInfo = do
     dir <- liftSh pwd
     liftSh $ do
         writefile "top.v"
@@ -114,7 +114,7 @@ runEquiv sim1 sim2 srcInfo = do
             ^. mainModule
         replaceMods (synthOutput sim1) "_1" srcInfo
         replaceMods (synthOutput sim2) "_2" srcInfo
-        writefile "proof.sby" $ sbyConfig sim1 sim2 srcInfo
+        writefile "proof.sby" $ sbyConfig datadir sim1 sim2 srcInfo
     e <- liftSh $ do
         exe dir "symbiyosys" "sby" ["-f", "proof.sby"]
         lastExitCode
-- 
cgit