| summaryrefslogtreecommitdiff | 
diff options
Diffstat (limited to 'data')
| -rw-r--r-- | data/property/cnes/CNE_01100.pp | 4 | ||||
| -rw-r--r-- | data/property/cnes/CNE_01100.pro | 21 | ||||
| -rw-r--r-- | data/property/cnes/CNE_01200.pp | 2 | ||||
| -rw-r--r-- | data/property/cnes/CNE_01200.pro | 9 | ||||
| -rw-r--r-- | data/property/cnes/CNE_01400.pp | 3 | ||||
| -rw-r--r-- | data/property/cnes/CNE_01400.pro | 8 | ||||
| -rw-r--r-- | data/property/cnes/CNE_02100.pp | 4 | ||||
| -rw-r--r-- | data/property/cnes/CNE_02100.pro | 12 | ||||
| -rw-r--r-- | data/property/cnes/CNE_02600.pp | 3 | ||||
| -rw-r--r-- | data/property/cnes/CNE_02600.pro | 6 | 
10 files changed, 72 insertions, 0 deletions
| diff --git a/data/property/cnes/CNE_01100.pp b/data/property/cnes/CNE_01100.pp new file mode 100644 index 0000000..4039897 --- /dev/null +++ b/data/property/cnes/CNE_01100.pp @@ -0,0 +1,4 @@ +The name of the port $pt.IDENTIFIER$ (declared in $pt.FILE$, line $pt.LINE$, +column $pt.COLUMN$) does not match its direction. According to CNE_01100, input +ports should be prefixed by "i_", output ports by "o_", and bidirectional ports +by "b_". diff --git a/data/property/cnes/CNE_01100.pro b/data/property/cnes/CNE_01100.pro new file mode 100644 index 0000000..ddeb4e3 --- /dev/null +++ b/data/property/cnes/CNE_01100.pro @@ -0,0 +1,21 @@ +(tag_existing +   ( +      (pt port CNE_01100_BAD_NAME) +   ) +   (not +      (or +         (and +            (string_matches [identifier pt] "i_.*") +            (has_mode pt "in") +         ) +         (and +            (string_matches [identifier pt] "o_.*") +            (has_mode pt "out") +         ) +         (and +            (string_matches [identifier pt] "b_.*") +            (has_mode pt "inout") +         ) +      ) +   ) +) diff --git a/data/property/cnes/CNE_01200.pp b/data/property/cnes/CNE_01200.pp new file mode 100644 index 0000000..68479eb --- /dev/null +++ b/data/property/cnes/CNE_01200.pp @@ -0,0 +1,2 @@ +The label for the process $ps.LABEL$ (declared in $ps.FILE$, line $ps.LINE$, +column $ps.COLUMN$) is not prefixed by "P_", despite CNE_01200 requiring it to. diff --git a/data/property/cnes/CNE_01200.pro b/data/property/cnes/CNE_01200.pro new file mode 100644 index 0000000..6649103 --- /dev/null +++ b/data/property/cnes/CNE_01200.pro @@ -0,0 +1,9 @@ +(tag_existing +   ( +      (ps process CNE_01200_BAD_NAME) +   ) +   (implies +      (is_explicit_process ps) +      (string_matches [label ps] "P_.*") +   ) +) diff --git a/data/property/cnes/CNE_01400.pp b/data/property/cnes/CNE_01400.pp new file mode 100644 index 0000000..6050265 --- /dev/null +++ b/data/property/cnes/CNE_01400.pp @@ -0,0 +1,3 @@ +The name of the generic port $gc.IDENTIFIER$ (declared in $gc.FILE$, +line $gc.LINE$, column $gc.COLUMN$) is not prefixed by "g_", despite CNE_01400 +requiring it to be. diff --git a/data/property/cnes/CNE_01400.pro b/data/property/cnes/CNE_01400.pro new file mode 100644 index 0000000..412650e --- /dev/null +++ b/data/property/cnes/CNE_01400.pro @@ -0,0 +1,8 @@ +(tag_existing +   ( +      (gc generic CNE_01400_BAD_NAME) +   ) +   (not +      (string_matches [identifier gc] "g_.*") +   ) +) diff --git a/data/property/cnes/CNE_02100.pp b/data/property/cnes/CNE_02100.pp new file mode 100644 index 0000000..ff0b8e7 --- /dev/null +++ b/data/property/cnes/CNE_02100.pp @@ -0,0 +1,4 @@ +The name of the architecture $arch.IDENTIFIER$ (declared in $arch.FILE$, +line $arch.LINE$, column $arch.COLUMN$) does not match any of the names of a RTL +architecture, as defined by CNE_02100. The allowed names are "Behavioral", +"RTL", and "Simulation". diff --git a/data/property/cnes/CNE_02100.pro b/data/property/cnes/CNE_02100.pro new file mode 100644 index 0000000..8b66f0b --- /dev/null +++ b/data/property/cnes/CNE_02100.pro @@ -0,0 +1,12 @@ +(tag_existing +   ( +      (arch architecture CNE_02100_BAD_NAME) +   ) +   (not +      (or +         (identifier arch "Behavioral") +         (identifier arch "RTL") +         (identifier arch "Simulation") +      ) +   ) +) diff --git a/data/property/cnes/CNE_02600.pp b/data/property/cnes/CNE_02600.pp new file mode 100644 index 0000000..ea2d44f --- /dev/null +++ b/data/property/cnes/CNE_02600.pp @@ -0,0 +1,3 @@ +The name of the signal $sl.IDENTIFIER$ (declared in $sl.FILE$, +line $sl.LINE$, column $sl.COLUMN$) has more than 20 characters, this is not +allowed by CNE_02600. diff --git a/data/property/cnes/CNE_02600.pro b/data/property/cnes/CNE_02600.pro new file mode 100644 index 0000000..f4f89ab --- /dev/null +++ b/data/property/cnes/CNE_02600.pro @@ -0,0 +1,6 @@ +(tag_existing +   ( +      (sl signal CNE_02600_BAD_NAME) +   ) +   (string_matches [identifier sl] ".{21,}") +) | 


