From 195765a2aa640ba46ea9989e10e204d2b5de637e Mon Sep 17 00:00:00 2001
From: tmeissner <programming@goodcleanfun.de>
Date: Sun, 22 Sep 2019 23:10:40 +0200
Subject: [PATCH] Adapt to use GHDL as plugin for Yosys VHDL synthesis

---
 vai_reg/Makefile       |  4 ++--
 vai_reg/symbiyosys.sby | 12 +++---------
 vai_reg/vai_reg.vhd    |  6 ++++++
 3 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/vai_reg/Makefile b/vai_reg/Makefile
index 8d2a410..3b6e7ca 100644
--- a/vai_reg/Makefile
+++ b/vai_reg/Makefile
@@ -1,5 +1,5 @@
-vai_reg: vai_reg.vhd properties.sv symbiyosys.sby
-	sby -f -d work symbiyosys.sby
+vai_reg: vai_reg.vhd symbiyosys.sby
+	sby --yosys "yosys -m ghdl" -f -d work symbiyosys.sby
 
 
 clean:
diff --git a/vai_reg/symbiyosys.sby b/vai_reg/symbiyosys.sby
index 2ce4a7c..fa2c454 100644
--- a/vai_reg/symbiyosys.sby
+++ b/vai_reg/symbiyosys.sby
@@ -1,19 +1,13 @@
 [options]
 depth 30
-wait on
-mode prove
-#mode bmc
+mode bmc
 
 [engines]
-smtbmc
-abc pdr
+smtbmc z3
 
 [script]
-verific -vhdl vai_reg.vhd
-verific -formal properties.sv
-verific -import -extnets -all vai_reg
+ghdl --std=08 -fpsl vai_reg.vhd -e vai_reg
 prep -top vai_reg
 
 [files]
 vai_reg.vhd
-properties.sv
diff --git a/vai_reg/vai_reg.vhd b/vai_reg/vai_reg.vhd
index 16a499b..86cebae 100644
--- a/vai_reg/vai_reg.vhd
+++ b/vai_reg/vai_reg.vhd
@@ -159,5 +159,11 @@ begin
   end process;
 
 
+  -- psl default clock is rising_edge(Clk_i);
+
+  -- psl restrict {Reset_n_i = '0'[*5]; Reset_n_i = '1'[+]}[*1];
+  -- psl assert always unsigned(a_addr) < 8;
+
+
 end architecture rtl;