From 240a3c65df7f7f3914c3d963acbf23b80694fd5a Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Tue, 19 Sep 2017 16:52:10 +0200 Subject: Fixes CNE_01200, adds CNE_01200 test. ... which somehow fails. --- data/property/CNE_01200.pro | 9 ++- data/test/CNE_01200/CNE_01200.pp | 1 + data/test/CNE_01200/invalid.vhd | 88 ++++++++++++++++++++++ data/test/CNE_01200/valid.vhd | 157 +++++++++++++++++++++++++++++++++++++++ 4 files changed, 253 insertions(+), 2 deletions(-) create mode 100644 data/test/CNE_01200/CNE_01200.pp create mode 100644 data/test/CNE_01200/invalid.vhd create mode 100644 data/test/CNE_01200/valid.vhd diff --git a/data/property/CNE_01200.pro b/data/property/CNE_01200.pro index 6649103..b738cf8 100644 --- a/data/property/CNE_01200.pro +++ b/data/property/CNE_01200.pro @@ -2,8 +2,13 @@ ( (ps process CNE_01200_BAD_NAME) ) - (implies + (and (is_explicit_process ps) - (string_matches [label ps] "P_.*") + (not + (and + (has_label ps) + (string_matches [label ps] "^P_.*") + ) + ) ) ) diff --git a/data/test/CNE_01200/CNE_01200.pp b/data/test/CNE_01200/CNE_01200.pp new file mode 100644 index 0000000..46d6c1e --- /dev/null +++ b/data/test/CNE_01200/CNE_01200.pp @@ -0,0 +1 @@ +($ps.LINE$) diff --git a/data/test/CNE_01200/invalid.vhd b/data/test/CNE_01200/invalid.vhd new file mode 100644 index 0000000..74c2244 --- /dev/null +++ b/data/test/CNE_01200/invalid.vhd @@ -0,0 +1,88 @@ +library IEEE; + +use IEEE.std_logic_1164.all; + +entity invalid is + port + ( + ip0, ip1, ip2, ip3: in std_logic; + op0, op1, op2, op3: out std_logic + ); +end; + +architecture RTL of invalid is + type enum_t is (V0, V1, V2, V3); + signal s0, s1, s2, s3: std_logic; + signal st0: enum_t; + signal n0, n1, n2, n3: natural range 0 to 3; +begin + P_s: process (s0, s1) + begin + case s1 is + when '0' => + op0 <= s0; + when others => + op0 <= s1; + end case; + end process; + + P_P_P_E: process (s0, s1) -- $SOL:1:0$ + begin + case s1 is + when '0' => + op0 <= s0; + op1 <= (s0 or s1); + when others => + op1 <= (s1 or '0'); + Nope: op0 <= s1; + end case; + end process; + + P_P: process (s0, s1) + begin + op2 <= '0'; + P_PP: + case s1 is + when '0' => + op0 <= s0; + op1 <= (s0 or s1); + when others => + op1 <= (s1 or '0'); + op0 <= s1; + op2 <= '1'; + end case; + end process; + + What: with ip0 select + s1 <= + ip1 when '0', + ip2 when '1', + ip3 when others; + + with st0 select + s2 <= + ip1 when V0, + ip2 when V1, + ip3 when V2, + s1 when V3; + + P_but_maybe_still: with st0 select + s2 <= + ip1 when V0, + ip2 when V1, + ip3 when others; + + P_oops: process (s0, s1, s2, s3) + begin + case st0 is + when V3 => + Cheese: op0 <= s0; + when V2 => + May: op0 <= s1; + when V1 => + Be: op0 <= s2; + when V0 => + Available: op0 <= s3; + end case; + end process; +end; diff --git a/data/test/CNE_01200/valid.vhd b/data/test/CNE_01200/valid.vhd new file mode 100644 index 0000000..ccb9947 --- /dev/null +++ b/data/test/CNE_01200/valid.vhd @@ -0,0 +1,157 @@ +library IEEE; + +use IEEE.std_logic_1164.all; + +entity valid is + port + ( + ip0, ip1, ip2, ip3: in std_logic; + op0, op1, op2, op3: out std_logic + ); +end; + +architecture RTL of valid is + type enum_t is (V0, V1, V2, V3); + signal s0, s1, s2, s3: std_logic; + signal st0: enum_t; + signal n0, n1, n2, n3: natural range 0 to 3; +begin + process (s0, s1) -- $SOL:0:0$ + begin + case s1 is + when '0' => + op0 <= s0; + when others => + op0 <= s1; + end case; + end process; + + process (s0, s1) -- $SOL:1:0$ + begin + case s1 is + when '0' => + op0 <= s0; + op1 <= (s0 or s1); + when others => + op1 <= (s1 or '0'); + op0 <= s1; + end case; + end process; + + process (s0, s1) -- $SOL:2:0$ + begin + op2 <= '0'; + case s1 is + when '0' => + op0 <= s0; + op1 <= (s0 or s1); + when others => + op1 <= (s1 or '0'); + op0 <= s1; + op2 <= '1'; + end case; + end process; + + process (s0, s1, s2) -- $SOL:3:0$ + begin + op2 <= '0'; + case s1 is + when '0' => + if (s2 = '0') + then + op0 <= s0; + else + op0 <= s1; + end if; + op1 <= (s0 or s1); + when others => + op1 <= (s1 or '0'); + op0 <= s1; + op2 <= '1'; + end case; + end process; + + with ip0 select + s1 <= + ip1 when '0', + ip2 when '1', + ip3 when others; + + with st0 select + s2 <= + ip1 when V0, + ip2 when V1, + ip3 when V2, + s1 when V3; + + + P_e: with st0 select + s2 <= + ip1 when V0, + ip2 when V1, + ip3 when others; + + process (s0, s1, s2, s3) -- $SOL:4:0$ + begin + case st0 is + when V3 => + op0 <= s0; + when V2 => + op0 <= s1; + when V1 => + op0 <= s2; + when V0 => + op0 <= s3; + end case; + end process; + + Inprocess: process (s0, s1, s2, s3) -- $SOL:5:0$ + begin + case st0 is + when V3 => + op0 <= s0; + when V2 => + op0 <= s1; + when others => + op0 <= s2; + end case; + end process; + + My_Process: process (n0, n2) -- $SOL:6:0$ + begin + case n0 is + when 0 => + n1 <= 0; + when 1 to 2 => + n1 <= n2; + when 3 => + n1 <= 2; + end case; + end process; + + nothing: process (n0, n2) -- $SOL:7:0$ + begin + case n0 is + when 0 => + P_I0: n1 <= 0; + when 1 => + P_I1: n1 <= n3; + when 2 => + P_I2: n1 <= n2; + when 3 => + P_I3: n1 <= 2; + end case; + end process; + + Still: process (n0, n3) -- $SOL:8:0$ + begin + What: case n0 is + when 0 => + May: n1 <= 0; + when 1 => + Be: n1 <= n3; + when others => + Caught: n1 <= n3; + end case; + end process; +end; -- cgit v1.2.3-70-g09d2