Skip to content

Commit

Permalink
[slang][lang-compliance] Introduce nondegeneracy check (#998)
Browse files Browse the repository at this point in the history 
Co-authored-by: Yan Churkin <yan@ispras.ru>
  • Loading branch information
@likeamahoney
likeamahoney and Yan Churkin committed May 25, 2024
1 parent 64ba9b0 commit 71c4be2
Show file tree
Hide file tree
Showing 7 changed files with 967 additions and 87 deletions.
2 changes: 1 addition & 1 deletion bindings/python/ASTBindings.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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));
});
Expand Down
157 changes: 137 additions & 20 deletions include/slang/ast/expressions/AssertionExpr.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,13 +67,41 @@ 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 {
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;
Expand All @@ -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<NondegeneracyStatus> checkNondegeneracy() const;

/// Computes possible clock ticks (delay) length of sequence under assertion expression
std::optional<SequenceRange> 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);
Expand Down Expand Up @@ -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<NondegeneracyStatus> checkNondegeneracyImpl() const {
return NondegeneracyStatus::None;
}

std::optional<SequenceRange> computeSequenceLengthImpl() const;

static bool isKind(AssertionExprKind kind) { return kind == AssertionExprKind::Invalid; }

Expand All @@ -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.
Expand Down Expand Up @@ -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.
Expand All @@ -239,11 +291,19 @@ class SLANG_EXPORT SimpleAssertionExpr : public AssertionExpr {
/// An optional repetition of the sequence.
std::optional<SequenceRepetition> repetition;

SimpleAssertionExpr(const Expression& expr, std::optional<SequenceRepetition> 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<SequenceRepetition> 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<NondegeneracyStatus> checkNondegeneracyImpl() const;

std::optional<SequenceRange> computeSequenceLengthImpl() const;

static AssertionExpr& fromSyntax(const syntax::SimpleSequenceExprSyntax& syntax,
const ASTContext& context, bool allowDisable);
Expand Down Expand Up @@ -276,7 +336,9 @@ class SLANG_EXPORT SequenceConcatExpr : public AssertionExpr {
explicit SequenceConcatExpr(std::span<const Element> elements) :
AssertionExpr(AssertionExprKind::SequenceConcat), elements(elements) {}

bool admitsEmptyImpl() const;
bitmask<NondegeneracyStatus> checkNondegeneracyImpl() const;

std::optional<SequenceRange> computeSequenceLengthImpl() const;

static AssertionExpr& fromSyntax(const syntax::DelayedSequenceExprSyntax& syntax,
const ASTContext& context);
Expand Down Expand Up @@ -310,7 +372,11 @@ class SLANG_EXPORT SequenceWithMatchExpr : public AssertionExpr {
AssertionExpr(AssertionExprKind::SequenceWithMatch), expr(expr), repetition(repetition),
matchItems(matchItems) {}

bool admitsEmptyImpl() const;
bitmask<NondegeneracyStatus> checkNondegeneracyImpl() const;

std::optional<SequenceRange> computeSequenceLengthImpl() const {
return expr.computeSequenceLength();
}

static AssertionExpr& fromSyntax(const syntax::ParenthesizedSequenceExprSyntax& syntax,
const ASTContext& context);
Expand Down Expand Up @@ -345,7 +411,13 @@ class SLANG_EXPORT UnaryAssertionExpr : public AssertionExpr {
std::optional<SequenceRange> range) :
AssertionExpr(AssertionExprKind::Unary), op(op), expr(expr), range(range) {}

bool admitsEmptyImpl() const { return false; }
bitmask<NondegeneracyStatus> checkNondegeneracyImpl() const {
return expr.checkNondegeneracy();
}

std::optional<SequenceRange> computeSequenceLengthImpl() const {
return expr.computeSequenceLength();
}

static AssertionExpr& fromSyntax(const syntax::UnaryPropertyExprSyntax& syntax,
const ASTContext& context);
Expand Down Expand Up @@ -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<NondegeneracyStatus> 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<SequenceRange> computeSequenceLengthImpl() const;

static AssertionExpr& fromSyntax(const syntax::BinarySequenceExprSyntax& syntax,
const ASTContext& context);
Expand Down Expand Up @@ -412,7 +493,11 @@ class SLANG_EXPORT FirstMatchAssertionExpr : public AssertionExpr {
std::span<const Expression* const> matchItems) :
AssertionExpr(AssertionExprKind::FirstMatch), seq(seq), matchItems(matchItems) {}

bool admitsEmptyImpl() const;
bitmask<NondegeneracyStatus> checkNondegeneracyImpl() const;

std::optional<SequenceRange> computeSequenceLengthImpl() const {
return seq.computeSequenceLength();
}

static AssertionExpr& fromSyntax(const syntax::FirstMatchSequenceExprSyntax& syntax,
const ASTContext& context);
Expand Down Expand Up @@ -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<NondegeneracyStatus> checkNondegeneracyImpl() const;

std::optional<SequenceRange> computeSequenceLengthImpl() const {
return expr.computeSequenceLength();
}

static AssertionExpr& fromSyntax(const syntax::ClockingSequenceExprSyntax& syntax,
const ASTContext& context);
Expand Down Expand Up @@ -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<NondegeneracyStatus> checkNondegeneracyImpl() const {
return expr.checkNondegeneracy();
}

std::optional<SequenceRange> computeSequenceLengthImpl() const {
return expr.computeSequenceLength();
}

static AssertionExpr& fromSyntax(const syntax::StrongWeakPropertyExprSyntax& syntax,
const ASTContext& context);
Expand Down Expand Up @@ -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<NondegeneracyStatus> checkNondegeneracyImpl() const {
return expr.checkNondegeneracy();
}

std::optional<SequenceRange> computeSequenceLengthImpl() const {
return expr.computeSequenceLength();
}

static AssertionExpr& fromSyntax(const syntax::AcceptOnPropertyExprSyntax& syntax,
const ASTContext& context);
Expand Down Expand Up @@ -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<NondegeneracyStatus> checkNondegeneracyImpl() const {
return NondegeneracyStatus::None;
}

/// Returns maximum possible sequence length beetween `if` and `else` sequence expressions.
std::optional<SequenceRange> computeSequenceLengthImpl() const;

static AssertionExpr& fromSyntax(const syntax::ConditionalPropertyExprSyntax& syntax,
const ASTContext& context);
Expand Down Expand Up @@ -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<NondegeneracyStatus> checkNondegeneracyImpl() const {
return NondegeneracyStatus::None;
}

/// Returns maximum possible sequence length beetween all case labels sequence expressions
/// include `default` label
std::optional<SequenceRange> computeSequenceLengthImpl() const;

static AssertionExpr& fromSyntax(const syntax::CasePropertyExprSyntax& syntax,
const ASTContext& context);
Expand Down Expand Up @@ -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<NondegeneracyStatus> checkNondegeneracyImpl() const {
return NondegeneracyStatus::None;
}

/// Returns `nullopt` if `disable iff` condition is always `true` (`1`)
std::optional<SequenceRange> computeSequenceLengthImpl() const;

static AssertionExpr& fromSyntax(const syntax::DisableIffSyntax& syntax,
const AssertionExpr& expr, const ASTContext& context);
Expand Down
9 changes: 8 additions & 1 deletion scripts/diagnostics.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand All @@ -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)"
Expand Down
Loading

0 comments on commit 71c4be2

Please sign in to comment.