From d823739fbc59db7fd7361eb6596527bae9152064 Mon Sep 17 00:00:00 2001
From: Joppe Blondel <joppe@blondel.nl>
Date: Tue, 6 Sep 2022 13:09:50 +0200
Subject: [PATCH] Added symbiyosys to toolchains

Signed-off-by: Joppe Blondel <joppe@blondel.nl>
---
 examples/formal/RTL/counter.vhd    | 15 ++++++-
 examples/formal/SIM/counter.sby    | 22 ++++++++++
 examples/formal/project.cfg        | 13 ++++++
 remotesyn/toolchains/symbiyosys.py | 66 ++++++++++++++++++++++++++++++
 4 files changed, 114 insertions(+), 2 deletions(-)
 create mode 100644 examples/formal/SIM/counter.sby
 create mode 100644 remotesyn/toolchains/symbiyosys.py

diff --git a/examples/formal/RTL/counter.vhd b/examples/formal/RTL/counter.vhd
index e4abd58..a643bef 100644
--- a/examples/formal/RTL/counter.vhd
+++ b/examples/formal/RTL/counter.vhd
@@ -24,12 +24,23 @@ begin
 
     cnt <= std_logic_vector(icnt);
 
-    process(ACLK, ARESETN)
+    f_counter : if formal generate
+    begin
+        -- Set clock source for all assertions
+        default clock is rising_edge(ACLK);
+        -- Counter is always under mxcnt if it started under max
+        a_never_exceeds_max : assert (always (icnt<mxcnt) -> always (icnt<mxcnt));
+        -- Counter is always reset to 0
+        a_counter_reset_to_zero : assert (always (ARESETN='0') -> (icnt=0));
+    end generate;
+
+    p_counter : process(ACLK, ARESETN)
     begin
         if ARESETN='0' then
             icnt <= (others=>'0');
         elsif rising_edge(ACLK) then
-            if icnt<mxcnt then
+            -- Without this -1 the assertion wont hold
+            if icnt<mxcnt-1 then
                 icnt <= icnt + 1;
             else 
                 icnt <= (others=>'0');
diff --git a/examples/formal/SIM/counter.sby b/examples/formal/SIM/counter.sby
new file mode 100644
index 0000000..5d4c6c4
--- /dev/null
+++ b/examples/formal/SIM/counter.sby
@@ -0,0 +1,22 @@
+[tasks]
+bmc d_12
+cover d_120
+prove d_4
+
+[options]
+bmc:mode bmc
+cover:mode cover
+prove:mode prove
+d_120:depth 120
+d_12:depth 12
+d_4:depth 4
+
+[engines]
+smtbmc
+
+[script]
+ghdl -fpsl --std=08 -gformal=true counter.vhd -e counter
+prep -top counter
+
+[files]
+RTL/counter.vhd
\ No newline at end of file
diff --git a/examples/formal/project.cfg b/examples/formal/project.cfg
index 5bae63c..d938f8b 100644
--- a/examples/formal/project.cfg
+++ b/examples/formal/project.cfg
@@ -25,4 +25,17 @@ runtime             = all
 # Fileset
 files_vhdl          = RTL/counter.vhd 
                       SIM/tb_counter.vhd
+# ######################################
+
+# ######################################
+# Formal verification with symbiyosys
+[target.formal]
+toolchain           = symbiyosys
+
+# Toolchain settings
+sby_opts            =
+
+# Fileset
+files_sby           = SIM/counter.sby
+files_other         = RTL/counter.vhd 
 # ######################################
\ No newline at end of file
diff --git a/remotesyn/toolchains/symbiyosys.py b/remotesyn/toolchains/symbiyosys.py
new file mode 100644
index 0000000..e80a156
--- /dev/null
+++ b/remotesyn/toolchains/symbiyosys.py
@@ -0,0 +1,66 @@
+import shutil
+import os
+import time
+import subprocess
+
+def execp(cmd, subprocesses, cwd):
+    p = subprocess.Popen(cmd, 
+        shell=True, cwd=cwd, 
+        stdin=subprocess.DEVNULL, stdout=subprocess.DEVNULL, stderr=subprocess.DEVNULL)
+    subprocesses.append(p)
+    while p.poll() is None:
+        time.sleep(1)
+    res = p.returncode
+    return res
+
+def do(config, target, log, subprocesses, prefix='.'):
+    shutil.rmtree(config.get('project', 'build_dir', fallback='build'), True)
+
+    log("Starting formal verification")
+    
+    log(" - parsing options")
+    toplevel = config.get(f'target.{target}', 'toplevel', fallback='toplevel')
+    runtime = config.get(f'target.{target}', 'runtime', fallback='100 ns')
+    sby_opts = config.get(f'target.{target}', 'sby_opts', fallback='')
+    files_sby = config.get(f'target.{target}', 'files_sby', fallback='').split()
+    files_other = config.get(f'target.{target}', 'files_other', fallback='').split()
+    build_dir = config.get(f'project', 'build_dir', fallback='build')
+    out_dir = config.get(f'project', 'out_dir', fallback='out')
+
+    prefix = f'{os.getcwd()}/{prefix}'
+    build_dir = f'{prefix}/{build_dir}'
+    out_dir = f'{prefix}/{out_dir}/{target}'
+
+    log(" - creating output directories")
+    os.makedirs(build_dir, exist_ok=True)
+    os.makedirs(out_dir, exist_ok=True)
+
+    log(" - copy needed files")
+    for f in files_other:
+        d = os.path.dirname(f)
+        os.makedirs(f"{build_dir}/{d}", exist_ok=True)
+        shutil.copy(f"{prefix}/{f}", f"{build_dir}/{f}")
+
+    res = 0
+    for f in files_sby:
+        log(" - running sby for", f)
+        d = os.path.dirname(f)
+        os.makedirs(f"{build_dir}/{d}", exist_ok=True)
+        shutil.copy(f"{prefix}/{f}", f"{build_dir}/{f}")
+
+        res = execp(f"sby --prefix sby_{os.path.basename(f)} --yosys \"yosys -m ghdl\" {sby_opts} -f {f}", subprocesses, build_dir)
+
+        log(" - copy logs and output files")
+        oname = f'sby_{os.path.basename(f)}'
+        for d in os.listdir(f'{build_dir}'):
+            if os.path.isdir(f'{build_dir}/{d}') and d.startswith(oname):
+                shutil.copy(f'{build_dir}/{d}/logfile.txt', f'{out_dir}/{d}.log')
+                shutil.copytree(f'{build_dir}/{d}/engine_0', f'{out_dir}/{d}', dirs_exist_ok=True)
+
+        if res!=0:
+            log(" - [-]")
+        else:
+            log(" - [+]")
+
+    
+    return 0
\ No newline at end of file