testsuite/synth: add a test for #1850

3 files changed, 82 insertions, 0 deletions

diff --git a/testsuite/synth/issue1850/detector.psl b/testsuite/synth/issue1850/detector.psl
new file mode 100644
index 000000000..656c2d659
--- /dev/null
+++ b/testsuite/synth/issue1850/detector.psl
@@ -0,0 +1,31 @@
+vunit i_rising_pulse_detector(rising_pulse_detector(rising_pulse_detector_1))
+{
+
+    default clock is rising_edge(clk);
+
+    -- reset is true at beginning
+    f_reset_initial : assume {rst};
+    -- no reset after begining
+    f_reset_disable : assume always {not rst} |=> {not rst};
+
+
+    --working cover without generate
+    fc_output_4 : cover {output_pulse(4) = '1'};
+
+    -- generate cover pulse
+    g1: for I in 0 to 15 generate
+        cover {output_pulse(I) = '1'};
+    end generate;
+
+    --working bmc witout generate:
+    f_ouptut_7 : assert always {(not rst) and output_pulse(7) = '1'}
+        |=> {output_pulse(7) = '0'};
+
+    -- generate pulse one cycle assertion
+    g2: for J in 0 to 15 generate
+        assert always {(not rst) and output_pulse(J) = '1'} |=> {output_pulse(J) = '0'};
+    end generate;
+
+
+} -- vunit i_rising_pulse_detector(rising_pulse_detector(rising_pulse_detector_1))
+
diff --git a/testsuite/synth/issue1850/pulse.vhdl b/testsuite/synth/issue1850/pulse.vhdl
new file mode 100644
index 000000000..97f4dd893
--- /dev/null
+++ b/testsuite/synth/issue1850/pulse.vhdl
@@ -0,0 +1,43 @@
+-- Created on    : 11/08/2021
+-- Author        : Fabien Marteau <fabien.marteau@armadeus.com>
+-- Copyright (c) ARMadeus systems 2015
+
+library IEEE;
+use IEEE.STD_LOGIC_1164.ALL;
+use IEEE.numeric_std.all;
+
+
+Entity rising_pulse_detector is
+generic( WAITPRETRIGG_CNT: natural := 1000);
+port
+(
+    clk : in std_logic;
+    rst : in std_logic;
+
+    inputvec : in std_logic_vector(15 downto 0);
+
+    output_pulse : out std_logic_vector(15 downto 0)
+
+);
+end entity;
+
+Architecture rising_pulse_detector_1 of rising_pulse_detector is
+
+    signal inputvec_old, inputvec_pulse : std_logic_vector(15 downto 0);
+
+begin
+
+    output_pulse <= inputvec_pulse;
+
+    process(clk, rst)
+    begin
+        if(rst = '1') then
+            inputvec_old <= (others => '0');
+            inputvec_pulse <= (others => '0');
+        elsif(rising_edge(clk)) then
+            inputvec_pulse <= (not inputvec_old) and inputvec;
+            inputvec_old <= inputvec;
+        end if;
+    end process;
+
+end architecture rising_pulse_detector_1;
diff --git a/testsuite/synth/issue1850/testsuite.sh b/testsuite/synth/issue1850/testsuite.sh
new file mode 100755
index 000000000..81eec2fc2
--- /dev/null
+++ b/testsuite/synth/issue1850/testsuite.sh
@@ -0,0 +1,8 @@
+#! /bin/sh
+
+. ../../testenv.sh
+
+GHDL_STD_FLAGS=--std=08
+synth pulse.vhdl detector.psl -e > syn_pulse.vhdl
+
+echo "Test successful"