synth: extract edge for PSL clocks.

5 files changed, 120 insertions, 29 deletions

diff --git a/src/synth/synth-stmts.adb b/src/synth/synth-stmts.adb
index 4c2c70c9a..7c0039a8c 100644
--- a/src/synth/synth-stmts.adb
+++ b/src/synth/synth-stmts.adb
@@ -48,6 +48,7 @@ with Vhdl.Annotations; use Vhdl.Annotations;
 with Netlists; use Netlists;
 with Netlists.Builders; use Netlists.Builders;
 with Netlists.Gates;
+with Netlists.Utils;
 
 package body Synth.Stmts is
    function Synth_Waveform (Syn_Inst : Synth_Instance_Acc;
@@ -1324,12 +1325,15 @@ package body Synth.Stmts is
       return Res;
    end Synth_Psl_NFA;
 
-   procedure Synth_Psl_Assume_Directive
-     (Syn_Inst : Synth_Instance_Acc; Stmt : Node)
+   function Synth_Psl_Directive
+     (Syn_Inst : Synth_Instance_Acc; Stmt : Node) return Net
    is
+      use Netlists.Utils;
+      use Netlists.Gates;
       Nbr_States : constant Int32 := Get_PSL_Nbr_States (Stmt);
       Init : Net;
       Clk : Net;
+      Clk_Inst : Instance;
       States : Net;
       Next_States : Net;
    begin
@@ -1338,6 +1342,15 @@ package body Synth.Stmts is
       Init := Build_Const_UB32 (Build_Context, 1, Uns32 (Nbr_States));
       Clk := Synth_PSL_Expression (Syn_Inst, Get_PSL_Clock (Stmt));
 
+      --  Check the clock is an edge and extract it.
+      Clk_Inst := Get_Parent (Clk);
+      if Get_Id (Clk_Inst) /= Id_Edge then
+         Error_Msg_Synth (+Stmt, "clock is not an edge");
+         return No_Net;
+      end if;
+
+      Clk := Get_Input_Net (Clk_Inst, 0);
+
       --  build idff
       States := Build_Idff (Build_Context, Clk, No_Net, Init);
 
@@ -1347,43 +1360,37 @@ package body Synth.Stmts is
         Synth_Psl_NFA (Syn_Inst, Get_PSL_NFA (Stmt), Nbr_States, States);
       Connect (Get_Input (Get_Parent (States), 1), Next_States);
 
+      --  The NFA state is correct as long as there is a 1.
+      return Build_Reduce (Build_Context,
+                           Netlists.Gates.Id_Red_Or, Next_States);
+   end Synth_Psl_Directive;
+
+   procedure Synth_Psl_Assume_Directive
+     (Syn_Inst : Synth_Instance_Acc; Stmt : Node)
+   is
+      Res : Net;
+   begin
       --  Build assume gate.
       --  Note: for synthesis, we assume the next state will be correct.
       --  (If we assume on States, then the first cycle is ignored).
-      Build_Assume (Build_Context,
-                    Build_Reduce (Build_Context,
-                                  Netlists.Gates.Id_Red_Or, Next_States));
+      Res := Synth_Psl_Directive (Syn_Inst, Stmt);
+      if Res /= No_Net then
+         Build_Assume (Build_Context, Res);
+      end if;
    end Synth_Psl_Assume_Directive;
 
    procedure Synth_Psl_Assert_Directive
      (Syn_Inst : Synth_Instance_Acc; Stmt : Node)
    is
-      Nbr_States : constant Int32 := Get_PSL_Nbr_States (Stmt);
-      Init : Net;
-      Clk : Net;
-      States : Net;
-      Next_States : Net;
+      Res : Net;
    begin
-      --  create init net, clock net
-      pragma Assert (Nbr_States <= 32);
-      Init := Build_Const_UB32 (Build_Context, 1, Uns32 (Nbr_States));
-      Clk := Synth_PSL_Expression (Syn_Inst, Get_PSL_Clock (Stmt));
-
-      --  build idff
-      States := Build_Idff (Build_Context, Clk, No_Net, Init);
-
-      --  create update nets
-      --  For each state: if set, evaluate all outgoing edges.
-      Next_States :=
-        Synth_Psl_NFA (Syn_Inst, Get_PSL_NFA (Stmt), Nbr_States, States);
-      Connect (Get_Input (Get_Parent (States), 1), Next_States);
-
       --  Build assert gate.
       --  Note: for synthesis, we assume the next state will be correct.
       --  (If we assert on States, then the first cycle is ignored).
-      Build_Assert (Build_Context,
-                    Build_Reduce (Build_Context,
-                                  Netlists.Gates.Id_Red_Or, Next_States));
+      Res := Synth_Psl_Directive (Syn_Inst, Stmt);
+      if Res /= No_Net then
+         Build_Assert (Build_Context, Res);
+      end if;
    end Synth_Psl_Assert_Directive;
 
    procedure Synth_Generate_Statement_Body (Syn_Inst : Synth_Instance_Acc;
diff --git a/testsuite/synth/psl01/assert1.vhdl b/testsuite/synth/psl01/assert1.vhdl
new file mode 100644
index 000000000..13e44a1e8
--- /dev/null
+++ b/testsuite/synth/psl01/assert1.vhdl
@@ -0,0 +1,27 @@
+library ieee;
+use ieee.std_logic_1164.all;
+use ieee.numeric_std.all;
+
+entity assert1 is
+ port (clk, rst: std_logic;
+       cnt : out unsigned(3 downto 0));
+end assert1;
+
+architecture behav of assert1 is
+ signal val : unsigned (3 downto 0);
+begin
+ process(clk)
+ begin
+   if rising_edge(clk) then
+     if rst = '1' then
+       val <= (others => '0');
+     else
+       val <= val + 1;
+     end if;
+   end if;
+ end process;
+ cnt <= val;
+
+ --psl default clock is rising_edge(clk);
+ --psl assert always val /= 5 or rst = '1';
+end behav;
diff --git a/testsuite/synth/psl01/assume1.vhdl b/testsuite/synth/psl01/assume1.vhdl
new file mode 100644
index 000000000..0bc54c56f
--- /dev/null
+++ b/testsuite/synth/psl01/assume1.vhdl
@@ -0,0 +1,27 @@
+library ieee;
+use ieee.std_logic_1164.all;
+use ieee.numeric_std.all;
+
+entity assume1 is
+ port (clk, rst: std_logic;
+       cnt : out unsigned(3 downto 0));
+end assume1;
+
+architecture behav of assume1 is
+ signal val : unsigned (3 downto 0);
+begin
+ process(clk)
+ begin
+   if rising_edge(clk) then
+     if rst = '1' then
+       val <= (others => '0');
+     else
+       val <= val + 1;
+     end if;
+   end if;
+ end process;
+ cnt <= val;
+
+ --psl default clock is rising_edge(clk);
+ --psl assume always val < 50;
+end behav;
diff --git a/testsuite/synth/psl01/restrict1.vhdl b/testsuite/synth/psl01/restrict1.vhdl
new file mode 100644
index 000000000..b932acc9a
--- /dev/null
+++ b/testsuite/synth/psl01/restrict1.vhdl
@@ -0,0 +1,27 @@
+library ieee;
+use ieee.std_logic_1164.all;
+use ieee.numeric_std.all;
+
+entity restrict1 is
+ port (clk, rst: std_logic;
+       cnt : out unsigned(3 downto 0));
+end restrict1;
+
+architecture behav of restrict1 is
+ signal val : unsigned (3 downto 0);
+begin
+ process(clk)
+ begin
+   if rising_edge(clk) then
+     if rst = '1' then
+       val <= (others => '0');
+     else
+       val <= val + 1;
+     end if;
+   end if;
+ end process;
+ cnt <= val;
+
+ --psl default clock is rising_edge (clk);
+ --psl restrict {rst; (not rst)[*]};
+end behav;
diff --git a/testsuite/synth/psl01/testsuite.sh b/testsuite/synth/psl01/testsuite.sh
index e6d4050e6..4c43382b6 100755
--- a/testsuite/synth/psl01/testsuite.sh
+++ b/testsuite/synth/psl01/testsuite.sh
@@ -3,8 +3,11 @@
 . ../../testenv.sh
 
 GHDL_STD_FLAGS=--std=08
-synth -fpsl hello.vhdl -e hello > syn_hello.vhdl
-analyze syn_hello.vhdl
+
+for f in restrict1 assume1 assert1; do
+  synth -fpsl $f.vhdl -e $f > syn_$f.vhdl
+  analyze syn_$f.vhdl
+done
 clean
 
 echo "Test successful"