From fb5957a16dea47ae4021c5d4c57b980cea02ee59 Mon Sep 17 00:00:00 2001 From: gingold Date: Tue, 12 Jan 2010 03:15:20 +0000 Subject: ghdl 0.29 release. --- psl/psl-subsets.ads | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 psl/psl-subsets.ads (limited to 'psl/psl-subsets.ads') 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; -- cgit v1.2.3