| summaryrefslogtreecommitdiff |
diff options
| author | Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org> | 2017-08-13 13:02:37 +0200 |
|---|---|---|
| committer | Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org> | 2017-08-13 13:02:37 +0200 |
| commit | d798d3d9a0ecf50ceba0d55645bc7ff626ed72e9 (patch) | |
| tree | d36d01d83c82f68d78c60b13b8ef4a500e71248f | |
| parent | d18ca72caf2004c7725b3de670c7397c5bf85eb4 (diff) | |
Adds more (rather simple) properties.
| -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,}") +) |


