aboutsummaryrefslogtreecommitdiffstats
path: root/psl/psl-subsets.ads
diff options
context:
space:
mode:
authorgingold <gingold@b72b5c32-5f01-0410-b925-b5c7b92870f7>2010-01-12 03:15:20 +0000
committergingold <gingold@b72b5c32-5f01-0410-b925-b5c7b92870f7>2010-01-12 03:15:20 +0000
commitfb5957a16dea47ae4021c5d4c57b980cea02ee59 (patch)
treeabdfbed5924f5be4418f74a0afe50b248e41c330 /psl/psl-subsets.ads
parent8cca0b24e2c19eedecffdeec89a8a2898da1e362 (diff)
downloadghdl-fb5957a16dea47ae4021c5d4c57b980cea02ee59.tar.gz
ghdl-fb5957a16dea47ae4021c5d4c57b980cea02ee59.tar.bz2
ghdl-fb5957a16dea47ae4021c5d4c57b980cea02ee59.zip
ghdl 0.29 release.
Diffstat (limited to 'psl/psl-subsets.ads')
-rw-r--r--psl/psl-subsets.ads23
1 files changed, 23 insertions, 0 deletions
diff --git a/psl/psl-subsets.ads b/psl/psl-subsets.ads
new file mode 100644
index 000000000..c3bae09ef
--- /dev/null
+++ b/psl/psl-subsets.ads
@@ -0,0 +1,23 @@
+with PSL.Nodes; use PSL.Nodes;
+
+package PSL.Subsets is
+ -- Check that N (a property) follows the simple subset rules from
+ -- PSL v1.1 4.4.4 Simple subset.
+ -- Ie:
+ -- - The operand of a negation operator is a Boolean.
+ -- - The operand of a 'never' operator is a Boolean or a Sequence.
+ -- - The operand of an 'eventually!' operator is a Boolean or a Sequence.
+ -- - The left-hand side operand of a logical 'and' operator is a Boolean.
+ -- - The left-hand side operand of a logical 'or' operator is a Boolean.
+ -- - The left-hand side operand of a logical implication '->' operator
+ -- is a Boolean.
+ -- - Both operands of a logical iff '<->' operator are Boolean.
+ -- - The right-hand side operand of a non-overlapping 'until*' operator is
+ -- a Boolean.
+ -- - Both operands of an overlapping 'until*' operator are Boolean.
+ -- - Both operands of a 'before*' operator are Boolean.
+ --
+ -- All other operators not mentioned above are supported in the simple
+ -- subset without restriction.
+ procedure Check_Simple (N : Node);
+end PSL.Subsets;