diff options
author | Xiretza <xiretza@xiretza.xyz> | 2020-05-14 16:39:19 +0200 |
---|---|---|
committer | tgingold <tgingold@users.noreply.github.com> | 2020-05-14 18:54:32 +0200 |
commit | 94a030e2fa33a7c29ef2c7dab7f88b4a00cfee0b (patch) | |
tree | b45afe2267e7bba961fbaa54f9833aa0e4c3de03 /testsuite/formal/gates/test_pmux.vhd | |
parent | 9984dc1a03316c21b4710b84a32b9fdb8aae1e05 (diff) | |
download | ghdl-yosys-plugin-94a030e2fa33a7c29ef2c7dab7f88b4a00cfee0b.tar.gz ghdl-yosys-plugin-94a030e2fa33a7c29ef2c7dab7f88b4a00cfee0b.tar.bz2 ghdl-yosys-plugin-94a030e2fa33a7c29ef2c7dab7f88b4a00cfee0b.zip |
Add formal test for pmux gate
Diffstat (limited to 'testsuite/formal/gates/test_pmux.vhd')
-rw-r--r-- | testsuite/formal/gates/test_pmux.vhd | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/testsuite/formal/gates/test_pmux.vhd b/testsuite/formal/gates/test_pmux.vhd new file mode 100644 index 0000000..b3901f4 --- /dev/null +++ b/testsuite/formal/gates/test_pmux.vhd @@ -0,0 +1,46 @@ +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + +entity ent is + port ( + clk : in std_logic; + a : in std_logic_vector(1 downto 0); + b : out std_logic_vector(1 downto 0) + ); +end entity; + +architecture a of ent is +begin + process(clk) + begin + if rising_edge(clk) then + case a is + when "00" => + b <= "01"; + when "01" => + b <= "10"; + when "11" => + b <= "00"; + when others => + b <= "11"; + end case; + end if; + end process; + + formal: block + signal has_run : std_logic := '0'; + signal prev_a : std_logic_vector(1 downto 0); + begin + process(clk) + begin + if rising_edge(clk) then + prev_a <= a; + has_run <= '1'; + end if; + end process; + + default clock is rising_edge(clk); + assert always has_run -> unsigned(prev_a) + 1 = unsigned(b); + end block; +end architecture; |