diff --git a/bindings/python/ASTBindings.cpp b/bindings/python/ASTBindings.cpp index e3769ca43..f46300652 100644 --- a/bindings/python/ASTBindings.cpp +++ b/bindings/python/ASTBindings.cpp @@ -333,7 +333,6 @@ void registerAST(py::module_& m) { .def_readonly("kind", &AssertionExpr::kind) .def_readonly("syntax", &AssertionExpr::syntax) .def_property_readonly("bad", &AssertionExpr::bad) - .def_property_readonly("checkNondegeneracy", &AssertionExpr::checkNondegeneracy) .def("__repr__", [](const AssertionExpr& self) { return fmt::format("AssertionExpr(AssertionExprKind.{})", toString(self.kind)); }); @@ -346,8 +345,7 @@ void registerAST(py::module_& m) { py::class_ seqRep(m, "SequenceRepetition"); seqRep.def_readonly("kind", &SequenceRepetition::kind) - .def_readonly("range", &SequenceRepetition::range) - .def_property_readonly("admitsEmpty", &SequenceRepetition::admitsEmpty); + .def_readonly("range", &SequenceRepetition::range); py::enum_(seqRep, "Kind") .value("Consecutive", SequenceRepetition::Kind::Consecutive) @@ -355,11 +353,6 @@ void registerAST(py::module_& m) { .value("GoTo", SequenceRepetition::Kind::GoTo) .export_values(); - py::enum_(seqRep, "AdmitsEmpty") - .value("Yes", SequenceRepetition::AdmitsEmpty::Yes) - .value("No", SequenceRepetition::AdmitsEmpty::No) - .value("Depends", SequenceRepetition::AdmitsEmpty::Depends); - py::class_(m, "SimpleAssertionExpr") .def_property_readonly("expr", [](const SimpleAssertionExpr& self) { return &self.expr; }) .def_readonly("repetition", &SimpleAssertionExpr::repetition); diff --git a/include/slang/ast/expressions/AssertionExpr.h b/include/slang/ast/expressions/AssertionExpr.h index dbd4a4a4a..3f2925f6f 100644 --- a/include/slang/ast/expressions/AssertionExpr.h +++ b/include/slang/ast/expressions/AssertionExpr.h @@ -67,41 +67,55 @@ SLANG_ENUM(BinaryAssertionOperator, OP) class ASTContext; class CallExpression; -struct SequenceRange; +/// Specifies possible classifications of assertion expressions +/// as they relate to "nondegeneracy", as described in the LRM. enum class NondegeneracyStatus { + /// No factors related to nondegeneracy (i.e. the expression + /// is nondegenerate). None = 0, - // Sequence admits empty matches + /// The sequence admits empty matches. AdmitsEmpty = 1 << 0, - // Sequence accepts only empty matches + /// The sequence accepts only empty matches. AcceptsOnlyEmpty = 1 << 1, - // Sequence admits no match + /// The sequence definitely admits no match. AdmitsNoMatch = 1 << 2 }; SLANG_BITMASK(NondegeneracyStatus, AdmitsNoMatch); +/// Represents a range of potential sequence matches. +struct SequenceRange { + /// The minimum length of the range. + uint32_t min = 1; + + /// The maximum length of the range. If unset, the maximum is unbounded. + std::optional max; + + static SequenceRange fromSyntax(const syntax::SelectorSyntax& syntax, const ASTContext& context, + bool allowUnbounded); + static SequenceRange fromSyntax(const syntax::RangeSelectSyntax& syntax, + const ASTContext& context, bool allowUnbounded); + + void serializeTo(ASTSerializer& serializer) const; + + bool operator<(const SequenceRange& right) const; + + /// Determines whether this range intersects with @a other. + bool intersects(const SequenceRange& other) const; + + /// Determines whether this range is fully contained within @a other. + bool isWithin(const SequenceRange& other) const; +}; + /// The base class for assertion expressions (sequences and properties). class SLANG_EXPORT AssertionExpr { public: /// The kind of expression; indicates the type of derived class. AssertionExprKind kind; - enum class NondegeneracyFlags { - // In case of overlapping implication or followed by (`#-#`) property - // left hand sequence shall be nondegenerate - IsOverlapImplOrHashMinus, - - // In case of nonoverlapping implication or followed by (`#=#`) property - // left hand sequence shall admit at least one match and can admit only empty matches. - // Generally such sequence can be degenerate. - IsNonOverlapImplOrHashEq, - - None - }; - /// The syntax used to create the expression, if any. An expression tree can /// be created manually in which case it may not have a syntax representation. const syntax::SyntaxNode* syntax = nullptr; @@ -115,21 +129,37 @@ class SLANG_EXPORT AssertionExpr { /// Indicates whether the expression is invalid. bool bad() const { return kind == AssertionExprKind::Invalid; } - // Checks that the sequence matches one of the following: - // - admits empty matches - // - accepts only empty matches - // - admits no matches + /// Checks whether this assertion expression is nondegenerate or whether it has + /// properties of degeneracy (admitting empty matches or no matches at all). bitmask checkNondegeneracy() const; - /// Computes possible clock ticks (delay) length of sequence under assertion expression + /// Computes possible clock ticks (delay) length of sequence under assertion expression. std::optional computeSequenceLength() const; + /// Specifies binding behavior of property expressions as + /// it pertains to nondegeneracy checking. + enum class NondegeneracyRequirement { + /// Any sequence that is used as a property shall be nondegenerate + // and shall not admit any empty match. + Default, + + /// Any sequence that is used as the antecedent of an overlapping implication + /// or followed-by operator shall be nondegenerate. + OverlapOp, + + /// Any sequence that is used as the antecedent of a nonoverlapping implication + /// or followed-by operator shall admit at least one match. Such a sequence can + /// admit only empty matches. + NonOverlapOp, + }; + static const AssertionExpr& bind(const syntax::SequenceExprSyntax& syntax, const ASTContext& context, bool allowDisable = false); - static const AssertionExpr& bind(const syntax::PropertyExprSyntax& syntax, - const ASTContext& context, bool allowDisable = false, - NondegeneracyFlags nondegFlags = NondegeneracyFlags::None); + static const AssertionExpr& bind( + const syntax::PropertyExprSyntax& syntax, const ASTContext& context, + bool allowDisable = false, + NondegeneracyRequirement nondegRequirement = NondegeneracyRequirement::Default); static const AssertionExpr& bind(const syntax::PropertySpecSyntax& syntax, const ASTContext& context); @@ -206,41 +236,13 @@ class SLANG_EXPORT InvalidAssertionExpr : public AssertionExpr { return NondegeneracyStatus::None; } - std::optional computeSequenceLengthImpl() const; + std::optional computeSequenceLengthImpl() const { return {}; } static bool isKind(AssertionExprKind kind) { return kind == AssertionExprKind::Invalid; } void serializeTo(ASTSerializer& serializer) const; }; -/// Represents a range of potential sequence matches. -struct SequenceRange { - /// The minimum length of the range. - uint32_t min = 1; - - /// The maximum length of the range. If unset, the maximum is unbounded. - std::optional max; - - static SequenceRange fromSyntax(const syntax::SelectorSyntax& syntax, const ASTContext& context, - bool allowUnbounded); - static SequenceRange fromSyntax(const syntax::RangeSelectSyntax& syntax, - const ASTContext& context, bool allowUnbounded); - - void serializeTo(ASTSerializer& serializer) const; - - bool operator<(const SequenceRange& right) const; - - /// `SequenceRange`s intersects if max delay of one range - /// is greater than min delay of other range. - bool isIntersect(const SequenceRange& other) const; - - /// `SequenceRange` is within other `SequenceRange` - /// if min delay of one range is greater or equal than - /// min delay of other range and max delay of one range - /// is less or equal than max delay of other range. - bool isWithin(const SequenceRange& other) const; -}; - /// Encodes a repetition of some sub-sequence. struct SequenceRepetition { /// The kind of repetition. @@ -261,23 +263,9 @@ struct SequenceRepetition { SequenceRepetition(const syntax::SequenceRepetitionSyntax& syntax, const ASTContext& context); - /// Defines ways in which a sequence may admit an empty match. - enum class AdmitsEmpty { - /// Yes, the sequence admits an empty match. - Yes, - - /// No, the sequence does not admit an empty match. - No, - - /// The sequence may or may not admit an empty match. - Depends, - - /// The sequence accepts only empty matches and nothing else. - Only, - }; - - /// Classifies the repetition as admitting an empty match or not. - AdmitsEmpty admitsEmpty() const; + /// Checks whether this assertion expression is nondegenerate or whether it has + /// properties of degeneracy (admitting empty matches or no matches at all). + bitmask checkNondegeneracy() const; void serializeTo(ASTSerializer& serializer) const; }; @@ -291,7 +279,7 @@ class SLANG_EXPORT SimpleAssertionExpr : public AssertionExpr { /// An optional repetition of the sequence. std::optional repetition; - /// Store `true` if sequence exression can be evaluated as constant `false` (`0`). + /// Set to true if the sequence expression is a known `false` constant value. bool isNullExpr; SimpleAssertionExpr(const Expression& expr, std::optional repetition, @@ -300,9 +288,7 @@ class SLANG_EXPORT SimpleAssertionExpr : public AssertionExpr { isNullExpr(isNullExpr) {} void requireSequence(const ASTContext& context, DiagCode code) const; - bitmask checkNondegeneracyImpl() const; - std::optional computeSequenceLengthImpl() const; static AssertionExpr& fromSyntax(const syntax::SimpleSequenceExprSyntax& syntax, @@ -337,7 +323,6 @@ class SLANG_EXPORT SequenceConcatExpr : public AssertionExpr { AssertionExpr(AssertionExprKind::SequenceConcat), elements(elements) {} bitmask checkNondegeneracyImpl() const; - std::optional computeSequenceLengthImpl() const; static AssertionExpr& fromSyntax(const syntax::DelayedSequenceExprSyntax& syntax, @@ -454,13 +439,6 @@ class SLANG_EXPORT BinaryAssertionExpr : public AssertionExpr { void requireSequence(const ASTContext& context, DiagCode code) const; bitmask checkNondegeneracyImpl() const; - - /// Returns the maximum possible sequence length of the two operands. - /// If one of the operands is unbounded, return `nullopt`. - /// In case of `through` binary operator it returns `SequenceRange` - /// of only right operand because just only right part have a real matches - /// unlike the left (left is just formally a condition). - /// See 16.9.9 of `SystemVerilog` LRM for details. std::optional computeSequenceLengthImpl() const; static AssertionExpr& fromSyntax(const syntax::BinarySequenceExprSyntax& syntax, @@ -526,7 +504,9 @@ class SLANG_EXPORT ClockingAssertionExpr : public AssertionExpr { ClockingAssertionExpr(const TimingControl& clocking, const AssertionExpr& expr) : AssertionExpr(AssertionExprKind::Clocking), clocking(clocking), expr(expr) {} - bitmask checkNondegeneracyImpl() const; + bitmask checkNondegeneracyImpl() const { + return expr.checkNondegeneracy(); + } std::optional computeSequenceLengthImpl() const { return expr.computeSequenceLength(); @@ -651,7 +631,6 @@ class SLANG_EXPORT ConditionalAssertionExpr : public AssertionExpr { return NondegeneracyStatus::None; } - /// Returns maximum possible sequence length beetween `if` and `else` sequence expressions. std::optional computeSequenceLengthImpl() const; static AssertionExpr& fromSyntax(const syntax::ConditionalPropertyExprSyntax& syntax, @@ -700,8 +679,6 @@ class SLANG_EXPORT CaseAssertionExpr : public AssertionExpr { return NondegeneracyStatus::None; } - /// Returns maximum possible sequence length beetween all case labels sequence expressions - /// include `default` label std::optional computeSequenceLengthImpl() const; static AssertionExpr& fromSyntax(const syntax::CasePropertyExprSyntax& syntax, @@ -741,7 +718,6 @@ class SLANG_EXPORT DisableIffAssertionExpr : public AssertionExpr { return NondegeneracyStatus::None; } - /// Returns `nullopt` if `disable iff` condition is always `true` (`1`) std::optional computeSequenceLengthImpl() const; static AssertionExpr& fromSyntax(const syntax::DisableIffSyntax& syntax, diff --git a/source/ast/expressions/AssertionExpr.cpp b/source/ast/expressions/AssertionExpr.cpp index 3573900c1..fe280e5ba 100644 --- a/source/ast/expressions/AssertionExpr.cpp +++ b/source/ast/expressions/AssertionExpr.cpp @@ -119,53 +119,47 @@ const AssertionExpr& AssertionExpr::bind(const SequenceExprSyntax& syntax, return *result; } +static void enforceNondegeneracy(const AssertionExpr& expr, const ASTContext& context, + AssertionExpr::NondegeneracyRequirement nondegRequirement, + const SyntaxNode& syntax) { + const auto seqNondegenSt = expr.checkNondegeneracy(); + const bool admitsEmpty = seqNondegenSt.has(NondegeneracyStatus::AdmitsEmpty); + const bool acceptsOnlyEmpty = seqNondegenSt.has(NondegeneracyStatus::AcceptsOnlyEmpty); + const bool admitsNoMatch = seqNondegenSt.has(NondegeneracyStatus::AdmitsNoMatch); + + using NR = AssertionExpr::NondegeneracyRequirement; + if (nondegRequirement == NR::OverlapOp) { + if (acceptsOnlyEmpty || admitsNoMatch) { + auto& diag = context.addDiag(diag::OverlapImplNondegenerate, syntax.sourceRange()); + diag.addNote(acceptsOnlyEmpty ? diag::SeqAcceptsOnlyEmptyMatches + : diag::SeqAdmitsNoMatches, + syntax.sourceRange()); + } + } + else if (nondegRequirement == NR::NonOverlapOp) { + if (admitsNoMatch) { + auto& diag = context.addDiag(diag::NonOverlapImplNondegenerate, syntax.sourceRange()); + diag.addNote(diag::SeqAdmitsNoMatches, syntax.sourceRange()); + } + } + else if (admitsEmpty || admitsNoMatch) { + auto& diag = context.addDiag(diag::SeqPropNondegenerate, syntax.sourceRange()); + diag.addNote(admitsEmpty ? diag::SeqAdmitsEmptyMatches : diag::SeqAdmitsNoMatches, + syntax.sourceRange()); + } +} + const AssertionExpr& AssertionExpr::bind(const PropertyExprSyntax& syntax, const ASTContext& context, bool allowDisable, - NondegeneracyFlags nondegFlags) { + NondegeneracyRequirement nondegRequirement) { ASTContext ctx(context); ctx.flags |= ASTFlags::AssignmentDisallowed; AssertionExpr* result; switch (syntax.kind) { case SyntaxKind::SimplePropertyExpr: { - // Just a simple passthrough to creating the sequence expression - // contained within. auto& seq = bind(*syntax.as().expr, ctx, allowDisable); - const auto seqNondegenSt = seq.checkNondegeneracy(); - bool isSeqAdmitsEmpty = seqNondegenSt.has(NondegeneracyStatus::AdmitsEmpty); - bool isSeqAcceptsOnlyEmpty = seqNondegenSt.has(NondegeneracyStatus::AcceptsOnlyEmpty); - bool isSeqAdmitsNoMatch = seqNondegenSt.has(NondegeneracyStatus::AdmitsNoMatch); - - // See 16.12.22 section at SystemVerilog LRM for details. - // Any sequence that is used as the antecedent of an overlapping implication (|->) shall - // be nondegenerate. - if (nondegFlags == NondegeneracyFlags::IsOverlapImplOrHashMinus) { - if (isSeqAcceptsOnlyEmpty || isSeqAdmitsNoMatch) { - auto& diag = context.addDiag(diag::OverlapImplNondegenerate, - syntax.sourceRange()); - diag.addNote((isSeqAcceptsOnlyEmpty) ? diag::SeqAcceptsOnlyEmptyMatches - : diag::SeqAdmitsNoMatches, - syntax.sourceRange()); - } - } - // Any sequence that is used as the antecedent of a nonoverlapping implication (|=>) - // shall admit at least one match. Such a sequence can admit only empty matches. - else if (nondegFlags == NondegeneracyFlags::IsNonOverlapImplOrHashEq) { - if (isSeqAdmitsNoMatch) { - auto& diag = context.addDiag(diag::NonOverlapImplNondegenerate, - syntax.sourceRange()); - diag.addNote(diag::SeqAdmitsNoMatches, syntax.sourceRange()); - } - } - // Any sequence that is used as a property shall be nondegenerate and shall not admit - // any empty match. - else if (isSeqAdmitsEmpty || isSeqAdmitsNoMatch) { - auto& diag = context.addDiag(diag::SeqPropNondegenerate, syntax.sourceRange()); - diag.addNote((isSeqAdmitsEmpty) ? diag::SeqAdmitsEmptyMatches - : diag::SeqAdmitsNoMatches, - syntax.sourceRange()); - } - + enforceNondegeneracy(seq, context, nondegRequirement, syntax); return seq; } case SyntaxKind::AndPropertyExpr: @@ -404,10 +398,6 @@ void AssertionExpr::checkSampledValueExpr(const Expression& expr, const ASTConte expr.visit(visitor); } -std::optional InvalidAssertionExpr::computeSequenceLengthImpl() const { - return std::nullopt; -} - void InvalidAssertionExpr::serializeTo(ASTSerializer& serializer) const { if (child) serializer.write("child", *child); @@ -469,44 +459,34 @@ void SequenceRange::serializeTo(ASTSerializer& serializer) const { } bool SequenceRange::operator<(const SequenceRange& right) const { - // if both sequences are unbounded then check min's + // if both sequences are unbounded then check mins if (!max.has_value() && !right.max.has_value()) return min < right.min; - // if both sequences are bounded then compare it's diff's - if (max.has_value() && right.max.has_value()) { - uint32_t maxVal = max.value(); - uint32_t rightMaxVal = right.max.value(); - return ((maxVal - min) < (rightMaxVal - right.min)) && (min < right.min); - } - - // if only left is bounded than return `true` because right sequence is potentially - // have an infinite number of matches - if (max.has_value()) - return true; + // if both sequences are bounded then compare the lengths + if (max.has_value() && right.max.has_value()) + return (*max - min) < (*right.max - right.min) && min < right.min; - // return `false` otherwise (in case is right sequence if bounded) - return false; + // Otherwise the left is smaller iff it is bounded. + return max.has_value(); } -bool SequenceRange::isIntersect(const SequenceRange& other) const { +bool SequenceRange::intersects(const SequenceRange& other) const { if (!max.has_value()) - return (other.max.has_value()) ? (min >= other.min && min <= other.max.value()) - : min == other.min; + return min >= other.min && min <= other.max.value_or(UINT32_MAX); if (!other.max.has_value()) - return (max.has_value()) ? (other.min >= min && other.min <= max.value()) - : other.min == min; + return other.min >= min && other.min <= max.value(); return !(max.value() < other.min || other.max.value() < min); } bool SequenceRange::isWithin(const SequenceRange& other) const { if (!other.max.has_value()) - return (max.has_value()) ? (min == other.min && max == other.min) : min == other.min; + return max.has_value() ? min == other.min && max == other.min : min == other.min; - return (max.has_value()) ? (min >= other.min && max <= other.max) - : (min >= other.min && min <= other.max); + return max.has_value() ? min >= other.min && max <= other.max + : min >= other.min && min <= other.max; } SequenceRepetition::SequenceRepetition(const SequenceRepetitionSyntax& syntax, @@ -532,24 +512,14 @@ SequenceRepetition::SequenceRepetition(const SequenceRepetitionSyntax& syntax, range = SequenceRange::fromSyntax(*syntax.selector, context, /* allowUnbounded */ true); } -SequenceRepetition::AdmitsEmpty SequenceRepetition::admitsEmpty() const { - // If and only if min and max delays are both zero, then the sequence accepts only empty - // matches. - if (range.min == 0 && range.max.has_value() && range.max.value() == 0) - return AdmitsEmpty::Only; - - switch (kind) { - case Consecutive: - if (range.min == 0) - return AdmitsEmpty::Yes; - return AdmitsEmpty::Depends; - case GoTo: - case Nonconsecutive: - if (range.min == 0) - return AdmitsEmpty::Yes; - return AdmitsEmpty::No; +bitmask SequenceRepetition::checkNondegeneracy() const { + bitmask res; + if (range.min == 0) { + res = NondegeneracyStatus::AdmitsEmpty; + if (range.max == 0) + res |= NondegeneracyStatus::AcceptsOnlyEmpty; } - SLANG_UNREACHABLE; + return res; } void SequenceRepetition::serializeTo(ASTSerializer& serializer) const { @@ -605,8 +575,7 @@ AssertionExpr& SimpleAssertionExpr::fromSyntax(const SimpleSequenceExprSyntax& s } const auto evaluatedValue = context.tryEval(expr); - return *comp.emplace( - expr, repetition, (evaluatedValue.isInteger() && !evaluatedValue.isTrue())); + return *comp.emplace(expr, repetition, evaluatedValue.isFalse()); } void SimpleAssertionExpr::requireSequence(const ASTContext& context, DiagCode code) const { @@ -623,20 +592,14 @@ void SimpleAssertionExpr::requireSequence(const ASTContext& context, DiagCode co } bitmask SimpleAssertionExpr::checkNondegeneracyImpl() const { + // If simple sequence expression can be evaluated to false + // then it admits no possible match. bitmask res = NondegeneracyStatus::None; + if (isNullExpr) + res |= NondegeneracyStatus::AdmitsNoMatch; - // If simple sequence expression can be evaluated to `false` (`0`) - // manually then it should be reported as sequence - // with no possible match - res = (isNullExpr) ? res | NondegeneracyStatus::AdmitsNoMatch : res; - - if (repetition) { - auto repEmptyStatus = repetition->admitsEmpty(); - if (repEmptyStatus == SequenceRepetition::AdmitsEmpty::Yes) - res |= NondegeneracyStatus::AdmitsEmpty; - if (repEmptyStatus == SequenceRepetition::AdmitsEmpty::Only) - res |= (NondegeneracyStatus::AcceptsOnlyEmpty | NondegeneracyStatus::AdmitsEmpty); - } + if (repetition) + res |= repetition->checkNondegeneracy(); if (expr.kind == ExpressionKind::AssertionInstance) { auto& aie = expr.as(); @@ -647,16 +610,17 @@ bitmask SimpleAssertionExpr::checkNondegeneracyImpl() const } std::optional SimpleAssertionExpr::computeSequenceLengthImpl() const { + // If there is only empty match sequence then it has a zero delay length. SequenceRange res; - // If there is only empty match sequence then it's have a zero delay length - res.min = (checkNondegeneracy().has(NondegeneracyStatus::AcceptsOnlyEmpty)) ? 0 : 1; + res.min = checkNondegeneracy().has(NondegeneracyStatus::AcceptsOnlyEmpty) ? 0 : 1; res.max = res.min; if (expr.kind == ExpressionKind::AssertionInstance) { if (auto& aie = expr.as(); aie.type->isSequenceType()) { - if (std::optional aieSeqLength = aie.body.computeSequenceLength(); - aieSeqLength.has_value() && (res < aieSeqLength.value())) + if (auto aieSeqLength = aie.body.computeSequenceLength(); + aieSeqLength.has_value() && (res < aieSeqLength.value())) { return aieSeqLength.value(); + } } } return res; @@ -720,8 +684,8 @@ bitmask SequenceConcatExpr::checkNondegeneracyImpl() const bool admitsNoMatch = false; auto left = elements.begin(); SLANG_ASSERT(left != elements.end()); - auto leftNondegenSt = left->sequence->checkNondegeneracy(); + auto leftNondegenSt = left->sequence->checkNondegeneracy(); if (left->delay.min != 0 || !leftNondegenSt.has(NondegeneracyStatus::AdmitsEmpty)) admitsEmpty = false; @@ -731,27 +695,27 @@ bitmask SequenceConcatExpr::checkNondegeneracyImpl() const // See SystemVerilog LRM sections 16.9.2.1 and F.3.4.2.2 for details while (admitsEmpty || !admitsNoMatch) { const auto right = left + 1; - if (left == elements.end() || right == elements.end()) + if (right == elements.end()) break; + // If any element of concat sequence is no match then all concat sequence is no match. const auto rightNondegenSt = right->sequence->checkNondegeneracy(); - // If any element of concat sequence is no match then all concat sequence is no match if (rightNondegenSt.has(NondegeneracyStatus::AdmitsNoMatch)) admitsNoMatch = true; if (!rightNondegenSt.has(NondegeneracyStatus::AdmitsEmpty)) admitsEmpty = false; - // If right part is present with zero min and max delays - if (!right->delay.min && right->delay.max.has_value() && !right->delay.max.value()) { + if (right->delay.min == 0 && right->delay.max == 0) { admitsEmpty = false; // (empty ##0 seq) does not result in a match // We need to check that case if and only if we are at the start of concat sequence // because empty parts in the middle of concat sequence are processed by the next `if` if (left == elements.begin() && - leftNondegenSt.has(NondegeneracyStatus::AcceptsOnlyEmpty)) + leftNondegenSt.has(NondegeneracyStatus::AcceptsOnlyEmpty)) { admitsNoMatch = true; + } // (seq ##0 empty) does not result in a match. if (rightNondegenSt.has(NondegeneracyStatus::AcceptsOnlyEmpty)) @@ -761,40 +725,37 @@ bitmask SequenceConcatExpr::checkNondegeneracyImpl() const if (right->delay.min > 1) admitsEmpty = false; - ++left; + left = right; leftNondegenSt = rightNondegenSt; } bitmask res; - res = (admitsEmpty) ? res | NondegeneracyStatus::AdmitsEmpty : res; - res = (admitsNoMatch) ? res | NondegeneracyStatus::AdmitsNoMatch : res; + if (admitsEmpty) + res |= NondegeneracyStatus::AdmitsEmpty; + if (admitsNoMatch) + res |= NondegeneracyStatus::AdmitsNoMatch; return res; } std::optional SequenceConcatExpr::computeSequenceLengthImpl() const { - auto it = elements.begin(); - SLANG_ASSERT(it != elements.end()); + uint32_t delayMin = 0; + uint32_t delayMax = 0; + for (auto it = elements.begin(); it != elements.end(); it++) { + const bool isAcceptsOnlyEmpty = it->sequence->checkNondegeneracy().has( + NondegeneracyStatus::AcceptsOnlyEmpty); - // Default delay length for concat sequence is 1 if it's admits not only empty matches. - bool isAcceptsOnlyEmpty = it->sequence->checkNondegeneracy().has( - NondegeneracyStatus::AcceptsOnlyEmpty); - uint32_t delayMin = (isAcceptsOnlyEmpty) ? 0 : 1; - uint32_t delayMax = delayMin; + // Default delay length for concat sequence is 1 if it admits a non-empty match. + if (it == elements.begin() && !isAcceptsOnlyEmpty) + delayMin = delayMax = 1; - while (it != elements.end()) { // (empty ##n seq), where n is greater than 0, is equivalent to (##(n-1) seq). - // also ((##n empty) ; (seq ##n empty)), where n is greater than 0, is equivalent to + // Also ((##n empty) ; (seq ##n empty)), where n is greater than 0, is equivalent to // ((##(n-1) `true) ; (seq ##(n-1) `true)) - delayMin += ((it->delay.min && isAcceptsOnlyEmpty) ? it->delay.min - 1 : it->delay.min); + delayMin += (it->delay.min && isAcceptsOnlyEmpty) ? it->delay.min - 1 : it->delay.min; if (it->delay.max.has_value()) { const auto maxVal = it->delay.max.value(); - delayMax += ((maxVal && isAcceptsOnlyEmpty) ? maxVal - 1 : maxVal); + delayMax += (maxVal && isAcceptsOnlyEmpty) ? maxVal - 1 : maxVal; } - - ++it; - if (it != elements.end()) - isAcceptsOnlyEmpty = it->sequence->checkNondegeneracy().has( - NondegeneracyStatus::AcceptsOnlyEmpty); } SequenceRange res; @@ -912,15 +873,8 @@ AssertionExpr& SequenceWithMatchExpr::fromSyntax(const ParenthesizedSequenceExpr bitmask SequenceWithMatchExpr::checkNondegeneracyImpl() const { bitmask res; - - if (repetition) { - const auto seqRepEmpty = repetition->admitsEmpty(); - res = (seqRepEmpty == SequenceRepetition::AdmitsEmpty::Yes) - ? res | NondegeneracyStatus::AdmitsEmpty - : res; - if (seqRepEmpty == SequenceRepetition::AdmitsEmpty::Only) - res = res | NondegeneracyStatus::AcceptsOnlyEmpty | NondegeneracyStatus::AdmitsEmpty; - } + if (repetition) + res = repetition->checkNondegeneracy(); return res | expr.checkNondegeneracy(); } @@ -1062,18 +1016,13 @@ AssertionExpr& BinaryAssertionExpr::fromSyntax(const BinarySequenceExprSyntax& s AssertionExpr& BinaryAssertionExpr::fromSyntax(const BinaryPropertyExprSyntax& syntax, const ASTContext& context) { - // The followed-by operators are the duals of the implication operators. So implication - // nondegeneracy check rules are also applyed to it. Therefore, sequence_expr #-# property_expr - // is equivalent to the following: `not (sequence_expr |-> not property_expr)` - bool isOverlapImplOrHashMinus = (syntax.op.kind == TokenKind::OrMinusArrow) || - (syntax.op.kind == TokenKind::HashMinusHash); - // sequence_expr #=# property_expr is equivalent to the following: - // not (sequence_expr |=> not property_expr) - bool isNonOverlapImplOrHashEq = (syntax.op.kind == TokenKind::OrEqualsArrow) || - (syntax.op.kind == TokenKind::HashEqualsHash); + const bool isOverlapOp = (syntax.op.kind == TokenKind::OrMinusArrow) || + (syntax.op.kind == TokenKind::HashMinusHash); + const bool isNonOverlapOp = (syntax.op.kind == TokenKind::OrEqualsArrow) || + (syntax.op.kind == TokenKind::HashEqualsHash); bitmask lflags, rflags; - if (isNonOverlapImplOrHashEq) { + if (isNonOverlapOp) { rflags = ASTFlags::PropertyTimeAdvance; } else if (syntax.kind == SyntaxKind::SUntilPropertyExpr || @@ -1081,14 +1030,14 @@ AssertionExpr& BinaryAssertionExpr::fromSyntax(const BinaryPropertyExprSyntax& s lflags = rflags = ASTFlags::PropertyNegation; } - NondegeneracyFlags nondegFlags = (isOverlapImplOrHashMinus) - ? NondegeneracyFlags::IsOverlapImplOrHashMinus - : NondegeneracyFlags::None; - nondegFlags = (isNonOverlapImplOrHashEq) ? NondegeneracyFlags::IsNonOverlapImplOrHashEq - : nondegFlags; + NondegeneracyRequirement nondegenRequirement = NondegeneracyRequirement::Default; + if (isOverlapOp) + nondegenRequirement = NondegeneracyRequirement::OverlapOp; + else if (isNonOverlapOp) + nondegenRequirement = NondegeneracyRequirement::NonOverlapOp; auto& comp = context.getCompilation(); - auto& left = bind(*syntax.left, context.resetFlags(lflags), false, nondegFlags); + auto& left = bind(*syntax.left, context.resetFlags(lflags), false, nondegenRequirement); auto& right = bind(*syntax.right, context.resetFlags(rflags)); // clang-format off @@ -1149,70 +1098,68 @@ void BinaryAssertionExpr::requireSequence(const ASTContext& context, DiagCode co } bitmask BinaryAssertionExpr::checkNondegeneracyImpl() const { - bitmask res; const auto leftNondegenSt = left.checkNondegeneracy(); const auto rightNondegenSt = right.checkNondegeneracy(); - bool leftAdmitsEmpty = leftNondegenSt.has(NondegeneracyStatus::AdmitsEmpty); - bool rightAdmitsEmpty = rightNondegenSt.has(NondegeneracyStatus::AdmitsEmpty); - bool leftAdmitsNoMatch = leftNondegenSt.has(NondegeneracyStatus::AdmitsNoMatch); - bool rightAdmitsNoMatch = rightNondegenSt.has(NondegeneracyStatus::AdmitsNoMatch); + const bool leftAdmitsEmpty = leftNondegenSt.has(NondegeneracyStatus::AdmitsEmpty); + const bool rightAdmitsEmpty = rightNondegenSt.has(NondegeneracyStatus::AdmitsEmpty); + const bool leftAdmitsNoMatch = leftNondegenSt.has(NondegeneracyStatus::AdmitsNoMatch); + const bool rightAdmitsNoMatch = rightNondegenSt.has(NondegeneracyStatus::AdmitsNoMatch); + bitmask res; switch (op) { case BinaryAssertionOperator::Or: { - res = (leftAdmitsEmpty || rightAdmitsEmpty) ? res | NondegeneracyStatus::AdmitsEmpty - : res; + if (leftAdmitsEmpty || rightAdmitsEmpty) + res |= NondegeneracyStatus::AdmitsEmpty; - // In case of `or` full sequence is no match if and only if both parts are no match - res = (leftAdmitsNoMatch && rightAdmitsNoMatch) - ? res | NondegeneracyStatus::AdmitsNoMatch - : res; + // In case of `or` full sequence is no match if and only if both parts are no match. + if (leftAdmitsNoMatch && rightAdmitsNoMatch) + res |= NondegeneracyStatus::AdmitsNoMatch; break; } case BinaryAssertionOperator::And: { - res = (leftAdmitsEmpty && rightAdmitsEmpty) ? res | NondegeneracyStatus::AdmitsEmpty - : res; + if (leftAdmitsEmpty && rightAdmitsEmpty) + res |= NondegeneracyStatus::AdmitsEmpty; - // In case of `and` full sequence is no match if and only if any part is no match - res = (leftAdmitsNoMatch || rightAdmitsNoMatch) - ? res | NondegeneracyStatus::AdmitsNoMatch - : res; + // In case of `and` full sequence is no match if and only if any part is no match. + if (leftAdmitsNoMatch || rightAdmitsNoMatch) + res |= NondegeneracyStatus::AdmitsNoMatch; break; } case BinaryAssertionOperator::Intersect: { - res = (leftAdmitsEmpty && rightAdmitsEmpty) ? res | NondegeneracyStatus::AdmitsEmpty - : res; + if (leftAdmitsEmpty && rightAdmitsEmpty) + res |= NondegeneracyStatus::AdmitsEmpty; + // In case of `intersect` full sequence is no match if both parts don't have any + // possible overlap in their length ranges. const auto leftLen = left.computeSequenceLength(); const auto rightLen = right.computeSequenceLength(); - - // In case of `intersect` full sequence is no match if both parts aren't have any - // possible equal delay range - res = (leftAdmitsNoMatch || rightAdmitsNoMatch || !leftLen.has_value() || - !rightLen.has_value() || !leftLen.value().isIntersect(rightLen.value())) - ? res | NondegeneracyStatus::AdmitsNoMatch - : res; + if (leftAdmitsNoMatch || rightAdmitsNoMatch || !leftLen.has_value() || + !rightLen.has_value() || !leftLen.value().intersects(rightLen.value())) { + res |= NondegeneracyStatus::AdmitsNoMatch; + } break; } case BinaryAssertionOperator::Within: { - res = (leftAdmitsEmpty && rightAdmitsEmpty) ? res | NondegeneracyStatus::AdmitsEmpty - : res; + if (leftAdmitsEmpty && rightAdmitsEmpty) + res |= NondegeneracyStatus::AdmitsEmpty; + // In case of `within` full sequence is no match if left side delay range is within + // right side delay range. const auto leftLen = left.computeSequenceLength(); const auto rightLen = right.computeSequenceLength(); - - // In case of `within` full sequence is no match if left part delay range is within - // right part delay range - res = (leftAdmitsNoMatch || rightAdmitsNoMatch || !leftLen.has_value() || - !rightLen.has_value() || !leftLen.value().isWithin(rightLen.value())) - ? res | NondegeneracyStatus::AdmitsNoMatch - : res; + if (leftAdmitsNoMatch || rightAdmitsNoMatch || !leftLen.has_value() || + !rightLen.has_value() || !leftLen.value().isWithin(rightLen.value())) { + res |= NondegeneracyStatus::AdmitsNoMatch; + } break; } case BinaryAssertionOperator::Throughout: { - res = (rightAdmitsEmpty) ? res | NondegeneracyStatus::AdmitsEmpty : res; + if (rightAdmitsEmpty) + res |= NondegeneracyStatus::AdmitsEmpty; // In case of `throughout` full sequence is no match if right part is no match - res = (rightAdmitsNoMatch) ? res | NondegeneracyStatus::AdmitsNoMatch : res; + if (rightAdmitsNoMatch) + res |= NondegeneracyStatus::AdmitsNoMatch; break; } default: @@ -1264,12 +1211,8 @@ AssertionExpr& FirstMatchAssertionExpr::fromSyntax(const FirstMatchSequenceExprS bitmask FirstMatchAssertionExpr::checkNondegeneracyImpl() const { auto res = seq.checkNondegeneracy(); - if (!matchItems.empty()) { - // Clear `admitEmpty` and `acceptOnlyEmpty` bits - res = (res.has(NondegeneracyStatus::AdmitsNoMatch)) ? NondegeneracyStatus::AdmitsNoMatch - : NondegeneracyStatus::None; - } - + if (!matchItems.empty()) + res &= ~(NondegeneracyStatus::AdmitsEmpty | NondegeneracyStatus::AcceptsOnlyEmpty); return res; } @@ -1330,10 +1273,6 @@ AssertionExpr& ClockingAssertionExpr::fromSyntax(const TimingControlSyntax& synt return *comp.emplace(clocking, expr); } -bitmask ClockingAssertionExpr::checkNondegeneracyImpl() const { - return expr.checkNondegeneracy(); -} - void ClockingAssertionExpr::serializeTo(ASTSerializer& serializer) const { serializer.write("clocking", clocking); serializer.write("expr", expr); @@ -1344,17 +1283,7 @@ AssertionExpr& StrongWeakAssertionExpr::fromSyntax(const StrongWeakPropertyExprS auto& comp = context.getCompilation(); auto& expr = bind(*syntax.expr, context); expr.requireSequence(context); - - // Any sequence that is used as a property shall be nondegenerate and shall not admit - // any empty match. - const auto seqNondegenSt = expr.checkNondegeneracy(); - bool isSeqAdmitsEmpty = seqNondegenSt.has(NondegeneracyStatus::AdmitsEmpty); - bool isSeqAdmitsNoMatch = seqNondegenSt.has(NondegeneracyStatus::AdmitsNoMatch); - if (isSeqAdmitsEmpty || isSeqAdmitsNoMatch) { - auto& diag = context.addDiag(diag::SeqPropNondegenerate, syntax.sourceRange()); - diag.addNote((isSeqAdmitsEmpty) ? diag::SeqAdmitsEmptyMatches : diag::SeqAdmitsNoMatches, - syntax.expr->sourceRange()); - } + enforceNondegeneracy(expr, context, NondegeneracyRequirement::Default, syntax); return *comp.emplace( expr, syntax.keyword.kind == TokenKind::StrongKeyword ? Strong : Weak); @@ -1407,15 +1336,12 @@ void AbortAssertionExpr::serializeTo(ASTSerializer& serializer) const { } std::optional ConditionalAssertionExpr::computeSequenceLengthImpl() const { - if (checkNondegeneracy().has(NondegeneracyStatus::AdmitsNoMatch)) - return std::nullopt; - std::optional max; - if (const auto ifLen = ifExpr.computeSequenceLength(); ifLen.has_value()) + if (const auto ifLen = ifExpr.computeSequenceLength()) max = ifLen.value(); if (elseExpr) { - if (const auto elseLen = elseExpr->computeSequenceLength(); elseLen.has_value()) { + if (const auto elseLen = elseExpr->computeSequenceLength()) { if (const auto elseLenVal = elseLen.value(); !max.has_value() || max < elseLenVal) max = elseLenVal; } @@ -1434,11 +1360,9 @@ AssertionExpr& ConditionalAssertionExpr::fromSyntax(const ConditionalPropertyExp if (syntax.elseClause) elseExpr = &bind(*syntax.elseClause->expr, context); - // If condition can be evaluated only as `false` (`0`) than sequence property - // is no match + // If condition is a constant false value then there is never a match. if (!elseExpr) { - if (const auto evaluatedValue = context.tryEval(cond); - evaluatedValue.isInteger() && !evaluatedValue.isTrue()) { + if (context.tryEval(cond).isFalse()) { auto& diag = context.addDiag(diag::SeqPropNondegenerate, syntax.sourceRange()); diag.addNote(diag::SeqPropCondAlwaysFalse, cond.sourceRange); } @@ -1457,18 +1381,18 @@ void ConditionalAssertionExpr::serializeTo(ASTSerializer& serializer) const { std::optional CaseAssertionExpr::computeSequenceLengthImpl() const { std::optional max; for (const auto& item : items) { - if (const auto itemLen = item.body->computeSequenceLength(); itemLen.has_value()) { + if (const auto itemLen = item.body->computeSequenceLength()) { if (const auto itemLenVal = itemLen.value(); !max.has_value() || max < itemLenVal) max = itemLenVal; } } if (defaultCase) { - if (const auto defaultItemLen = defaultCase->computeSequenceLength(); - defaultItemLen.has_value()) { + if (const auto defaultItemLen = defaultCase->computeSequenceLength()) { if (const auto defaultItemLenVal = defaultItemLen.value(); - !max.has_value() || max < defaultItemLenVal) + !max.has_value() || max < defaultItemLenVal) { max = defaultItemLenVal; + } } } @@ -1543,8 +1467,7 @@ AssertionExpr& DisableIffAssertionExpr::fromSyntax(const DisableIffSyntax& synta checkSampledValueExpr(cond, context, false, diag::DisableIffLocalVar, diag::DisableIffMatched); - // If condition of `disable iff` can be evaluated only as `true` (`1`) than sequence property - // is no match + // If condition is always true then there's never a match. if (context.tryEval(cond).isTrue()) { auto& diag = context.addDiag(diag::SeqPropNondegenerate, syntax.sourceRange()); diag.addNote(diag::DisableIffCondAlwaysTrue, cond.sourceRange); diff --git a/tests/unittests/ast/AssertionTests.cpp b/tests/unittests/ast/AssertionTests.cpp index de27ff3a8..170a1d7f2 100644 --- a/tests/unittests/ast/AssertionTests.cpp +++ b/tests/unittests/ast/AssertionTests.cpp @@ -2,6 +2,7 @@ // SPDX-License-Identifier: MIT #include "Test.h" +#include #include "slang/diagnostics/StatementsDiags.h" @@ -2359,171 +2360,225 @@ endmodule CHECK(diags[0].code == diag::UndeclaredIdentifier); } -TEST_CASE("Sequence nondegeneracy tests") { - auto tree = SyntaxTree::fromText(R"( -module top(); - assert property ((1'b1 ##[1:2] 1'b1) intersect (1'b1 ##[2:4] 1'b1)); // legal - - assert property ((1'b1 ##[1:2] 1'b1) intersect (1'b1 ##[3:4] 1'b1)); // illegal - - assert property ((1'b1) intersect (1'b1[*0] ##2 1'b1)); // illegal - - assert property ((1'b1 ##1 1'b1) intersect (1'b1[*0] ##2 1'b1)); // legal - - assert property ((1'b1 ##1 1'b0) intersect (1'b1[*0] ##2 1'b1)); // illegal - - assert property( (1'b1) intersect (1'b1 ##[1:3] 1'b1)); // illegal - - assert property( (1'b1 ##1 1'b1) intersect (1'b1 ##[1:3] 1'b1)); // legal - - assert property( (1'b1 ##0 1'b1) intersect (1'b1 ##[1:3] 1'b1)); // illegal - - assert property( (1'b1[*2]) intersect (1'b1 ##[1:3] 1'b1)); // illegal - - assert property( (##2 1'b1[*2]) intersect (1'b1 ##[1:3] 1'b1)); // legal -endmodule - -module top1(); +TEST_CASE("Sequence nondegeneracy tests 1") { + auto test = [](std::string_view expr, std::optional code = {}) { + auto tree = SyntaxTree::fromText(fmt::format(R"( +module top; string a; logic b; - int c,d,e; - - assert property (##0 a[*0:4] ##0 b[=4] ##0 c[->1:2] ##0 c[*] ##1 d[+]); // legal - - assert property (##0 a[*0:4] ##0 b[=4] ##0 c[->1:2] ##0 c[*0] ##1 d[+]); // illegal - - assert property (##0 a[*0] ##0 b[=4] ##0 c[->1:2] ##0 c[*] ##1 d[+]); // illegal -endmodule - -module top2(input a, input b); -property p; - !(2'b01 - 2'b01 + 3'b010 - 3'b010 + 4'b0010); // illegal -endproperty - -property pp; - 2'b01 - 2'b01 + 3'b010 - 3'b010 + 4'b0010; // legal -endproperty - -property p1; - a[*0] |-> b; // illegal -endproperty - -property pp1; - a[*1] |-> b; // legal -endproperty - -property p2; - 1'b1 ##1 b; // legal -endproperty - -assert property (p); -assert property (pp); -assert property (p1); -assert property (p2); - -endmodule - -module top3(a, b, e); + int c, d, e; + assert property ({}); +endmodule +)", + expr)); + Compilation compilation; + compilation.addSyntaxTree(tree); + + auto& diags = compilation.getAllDiagnostics(); + if (!code) { + CHECK(diags.empty()); + if (!diags.empty()) + FAIL_CHECK(expr); + } + else if (diags.size() != 1 || diags[0].code != code) { + FAIL_CHECK(expr); + CHECK(diags[0].code == *code); + } + }; + + test("(1'b1 ##[1:2] 1'b1) intersect (1'b1 ##[2:4] 1'b1)"); + test("(1'b1 ##[1:2] 1'b1) intersect (1'b1 ##[3:4] 1'b1)", diag::SeqPropNondegenerate); + test("(1'b1) intersect (1'b1[*0] ##2 1'b1)", diag::SeqPropNondegenerate); + test("(1'b1 ##1 1'b1) intersect (1'b1[*0] ##2 1'b1)"); + test("(1'b1 ##1 1'b0) intersect (1'b1[*0] ##2 1'b1)", diag::SeqPropNondegenerate); + test("(1'b1) intersect (1'b1 ##[1:3] 1'b1)", diag::SeqPropNondegenerate); + test("(1'b1 ##1 1'b1) intersect (1'b1 ##[1:3] 1'b1)"); + test("(1'b1 ##0 1'b1) intersect (1'b1 ##[1:3] 1'b1)", diag::SeqPropNondegenerate); + test("(1'b1[*2]) intersect (1'b1 ##[1:3] 1'b1)", diag::SeqPropNondegenerate); + test("(##2 1'b1[*2]) intersect (1'b1 ##[1:3] 1'b1)"); + test("##0 a[*0:4] ##0 b[=4] ##0 c[->1:2] ##0 c[*] ##1 d[+]"); + test("##0 a[*0:4] ##0 b[=4] ##0 c[->1:2] ##0 c[*0] ##1 d[+]", diag::SeqPropNondegenerate); + test("##0 a[*0] ##0 b[=4] ##0 c[->1:2] ##0 c[*] ##1 d[+]", diag::SeqPropNondegenerate); +} + +TEST_CASE("Sequence nondegeneracy tests 2") { + auto test = [](std::string_view expr, std::optional code = {}) { + auto tree = SyntaxTree::fromText(fmt::format(R"( +module top(a, b, e); input a; input b; input e; int c, d; - property p(int i, foo = 1); - ##1 c ##1 d ##1 i; // may be legal or not - depends on value of `i` - endproperty - - property p1(); - ##0 c; // legal - endproperty - - property p2(); - 1'b1 ##1 1'b0 ##0 d ##1 1'b1; // illegal - endproperty - - property p3(); - 1'b1 ##1 1'b1 ##0 d ##1 1'b1; // legal - endproperty - - property p4(); - b ##0 a[*0]; // illegal - endproperty - - property pp4(); - b ##0 a[*1]; // legal - endproperty - - property p5(); - a[*0] ##1 b; // legal - endproperty - - property p6(); - a ##1 b[*0] ##0 c; // legal - endproperty + logic clk; - property p7(); - a ##1(b[*0] ##0 c); // illegal + property p; + {}; endproperty - assert property (p (0, 0)); // illegal - assert property (p (1, 0)); // legal - assert property (p1); - assert property (p2); - assert property (p3); - assert property (p4); - assert property (pp4); - assert property (p5); - assert property (p6); - assert property (p7); + assert property (p); endmodule +)", + expr)); + Compilation compilation; + compilation.addSyntaxTree(tree); -module top4; + auto& diags = compilation.getAllDiagnostics(); + if (!code) { + CHECK(diags.empty()); + if (!diags.empty()) + FAIL_CHECK(expr); + } + else if (diags.size() != 1 || diags[0].code != code) { + FAIL_CHECK(expr); + CHECK(diags[0].code == *code); + } + }; + + test("!(2'b01 - 2'b01 + 3'b010 - 3'b010 + 4'b0010)", diag::SeqPropNondegenerate); + test("2'b01 - 2'b01 + 3'b010 - 3'b010 + 4'b0010"); + test("a[*0] |-> b", diag::OverlapImplNondegenerate); + test("a[*1] |-> b"); + test("1'b1 ##1 b"); + + test("##0 c"); + test("1'b1 ##1 1'b0 ##0 d ##1 1'b1", diag::SeqPropNondegenerate); + test("1'b1 ##1 1'b1 ##0 d ##1 1'b1"); + test("b ##0 a[*0]", diag::SeqPropNondegenerate); + test("b ##0 a[*1]"); + test("a[*0] ##1 b"); + test("a ##1 b[*0] ##0 c"); + test("a ##1(b[*0] ##0 c)", diag::SeqPropNondegenerate); + + test("(1 ##1 0)[*0]", diag::SeqPropNondegenerate); + test("(a[*0] ##1 a[*0])[*1]", diag::SeqPropNondegenerate); + test("(a[*0] ##2 a[*0])[*1]"); + test("not (a[*0] ##0 b)", diag::SeqPropNondegenerate); + test("not (a[*0] ##1 b)"); + + test("(1'b1) intersect (##[1:3] 1'b1 ##0 1'b1[*0:3] ##[2:3] 1'b1[*1])", + diag::SeqPropNondegenerate); + test("(1'b1) intersect (##[1:3] 1'b1 ##0 1'b1[*0:3] ##[2:3] 1'b1[*0])", + diag::SeqPropNondegenerate); + test("(1'b1) intersect (##[0:3] 1'b1 ##1 1'b1[*0:2] ##[2:3] 1'b1[*0])", + diag::SeqPropNondegenerate); + test("(1'b1) intersect (##[0:3] 1'b1[*0:2])"); + test("(1'b1) intersect (##[0:3] 1'b1[*0])"); + test("(1'b1) intersect (##[0:3] 1'b1)"); + test("(1'b1) intersect (1'b1[*0] ##[0:3] 1'b1)"); + test("(1'b1) intersect (1'b1[*0:2] ##[0:3] 1'b1)"); + test("(1'b1) intersect (1'b1 ##[1:3] 1'b1)", diag::SeqPropNondegenerate); + test("1'b0 ##2 1'b1", diag::SeqPropNondegenerate); + test("1[*2]"); + test("1[*0]", diag::SeqPropNondegenerate); + test("1[*0:2]", diag::SeqPropNondegenerate); + test("1'b1"); + test("1'b0", diag::SeqPropNondegenerate); + + test("1'b1 |=> 1"); + test("1'b0 |=> 1", diag::NonOverlapImplNondegenerate); + test("1[*2] |=> 1"); + test("1[*0] |=> 1"); + test("1'b1 |-> 1"); + test("1'b0 |-> 1", diag::OverlapImplNondegenerate); + test("1[*0] |-> 1", diag::OverlapImplNondegenerate); + test("1[*0:2] |-> 1"); + + test("1'b1 #=# 1"); + test("1'b0 #=# 1", diag::NonOverlapImplNondegenerate); + test("1[*2] #=# 1"); + test("1[*0] #=# 1"); + test("1'b1 #-# 1"); + test("1'b0 #-# 1", diag::OverlapImplNondegenerate); + test("1[*0] #-# 1", diag::OverlapImplNondegenerate); + test("1[*0:2] #-# 1"); + + test("first_match(a and b)"); + test("(first_match(a and b))[*0]", diag::SeqPropNondegenerate); + test("first_match(a and (b[*0] ##0 b))", diag::SeqPropNondegenerate); + test("@clk a ##1 b"); + test("@clk a[*0] ##0 b", diag::SeqPropNondegenerate); + test("strong(a ##1 b)"); + test("strong(a ##0 b[*0])", diag::SeqPropNondegenerate); + test("weak(a intersect b)"); + test("weak(a intersect ##2 b)", diag::SeqPropNondegenerate); + test("accept_on(b) sync_reject_on(c) sync_accept_on(d) reject_on(e) b ##1 c"); + test("accept_on(b) b intersect ##2 b", diag::SeqPropNondegenerate); + test("accept_on(b) ##2 b intersect ##2 b"); + test("accept_on(b) b[*0] ##0 b", diag::SeqPropNondegenerate); + + test("if (b) a ##1 c else d ##1 e"); + test("if (1'b0) a ##1 c else d ##1 e"); + test("if (1'b0) a ##1 c", diag::SeqPropNondegenerate); + test("if (1'b1) a ##1 c else d ##1 e"); + test("if (a) b intersect ##2 b", diag::SeqPropNondegenerate); + test("if (a) ##2 b intersect ##2 b"); + test("case (b) 1, 2, 3: 1 ##1 b; 4: a and b; default: 1 |-> b; endcase"); + test("case (b) 1, 2, 3: 1 ##1 b; 4: a and b; default: 1[*0] |-> b; endcase", + diag::OverlapImplNondegenerate); + test("disable iff (clk) a"); + test("disable iff (1'b1) a", diag::SeqPropNondegenerate); +} + +TEST_CASE("Sequence nondegeneracy tests 3") { + auto test = [](std::string_view expr, std::optional code = {}) { + auto tree = SyntaxTree::fromText(fmt::format(R"( +module top; sequence s(int i); int j, k = j; - (i == i, j = 1, j++)[*0:1]; // illegal - empty matches - endsequence - - sequence s1(int i); - int j, k = j; - (i != i, j = 1, j++)[*1:1]; // illegal - always `false` condition + {}; endsequence - sequence s2(int i); - int j, k = j; - (i != i, j = 1, j++)[*0:1]; // illegal - always `false` condition and empty matches - endsequence + assert property (s(1)); +endmodule +)", + expr)); + Compilation compilation; + compilation.addSyntaxTree(tree); - sequence s3(int i); - int j, k = j; - (i == i, j = 1, j++)[*1:1]; // legal - endsequence + auto& diags = compilation.getAllDiagnostics(); + if (!code) { + CHECK(diags.empty()); + if (!diags.empty()) + FAIL_CHECK(expr); + } + else if (diags.size() != 1 || diags[0].code != code) { + FAIL_CHECK(expr); + CHECK(diags[0].code == *code); + } + }; - sequence s4(int i); - int j, k = j; - (i == i, j = 1, j++)[*0:0]; // illegal - only empty matches - endsequence + test("(i == i, j = 1, j++)[*0:1]", diag::SeqPropNondegenerate); + test("(i != i, j = 1, j++)[*1:1]", diag::SeqPropNondegenerate); + test("(i != i, j = 1, j++)[*0:1]", diag::SeqPropNondegenerate); + test("(i == i, j = 1, j++)[*1:1]"); + test("(i == i, j = 1, j++)[*0:0]", diag::SeqPropNondegenerate); + test("(i == i, j = 1, j++)[*0]", diag::SeqPropNondegenerate); +} - sequence s5(int i); - int j, k = j; - (i == i, j = 1, j++)[*0]; // illegal - only empty matches - endsequence +TEST_CASE("Sequence nondegeneracy tests 4") { + auto tree = SyntaxTree::fromText(R"( +module top; + int c, d; + property p(int i, foo = 1); + ##1 c ##1 d ##1 i; // may be legal or not - depends on value of `i` + endproperty - assert property (s(1)); // illegal - assert property (s1(1)); // illegal - assert property (s2(1)); // illegal - assert property (s3(1)); // legal - assert property (s4(1)); // illegal - assert property (s5(1)); // illegal + assert property (p (0, 0)); // illegal + assert property (p (1, 0)); // legal endmodule +)"); -module top5(input a, input b); - assert property ((1 ##1 0)[*0]); // illegal - assert property ((a[*0] ##1 a[*0])[*1]); // illegal - assert property ((a[*0] ##2 a[*0])[*1]); // legal - assert property (not (a[*0] ##0 b)); // illegal - assert property (not (a[*0] ##1 b)); // legal -endmodule + Compilation compilation; + compilation.addSyntaxTree(tree); -module top6(); + auto& diags = compilation.getAllDiagnostics(); + REQUIRE(diags.size() == 1); + CHECK(diags[0].code == diag::SeqPropNondegenerate); +} + +TEST_CASE("Sequence nondegeneracy tests 5") { + auto tree = SyntaxTree::fromText(R"( +module top; logic clk, reset, a, b; assert property(@(posedge clk) disable iff (reset) a |-> {500-$bits($past(b)){1'b0}}); // illegal @@ -2534,216 +2589,12 @@ module top6(); assert property(@(posedge clk) disable iff (reset) {500 - $bits(b){1'b1}}); // legal endmodule - -module top7; - property p; - (1'b1) intersect (##[1:3] 1'b1 ##0 1'b1[*0:3] ##[2:3] 1'b1[*1]); // illegal - endproperty - - property p1; - (1'b1) intersect (##[1:3] 1'b1 ##0 1'b1[*0:3] ##[2:3] 1'b1[*0]); // illegal - endproperty - - property p2; - (1'b1) intersect (##[0:3] 1'b1 ##1 1'b1[*0:2] ##[2:3] 1'b1[*0]); // illegal - endproperty - - property p3; - (1'b1) intersect (##[0:3] 1'b1[*0:2]); // legal - endproperty - - property p4; - (1'b1) intersect (##[0:3] 1'b1[*0]); // legal - endproperty - - property p5; - (1'b1) intersect (##[0:3] 1'b1); // legal - endproperty - - property p6; - (1'b1) intersect (1'b1[*0] ##[0:3] 1'b1); // legal - endproperty - - property p7; - (1'b1) intersect (1'b1[*0:2] ##[0:3] 1'b1); // legal - endproperty - - property p8; - (1'b1) intersect (1'b1 ##[1:3] 1'b1); // illegal - endproperty - - property p9; - 1'b0 ##2 1'b1; // illegal - endproperty - - property p10; - 1[*2]; // legal - endproperty - - property p11; - 1[*0]; // illegal - endproperty - - property p12; - 1[*0:2]; // illegal - endproperty - - property p13; - 1'b1; // legal - endproperty - - property p14; - 1'b0; // illegal - endproperty - - property p15; - 1'b1 |=> 1; // legal - endproperty - - property p16; - 1'b0 |=> 1; // illegal - endproperty - - property p17; - 1[*2] |=> 1; // legal - endproperty - - property p18; - 1[*0] |=> 1; // legal - endproperty - - property p19; - 1'b1 |-> 1; // legal - endproperty - - property p20; - 1'b0 |-> 1; // illegal - endproperty - - property p21; - 1[*0] |-> 1; // illegal - endproperty - - property p22; - 1[*0:2] |-> 1; // legal - endproperty - - assert property (p); - assert property (p1); - assert property (p2); - assert property (p3); - assert property (p4); - assert property (p5); - assert property (p6); - assert property (p7); - assert property (p8); - assert property (p9); - assert property (p10); - assert property (p11); - assert property (p12); - assert property (p13); - assert property (p14); - assert property (p15); - assert property (p16); - assert property (p17); - assert property (p18); - assert property (p19); - assert property (p20); - assert property (p21); - assert property (p22); -endmodule - -module top8(input clk); - logic a, b, c, d, e; - - assert property (first_match(a and b)); // legal - - assert property ((first_match(a and b))[*0]); // illegal - - assert property (first_match(a and (b[*0] ##0 b))); // illegal - - assert property (@clk a ##1 b); // legal - - assert property (@clk a[*0] ##0 b); // illegal - - assert property(strong(a ##1 b)); // legal - - assert property(strong(a ##0 b[*0])); // illegal - - assert property(weak(a intersect b)); // legal - - assert property(weak(a intersect ##2 b)); // illegal - - assert property (accept_on(b) sync_reject_on(c) sync_accept_on(d) reject_on(e) b ##1 c); // legal - - assert property (accept_on(b) b intersect ##2 b); // illegal - - assert property (accept_on(b) ##2 b intersect ##2 b); // legal - - assert property (accept_on(b) b[*0] ##0 b); // illegal - - assert property (if (b) a ##1 c else d ##1 e); // legal - - assert property (if (1'b0) a ##1 c else d ##1 e); // legal - - assert property (if (1'b0) a ##1 c); // illegal - - assert property (if (1'b1) a ##1 c else d ##1 e); // legal - - assert property (if (a) b intersect ##2 b); // illegal - - assert property (if (a) ##2 b intersect ##2 b); // legal - - assert property (case (b) 1, 2, 3: 1 ##1 b; 4: a and b; default: 1 |-> b; endcase); // legal - - assert property (case (b) 1, 2, 3: 1 ##1 b; 4: a and b; default: 1[*0] |-> b; endcase); // illegal - - assert property (disable iff (clk) a); // legal - - assert property (disable iff (1'b1) a); // illegal - -endmodule - -module m9; - property p1; - 1'b1 #=# 1; // legal - endproperty - property p2; - 1'b0 #=# 1; // illegal - endproperty - property p3; - 1[*2] #=# 1; // legal - endproperty - property p4; - 1[*0] #=# 1; // legal - endproperty - property p5; - 1'b1 #-# 1; // legal - endproperty - property p6; - 1'b0 #-# 1; // illegal - endproperty - property p7; - 1[*0] #-# 1; // illegal - endproperty - property p8; - 1[*0:2] #-# 1; // legal - endproperty - - assert property (p1); - assert property (p2); - assert property (p3); - assert property (p4); - assert property (p5); - assert property (p6); - assert property (p7); - assert property (p8); -endmodule )"); Compilation compilation; compilation.addSyntaxTree(tree); auto& diags = compilation.getAllDiagnostics(); - REQUIRE(diags.size() == 48); + REQUIRE(diags.size() == 1); + CHECK(diags[0].code == diag::SeqPropNondegenerate); }