From 71c4be209f98ec1f5b19649a598c4a5c24bb8aab Mon Sep 17 00:00:00 2001 From: Yan <62220457+likeamahoney@users.noreply.github.com> Date: Sat, 25 May 2024 10:20:03 +0300 Subject: [PATCH] [slang][lang-compliance] Introduce nondegeneracy check (#998) Co-authored-by: Yan Churkin --- bindings/python/ASTBindings.cpp | 2 +- include/slang/ast/expressions/AssertionExpr.h | 157 +++++- scripts/diagnostics.txt | 9 +- source/ast/expressions/AssertionExpr.cpp | 482 +++++++++++++++--- source/ast/expressions/MiscExpressions.cpp | 3 +- tests/unittests/ast/AssertionTests.cpp | 399 ++++++++++++++- tests/unittests/ast/MemberTests.cpp | 2 +- 7 files changed, 967 insertions(+), 87 deletions(-) diff --git a/bindings/python/ASTBindings.cpp b/bindings/python/ASTBindings.cpp index 1ea5b80c4..e3769ca43 100644 --- a/bindings/python/ASTBindings.cpp +++ b/bindings/python/ASTBindings.cpp @@ -333,7 +333,7 @@ void registerAST(py::module_& m) { .def_readonly("kind", &AssertionExpr::kind) .def_readonly("syntax", &AssertionExpr::syntax) .def_property_readonly("bad", &AssertionExpr::bad) - .def_property_readonly("admitsEmpty", &AssertionExpr::admitsEmpty) + .def_property_readonly("checkNondegeneracy", &AssertionExpr::checkNondegeneracy) .def("__repr__", [](const AssertionExpr& self) { return fmt::format("AssertionExpr(AssertionExprKind.{})", toString(self.kind)); }); diff --git a/include/slang/ast/expressions/AssertionExpr.h b/include/slang/ast/expressions/AssertionExpr.h index f1367407e..dbd4a4a4a 100644 --- a/include/slang/ast/expressions/AssertionExpr.h +++ b/include/slang/ast/expressions/AssertionExpr.h @@ -67,6 +67,21 @@ SLANG_ENUM(BinaryAssertionOperator, OP) class ASTContext; class CallExpression; +struct SequenceRange; + +enum class NondegeneracyStatus { + None = 0, + + // Sequence admits empty matches + AdmitsEmpty = 1 << 0, + + // Sequence accepts only empty matches + AcceptsOnlyEmpty = 1 << 1, + + // Sequence admits no match + AdmitsNoMatch = 1 << 2 +}; +SLANG_BITMASK(NondegeneracyStatus, AdmitsNoMatch); /// The base class for assertion expressions (sequences and properties). class SLANG_EXPORT AssertionExpr { @@ -74,6 +89,19 @@ class SLANG_EXPORT AssertionExpr { /// 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; @@ -87,16 +115,21 @@ class SLANG_EXPORT AssertionExpr { /// Indicates whether the expression is invalid. bool bad() const { return kind == AssertionExprKind::Invalid; } - /// @returns true if this is a sequence expression that admits an empty match, - /// and false otherwise. - bool admitsEmpty() const; + // Checks that the sequence matches one of the following: + // - admits empty matches + // - accepts only empty matches + // - admits no matches + bitmask checkNondegeneracy() const; + + /// Computes possible clock ticks (delay) length of sequence under assertion expression + std::optional computeSequenceLength() const; 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, - bool allowSeqAdmitEmpty = false); + NondegeneracyFlags nondegFlags = NondegeneracyFlags::None); static const AssertionExpr& bind(const syntax::PropertySpecSyntax& syntax, const ASTContext& context); @@ -169,7 +202,11 @@ class SLANG_EXPORT InvalidAssertionExpr : public AssertionExpr { explicit InvalidAssertionExpr(const AssertionExpr* child) : AssertionExpr(AssertionExprKind::Invalid), child(child) {} - bool admitsEmptyImpl() const { return false; } + bitmask checkNondegeneracyImpl() const { + return NondegeneracyStatus::None; + } + + std::optional computeSequenceLengthImpl() const; static bool isKind(AssertionExprKind kind) { return kind == AssertionExprKind::Invalid; } @@ -190,6 +227,18 @@ struct SequenceRange { 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. @@ -221,7 +270,10 @@ struct SequenceRepetition { No, /// The sequence may or may not admit an empty match. - Depends + Depends, + + /// The sequence accepts only empty matches and nothing else. + Only, }; /// Classifies the repetition as admitting an empty match or not. @@ -239,11 +291,19 @@ class SLANG_EXPORT SimpleAssertionExpr : public AssertionExpr { /// An optional repetition of the sequence. std::optional repetition; - SimpleAssertionExpr(const Expression& expr, std::optional repetition) : - AssertionExpr(AssertionExprKind::Simple), expr(expr), repetition(repetition) {} + /// Store `true` if sequence exression can be evaluated as constant `false` (`0`). + bool isNullExpr; + + SimpleAssertionExpr(const Expression& expr, std::optional repetition, + bool isNullExpr = false) : + AssertionExpr(AssertionExprKind::Simple), expr(expr), repetition(repetition), + isNullExpr(isNullExpr) {} void requireSequence(const ASTContext& context, DiagCode code) const; - bool admitsEmptyImpl() const; + + bitmask checkNondegeneracyImpl() const; + + std::optional computeSequenceLengthImpl() const; static AssertionExpr& fromSyntax(const syntax::SimpleSequenceExprSyntax& syntax, const ASTContext& context, bool allowDisable); @@ -276,7 +336,9 @@ class SLANG_EXPORT SequenceConcatExpr : public AssertionExpr { explicit SequenceConcatExpr(std::span elements) : AssertionExpr(AssertionExprKind::SequenceConcat), elements(elements) {} - bool admitsEmptyImpl() const; + bitmask checkNondegeneracyImpl() const; + + std::optional computeSequenceLengthImpl() const; static AssertionExpr& fromSyntax(const syntax::DelayedSequenceExprSyntax& syntax, const ASTContext& context); @@ -310,7 +372,11 @@ class SLANG_EXPORT SequenceWithMatchExpr : public AssertionExpr { AssertionExpr(AssertionExprKind::SequenceWithMatch), expr(expr), repetition(repetition), matchItems(matchItems) {} - bool admitsEmptyImpl() const; + bitmask checkNondegeneracyImpl() const; + + std::optional computeSequenceLengthImpl() const { + return expr.computeSequenceLength(); + } static AssertionExpr& fromSyntax(const syntax::ParenthesizedSequenceExprSyntax& syntax, const ASTContext& context); @@ -345,7 +411,13 @@ class SLANG_EXPORT UnaryAssertionExpr : public AssertionExpr { std::optional range) : AssertionExpr(AssertionExprKind::Unary), op(op), expr(expr), range(range) {} - bool admitsEmptyImpl() const { return false; } + bitmask checkNondegeneracyImpl() const { + return expr.checkNondegeneracy(); + } + + std::optional computeSequenceLengthImpl() const { + return expr.computeSequenceLength(); + } static AssertionExpr& fromSyntax(const syntax::UnaryPropertyExprSyntax& syntax, const ASTContext& context); @@ -380,7 +452,16 @@ class SLANG_EXPORT BinaryAssertionExpr : public AssertionExpr { AssertionExpr(AssertionExprKind::Binary), op(op), left(left), right(right) {} void requireSequence(const ASTContext& context, DiagCode code) const; - bool admitsEmptyImpl() 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, const ASTContext& context); @@ -412,7 +493,11 @@ class SLANG_EXPORT FirstMatchAssertionExpr : public AssertionExpr { std::span matchItems) : AssertionExpr(AssertionExprKind::FirstMatch), seq(seq), matchItems(matchItems) {} - bool admitsEmptyImpl() const; + bitmask checkNondegeneracyImpl() const; + + std::optional computeSequenceLengthImpl() const { + return seq.computeSequenceLength(); + } static AssertionExpr& fromSyntax(const syntax::FirstMatchSequenceExprSyntax& syntax, const ASTContext& context); @@ -441,7 +526,11 @@ class SLANG_EXPORT ClockingAssertionExpr : public AssertionExpr { ClockingAssertionExpr(const TimingControl& clocking, const AssertionExpr& expr) : AssertionExpr(AssertionExprKind::Clocking), clocking(clocking), expr(expr) {} - bool admitsEmptyImpl() const; + bitmask checkNondegeneracyImpl() const; + + std::optional computeSequenceLengthImpl() const { + return expr.computeSequenceLength(); + } static AssertionExpr& fromSyntax(const syntax::ClockingSequenceExprSyntax& syntax, const ASTContext& context); @@ -478,7 +567,13 @@ class SLANG_EXPORT StrongWeakAssertionExpr : public AssertionExpr { StrongWeakAssertionExpr(const AssertionExpr& expr, Strength strength) : AssertionExpr(AssertionExprKind::StrongWeak), expr(expr), strength(strength) {} - bool admitsEmptyImpl() const { return false; } + bitmask checkNondegeneracyImpl() const { + return expr.checkNondegeneracy(); + } + + std::optional computeSequenceLengthImpl() const { + return expr.computeSequenceLength(); + } static AssertionExpr& fromSyntax(const syntax::StrongWeakPropertyExprSyntax& syntax, const ASTContext& context); @@ -513,7 +608,13 @@ class SLANG_EXPORT AbortAssertionExpr : public AssertionExpr { AssertionExpr(AssertionExprKind::Abort), condition(condition), expr(expr), action(action), isSync(isSync) {} - bool admitsEmptyImpl() const { return false; } + bitmask checkNondegeneracyImpl() const { + return expr.checkNondegeneracy(); + } + + std::optional computeSequenceLengthImpl() const { + return expr.computeSequenceLength(); + } static AssertionExpr& fromSyntax(const syntax::AcceptOnPropertyExprSyntax& syntax, const ASTContext& context); @@ -546,7 +647,12 @@ class SLANG_EXPORT ConditionalAssertionExpr : public AssertionExpr { AssertionExpr(AssertionExprKind::Conditional), condition(condition), ifExpr(ifExpr), elseExpr(elseExpr) {} - bool admitsEmptyImpl() const { return false; } + bitmask checkNondegeneracyImpl() const { + 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, const ASTContext& context); @@ -590,7 +696,13 @@ class SLANG_EXPORT CaseAssertionExpr : public AssertionExpr { AssertionExpr(AssertionExprKind::Case), expr(expr), items(items), defaultCase(defaultCase) { } - bool admitsEmptyImpl() const { return false; } + bitmask checkNondegeneracyImpl() const { + 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, const ASTContext& context); @@ -625,7 +737,12 @@ class SLANG_EXPORT DisableIffAssertionExpr : public AssertionExpr { DisableIffAssertionExpr(const Expression& condition, const AssertionExpr& expr) : AssertionExpr(AssertionExprKind::DisableIff), condition(condition), expr(expr) {} - bool admitsEmptyImpl() const { return false; } + bitmask checkNondegeneracyImpl() const { + return NondegeneracyStatus::None; + } + + /// Returns `nullopt` if `disable iff` condition is always `true` (`1`) + std::optional computeSequenceLengthImpl() const; static AssertionExpr& fromSyntax(const syntax::DisableIffSyntax& syntax, const AssertionExpr& expr, const ASTContext& context); diff --git a/scripts/diagnostics.txt b/scripts/diagnostics.txt index 6c9f6688a..589ab0cf2 100644 --- a/scripts/diagnostics.txt +++ b/scripts/diagnostics.txt @@ -840,7 +840,9 @@ error DisableIffLocalVar "local variables cannot be used in disable iff conditio error DisableIffMatched "'matched' method cannot be used in disable iff conditions" error PropAbortLocalVar "local variables cannot be used in property abort conditions" error PropAbortMatched "'matched' method cannot be used in property abort conditions" -error SeqPropAdmitEmpty "sequence properties cannot admit an empty match" +error SeqPropNondegenerate "any sequence that is used as a property shall be nondegenerate and shall not admit any empty match" +error OverlapImplNondegenerate "any sequence that is used as the antecedent of an overlapping implication (|->) shall be nondegenerate" +error NonOverlapImplNondegenerate "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" error RecursivePropDisableIff "recursive properties cannot have disable iff conditions" error ConcurrentAssertActionBlock "cannot have '{}' statement in the action block of another concurrent assertion" error InvalidForStepExpression "for loop step expression must be an assignment, increment/decrement operator, or a subroutine call" @@ -856,6 +858,11 @@ warning bad-procedural-force BadProceduralForce "lvalue of force/release must be warning multibit-edge MultiBitEdge "edge of expression of type {} will only trigger on changes to the first bit" note NoteWhileExpanding "while expanding {} '{}'" note NoteExpandedHere "expanded here" +note SeqAdmitsEmptyMatches "sequence property admits empty matches" +note SeqAdmitsNoMatches "sequence property can never be matched" +note SeqAcceptsOnlyEmptyMatches "sequence property admits only empty matches" +note SeqPropCondAlwaysFalse "condition is always false" +note DisableIffCondAlwaysTrue "disable iff condition is always true" subsystem Types error InvalidEnumBase "invalid enum base type {} (must be a single dimensional integer type)" diff --git a/source/ast/expressions/AssertionExpr.cpp b/source/ast/expressions/AssertionExpr.cpp index b421a37f4..3573900c1 100644 --- a/source/ast/expressions/AssertionExpr.cpp +++ b/source/ast/expressions/AssertionExpr.cpp @@ -26,13 +26,23 @@ namespace { using namespace slang::ast; -struct AdmitsEmptyVisitor { +struct NondegeneracyCheckVisitor { template - bool visit(const T& expr) { + slang::bitmask visit(const T& expr) { if (expr.bad()) - return false; + return NondegeneracyStatus::None; + + return expr.checkNondegeneracyImpl(); + } +}; - return expr.admitsEmptyImpl(); +struct SequenceLengthVisitor { + template + std::optional visit(const T& expr) { + if (expr.bad()) + return std::nullopt; + + return expr.computeSequenceLengthImpl(); } }; @@ -111,7 +121,7 @@ const AssertionExpr& AssertionExpr::bind(const SequenceExprSyntax& syntax, const AssertionExpr& AssertionExpr::bind(const PropertyExprSyntax& syntax, const ASTContext& context, bool allowDisable, - bool allowSeqAdmitEmpty) { + NondegeneracyFlags nondegFlags) { ASTContext ctx(context); ctx.flags |= ASTFlags::AssignmentDisallowed; @@ -121,8 +131,40 @@ const AssertionExpr& AssertionExpr::bind(const PropertyExprSyntax& syntax, // Just a simple passthrough to creating the sequence expression // contained within. auto& seq = bind(*syntax.as().expr, ctx, allowDisable); - if (!allowSeqAdmitEmpty && seq.admitsEmpty()) - context.addDiag(diag::SeqPropAdmitEmpty, syntax.sourceRange()); + 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()); + } return seq; } @@ -243,8 +285,13 @@ void AssertionExpr::requireSequence(const ASTContext& context, DiagCode code) co SLANG_UNREACHABLE; } -bool AssertionExpr::admitsEmpty() const { - AdmitsEmptyVisitor visitor; +bitmask AssertionExpr::checkNondegeneracy() const { + NondegeneracyCheckVisitor visitor; + return visit(visitor); +} + +std::optional AssertionExpr::computeSequenceLength() const { + SequenceLengthVisitor visitor; return visit(visitor); } @@ -357,6 +404,10 @@ 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); @@ -417,6 +468,47 @@ void SequenceRange::serializeTo(ASTSerializer& serializer) const { serializer.write("max", "$"sv); } +bool SequenceRange::operator<(const SequenceRange& right) const { + // if both sequences are unbounded then check min's + 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; + + // return `false` otherwise (in case is right sequence if bounded) + return false; +} + +bool SequenceRange::isIntersect(const SequenceRange& other) const { + if (!max.has_value()) + return (other.max.has_value()) ? (min >= other.min && min <= other.max.value()) + : min == other.min; + + if (!other.max.has_value()) + return (max.has_value()) ? (other.min >= min && other.min <= max.value()) + : other.min == min; + + 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.max) + : (min >= other.min && min <= other.max); +} + SequenceRepetition::SequenceRepetition(const SequenceRepetitionSyntax& syntax, const ASTContext& context) { switch (syntax.op.kind) { @@ -441,6 +533,11 @@ SequenceRepetition::SequenceRepetition(const SequenceRepetitionSyntax& syntax, } 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) @@ -507,7 +604,9 @@ AssertionExpr& SimpleAssertionExpr::fromSyntax(const SimpleSequenceExprSyntax& s } } - return *comp.emplace(expr, repetition); + const auto evaluatedValue = context.tryEval(expr); + return *comp.emplace( + expr, repetition, (evaluatedValue.isInteger() && !evaluatedValue.isTrue())); } void SimpleAssertionExpr::requireSequence(const ASTContext& context, DiagCode code) const { @@ -523,22 +622,44 @@ void SimpleAssertionExpr::requireSequence(const ASTContext& context, DiagCode co } } -bool SimpleAssertionExpr::admitsEmptyImpl() const { +bitmask SimpleAssertionExpr::checkNondegeneracyImpl() const { + bitmask res = NondegeneracyStatus::None; + + // 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 result = repetition->admitsEmpty(); - if (result == SequenceRepetition::AdmitsEmpty::Yes) - return true; - if (result == SequenceRepetition::AdmitsEmpty::No) - return false; + auto repEmptyStatus = repetition->admitsEmpty(); + if (repEmptyStatus == SequenceRepetition::AdmitsEmpty::Yes) + res |= NondegeneracyStatus::AdmitsEmpty; + if (repEmptyStatus == SequenceRepetition::AdmitsEmpty::Only) + res |= (NondegeneracyStatus::AcceptsOnlyEmpty | NondegeneracyStatus::AdmitsEmpty); } if (expr.kind == ExpressionKind::AssertionInstance) { auto& aie = expr.as(); if (aie.type->isSequenceType()) - return aie.body.admitsEmpty(); + res |= aie.body.checkNondegeneracy(); } + return res; +} - return false; +std::optional SimpleAssertionExpr::computeSequenceLengthImpl() const { + 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.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())) + return aieSeqLength.value(); + } + } + return res; } void SimpleAssertionExpr::serializeTo(ASTSerializer& serializer) const { @@ -594,26 +715,92 @@ AssertionExpr& SequenceConcatExpr::fromSyntax(const DelayedSequenceExprSyntax& s return *result; } -bool SequenceConcatExpr::admitsEmptyImpl() const { - auto it = elements.begin(); - SLANG_ASSERT(it != elements.end()); +bitmask SequenceConcatExpr::checkNondegeneracyImpl() const { + bool admitsEmpty = true; + bool admitsNoMatch = false; + auto left = elements.begin(); + SLANG_ASSERT(left != elements.end()); + auto leftNondegenSt = left->sequence->checkNondegeneracy(); - // See F.3.4.2.2 for the rules here. - if (it->delay.min != 0 || !it->sequence->admitsEmpty()) - return false; + if (left->delay.min != 0 || !leftNondegenSt.has(NondegeneracyStatus::AdmitsEmpty)) + admitsEmpty = false; - while (++it != elements.end()) { - if (!it->sequence->admitsEmpty()) - return false; + if (leftNondegenSt.has(NondegeneracyStatus::AdmitsNoMatch)) + admitsNoMatch = true; - if (it->delay.min == 0u && it->delay.max == 0u) - return false; + // 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()) + break; - if (it->delay.min > 1) - return false; + 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()) { + 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)) + admitsNoMatch = true; + + // (seq ##0 empty) does not result in a match. + if (rightNondegenSt.has(NondegeneracyStatus::AcceptsOnlyEmpty)) + admitsNoMatch = true; + } + + if (right->delay.min > 1) + admitsEmpty = false; + + ++left; + leftNondegenSt = rightNondegenSt; } - return true; + bitmask res; + res = (admitsEmpty) ? res | NondegeneracyStatus::AdmitsEmpty : res; + res = (admitsNoMatch) ? res | NondegeneracyStatus::AdmitsNoMatch : res; + return res; +} + +std::optional SequenceConcatExpr::computeSequenceLengthImpl() const { + auto it = elements.begin(); + SLANG_ASSERT(it != elements.end()); + + // 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; + + 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 + // ((##(n-1) `true) ; (seq ##(n-1) `true)) + 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); + } + + ++it; + if (it != elements.end()) + isAcceptsOnlyEmpty = it->sequence->checkNondegeneracy().has( + NondegeneracyStatus::AcceptsOnlyEmpty); + } + + SequenceRange res; + res.min = delayMin; + res.max = delayMax; + return res; } void SequenceConcatExpr::serializeTo(ASTSerializer& serializer) const { @@ -695,7 +882,7 @@ static std::span bindMatchItems(const SequenceMatchList } } - if (sequence.admitsEmpty()) { + if (sequence.checkNondegeneracy().has(NondegeneracyStatus::AdmitsEmpty)) { auto& diag = context.addDiag(diag::MatchItemsAdmitEmpty, syntax.items.sourceRange()); if (sequence.syntax) diag << sequence.syntax->sourceRange(); @@ -723,10 +910,19 @@ AssertionExpr& SequenceWithMatchExpr::fromSyntax(const ParenthesizedSequenceExpr return *context.getCompilation().emplace(expr, repetition, matchItems); } -bool SequenceWithMatchExpr::admitsEmptyImpl() const { - if (repetition && repetition->admitsEmpty() == SequenceRepetition::AdmitsEmpty::Yes) - return true; - return false; +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; + } + + return res | expr.checkNondegeneracy(); } void SequenceWithMatchExpr::serializeTo(ASTSerializer& serializer) const { @@ -866,11 +1062,18 @@ AssertionExpr& BinaryAssertionExpr::fromSyntax(const BinarySequenceExprSyntax& s AssertionExpr& BinaryAssertionExpr::fromSyntax(const BinaryPropertyExprSyntax& syntax, const ASTContext& context) { - bool allowSeqAdmitEmpty = syntax.kind == SyntaxKind::ImplicationPropertyExpr || - syntax.kind == SyntaxKind::FollowedByPropertyExpr; + // 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); bitmask lflags, rflags; - if (syntax.op.kind == TokenKind::OrEqualsArrow || syntax.op.kind == TokenKind::HashEqualsHash) { + if (isNonOverlapImplOrHashEq) { rflags = ASTFlags::PropertyTimeAdvance; } else if (syntax.kind == SyntaxKind::SUntilPropertyExpr || @@ -878,8 +1081,14 @@ AssertionExpr& BinaryAssertionExpr::fromSyntax(const BinaryPropertyExprSyntax& s lflags = rflags = ASTFlags::PropertyNegation; } + NondegeneracyFlags nondegFlags = (isOverlapImplOrHashMinus) + ? NondegeneracyFlags::IsOverlapImplOrHashMinus + : NondegeneracyFlags::None; + nondegFlags = (isNonOverlapImplOrHashEq) ? NondegeneracyFlags::IsNonOverlapImplOrHashEq + : nondegFlags; + auto& comp = context.getCompilation(); - auto& left = bind(*syntax.left, context.resetFlags(lflags), false, allowSeqAdmitEmpty); + auto& left = bind(*syntax.left, context.resetFlags(lflags), false, nondegFlags); auto& right = bind(*syntax.right, context.resetFlags(rflags)); // clang-format off @@ -939,19 +1148,99 @@ void BinaryAssertionExpr::requireSequence(const ASTContext& context, DiagCode co SLANG_UNREACHABLE; } -bool BinaryAssertionExpr::admitsEmptyImpl() const { +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); + switch (op) { - case BinaryAssertionOperator::Or: - return left.admitsEmpty() || right.admitsEmpty(); - case BinaryAssertionOperator::And: - case BinaryAssertionOperator::Intersect: - case BinaryAssertionOperator::Within: - return left.admitsEmpty() && right.admitsEmpty(); - case BinaryAssertionOperator::Throughout: - return right.admitsEmpty(); + case BinaryAssertionOperator::Or: { + res = (leftAdmitsEmpty || rightAdmitsEmpty) ? res | NondegeneracyStatus::AdmitsEmpty + : res; + + // 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; + break; + } + case BinaryAssertionOperator::And: { + res = (leftAdmitsEmpty && rightAdmitsEmpty) ? res | NondegeneracyStatus::AdmitsEmpty + : res; + + // 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; + break; + } + case BinaryAssertionOperator::Intersect: { + res = (leftAdmitsEmpty && rightAdmitsEmpty) ? res | NondegeneracyStatus::AdmitsEmpty + : res; + + 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; + break; + } + case BinaryAssertionOperator::Within: { + res = (leftAdmitsEmpty && rightAdmitsEmpty) ? res | NondegeneracyStatus::AdmitsEmpty + : res; + + 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; + break; + } + case BinaryAssertionOperator::Throughout: { + res = (rightAdmitsEmpty) ? res | NondegeneracyStatus::AdmitsEmpty : res; + + // In case of `throughout` full sequence is no match if right part is no match + res = (rightAdmitsNoMatch) ? res | NondegeneracyStatus::AdmitsNoMatch : res; + break; + } default: - return false; + break; + } + + return res; +}; + +std::optional BinaryAssertionExpr::computeSequenceLengthImpl() const { + if (op == BinaryAssertionOperator::Throughout) + return right.computeSequenceLength(); + + const auto leftLen = left.computeSequenceLength(); + const auto rightLen = right.computeSequenceLength(); + if (leftLen.has_value() && rightLen.has_value()) { + const auto leftLenVal = leftLen.value(); + const auto rightLenVal = rightLen.value(); + return (rightLenVal < leftLenVal) ? leftLenVal : rightLenVal; + } + else if (leftLen.has_value()) { + return leftLen.value(); } + else if (rightLen.has_value()) { + return rightLen.value(); + } + + return std::nullopt; } void BinaryAssertionExpr::serializeTo(ASTSerializer& serializer) const { @@ -973,11 +1262,15 @@ AssertionExpr& FirstMatchAssertionExpr::fromSyntax(const FirstMatchSequenceExprS return *comp.emplace(seq, matchItems); } -bool FirstMatchAssertionExpr::admitsEmptyImpl() const { - if (!matchItems.empty()) - return false; +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; + } - return seq.admitsEmpty(); + return res; } void FirstMatchAssertionExpr::serializeTo(ASTSerializer& serializer) const { @@ -1037,8 +1330,8 @@ AssertionExpr& ClockingAssertionExpr::fromSyntax(const TimingControlSyntax& synt return *comp.emplace(clocking, expr); } -bool ClockingAssertionExpr::admitsEmptyImpl() const { - return expr.admitsEmpty(); +bitmask ClockingAssertionExpr::checkNondegeneracyImpl() const { + return expr.checkNondegeneracy(); } void ClockingAssertionExpr::serializeTo(ASTSerializer& serializer) const { @@ -1052,8 +1345,16 @@ AssertionExpr& StrongWeakAssertionExpr::fromSyntax(const StrongWeakPropertyExprS auto& expr = bind(*syntax.expr, context); expr.requireSequence(context); - if (expr.admitsEmpty()) - context.addDiag(diag::SeqPropAdmitEmpty, syntax.expr->sourceRange()); + // 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()); + } return *comp.emplace( expr, syntax.keyword.kind == TokenKind::StrongKeyword ? Strong : Weak); @@ -1105,6 +1406,24 @@ void AbortAssertionExpr::serializeTo(ASTSerializer& serializer) const { serializer.write("isSync", isSync); } +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()) + max = ifLen.value(); + + if (elseExpr) { + if (const auto elseLen = elseExpr->computeSequenceLength(); elseLen.has_value()) { + if (const auto elseLenVal = elseLen.value(); !max.has_value() || max < elseLenVal) + max = elseLenVal; + } + } + + return max; +} + AssertionExpr& ConditionalAssertionExpr::fromSyntax(const ConditionalPropertyExprSyntax& syntax, const ASTContext& context) { auto& comp = context.getCompilation(); @@ -1115,6 +1434,16 @@ 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 (!elseExpr) { + if (const auto evaluatedValue = context.tryEval(cond); + evaluatedValue.isInteger() && !evaluatedValue.isTrue()) { + auto& diag = context.addDiag(diag::SeqPropNondegenerate, syntax.sourceRange()); + diag.addNote(diag::SeqPropCondAlwaysFalse, cond.sourceRange); + } + } + return *comp.emplace(cond, ifExpr, elseExpr); } @@ -1125,6 +1454,27 @@ void ConditionalAssertionExpr::serializeTo(ASTSerializer& serializer) const { serializer.write("else", *elseExpr); } +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 itemLenVal = itemLen.value(); !max.has_value() || max < itemLenVal) + max = itemLenVal; + } + } + + if (defaultCase) { + if (const auto defaultItemLen = defaultCase->computeSequenceLength(); + defaultItemLen.has_value()) { + if (const auto defaultItemLenVal = defaultItemLen.value(); + !max.has_value() || max < defaultItemLenVal) + max = defaultItemLenVal; + } + } + + return max; +}; + AssertionExpr& CaseAssertionExpr::fromSyntax(const CasePropertyExprSyntax& syntax, const ASTContext& context) { auto& comp = context.getCompilation(); @@ -1178,6 +1528,13 @@ void CaseAssertionExpr::serializeTo(ASTSerializer& serializer) const { serializer.write("defaultCase", *defaultCase); } +std::optional DisableIffAssertionExpr::computeSequenceLengthImpl() const { + if (condition.constant && condition.constant->isTrue()) + return std::nullopt; + + return expr.computeSequenceLength(); +} + AssertionExpr& DisableIffAssertionExpr::fromSyntax(const DisableIffSyntax& syntax, const AssertionExpr& expr, const ASTContext& context) { @@ -1186,6 +1543,13 @@ 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 (context.tryEval(cond).isTrue()) { + auto& diag = context.addDiag(diag::SeqPropNondegenerate, syntax.sourceRange()); + diag.addNote(diag::DisableIffCondAlwaysTrue, cond.sourceRange); + } + if (context.assertionInstance && context.assertionInstance->isRecursive) context.addDiag(diag::RecursivePropDisableIff, syntax.sourceRange()); diff --git a/source/ast/expressions/MiscExpressions.cpp b/source/ast/expressions/MiscExpressions.cpp index 1bb753a52..073c54b2f 100644 --- a/source/ast/expressions/MiscExpressions.cpp +++ b/source/ast/expressions/MiscExpressions.cpp @@ -762,7 +762,8 @@ static const AssertionExpr& bindAssertionBody(const Symbol& symbol, const Syntax auto& result = AssertionExpr::bind(*sds.seqExpr, context); result.requireSequence(context); - if (outputLocalVarArgLoc && result.admitsEmpty()) { + if (outputLocalVarArgLoc && + result.checkNondegeneracy().has(NondegeneracyStatus::AdmitsEmpty)) { auto& diag = context.addDiag(diag::LocalVarOutputEmptyMatch, sds.seqExpr->sourceRange()); diag << symbol.name; diff --git a/tests/unittests/ast/AssertionTests.cpp b/tests/unittests/ast/AssertionTests.cpp index 3166fad97..de27ff3a8 100644 --- a/tests/unittests/ast/AssertionTests.cpp +++ b/tests/unittests/ast/AssertionTests.cpp @@ -3,6 +3,8 @@ #include "Test.h" +#include "slang/diagnostics/StatementsDiags.h" + TEST_CASE("Named sequences") { auto tree = SyntaxTree::fromText(R"( module m; @@ -52,7 +54,7 @@ module m; foo: assert property (a); assert property (a ##1 b ##[+] c ##[*] d ##[1:5] e); - assert property (##0 a[*0:4] ##0 b[=4] ##0 c[->1:2] ##0 c[*] ##1 d[+]); + assert property (##0 a[*1:4] ##0 b[=4] ##0 c[->1:2] ##0 c[*] ##1 d[+]); assert property (##[1:$] a[*0:$]); assert property ((a ##0 b) and (c or d)); assert property ((a ##0 b) and (c or d)); @@ -1048,8 +1050,8 @@ endmodule auto& diags = compilation.getAllDiagnostics(); REQUIRE(diags.size() == 2); - CHECK(diags[0].code == diag::SeqPropAdmitEmpty); - CHECK(diags[1].code == diag::SeqPropAdmitEmpty); + CHECK(diags[0].code == diag::SeqPropNondegenerate); + CHECK(diags[1].code == diag::SeqPropNondegenerate); } TEST_CASE("Illegal property recursion cases") { @@ -1191,7 +1193,7 @@ TEST_CASE("$past in $bits regress GH #509") { module top; logic clk, reset, a, b, c; assert property(@(posedge clk) disable iff (reset) - a |-> {500-$bits($past(b)){1'b0}}); + a |-> {500-$bits($past(b)){1'b1}}); endmodule )"); @@ -2356,3 +2358,392 @@ endmodule REQUIRE(diags.size() == 1); 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(); + 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); + 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 + + property p7(); + a ##1(b[*0] ##0 c); // illegal + 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); +endmodule + +module top4; + 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 + + sequence s3(int i); + int j, k = j; + (i == i, j = 1, j++)[*1:1]; // legal + endsequence + + sequence s4(int i); + int j, k = j; + (i == i, j = 1, j++)[*0:0]; // illegal - only empty matches + endsequence + + sequence s5(int i); + int j, k = j; + (i == i, j = 1, j++)[*0]; // illegal - only empty matches + endsequence + + 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 +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 + +module top6(); + logic clk, reset, a, b; + assert property(@(posedge clk) disable iff (reset) + a |-> {500-$bits($past(b)){1'b0}}); // illegal + + assert property(@(posedge clk) disable iff (reset) + {3 - 2{3'b111}}); // legal + + 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); +} diff --git a/tests/unittests/ast/MemberTests.cpp b/tests/unittests/ast/MemberTests.cpp index 888f9a5de..1ae6f2176 100644 --- a/tests/unittests/ast/MemberTests.cpp +++ b/tests/unittests/ast/MemberTests.cpp @@ -2265,7 +2265,7 @@ property myprop(k); endproperty genvar k; -for (k=0; k < 4; k++) begin: m +for (k=1; k < 4; k++) begin: m if (A) label1: assert property(myprop(k)); else