-
Notifications
You must be signed in to change notification settings - Fork 348
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
testsuite/synth: add a test for #1850
- Loading branch information
Showing
3 changed files
with
82 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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)) | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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" |