Adapt to use GHDL as plugin for Yosys VHDL synthesis

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:

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

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;