[slang][lang-compliance] Introduce nondegeneracy check #998

likeamahoney · 2024-05-17T15:08:24Z

Based on 16.12.22 SystemVerilog LRM section and partially (F.4.3/F.5.2/F.5.5).

Also Ben Cohen's paper about nondegeneracy understanding from here.

Complex sequences are not often used in industrial/open source designs, but I think these checks will help to verify restrictions from 16.12.22 in most cases.

I written about ~300 lines of sv tests but i need help with more complex test cases but if anyone could also come up with more complex tests to test heuristics, that would be nice.

codecov · 2024-05-17T15:28:02Z

Codecov Report

Attention: Patch coverage is 74.46043% with 71 lines in your changes are missing coverage. Please review.

Project coverage is 94.14%. Comparing base (b1354ad) to head (a4b2714).

Additional details and impacted files

@@            Coverage Diff             @@
##           master     #998      +/-   ##
==========================================
- Coverage   94.24%   94.14%   -0.10%     
==========================================
  Files         191      191              
  Lines       47344    47568     +224     
==========================================
+ Hits        44618    44785     +167     
- Misses       2726     2783      +57

Files	Coverage Δ
source/ast/expressions/MiscExpressions.cpp	`94.11% <100.00%> (+<0.01%)`	⬆️
include/slang/ast/expressions/AssertionExpr.h	`55.65% <22.58%> (-7.79%)`	⬇️
source/ast/expressions/AssertionExpr.cpp	`87.45% <80.81%> (-2.75%)`	⬇️

... and 2 files with indirect coverage changes

Continue to review full report in Codecov by Sentry.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update b1354ad...a4b2714. Read the comment docs.

MikePopoloski · 2024-05-18T10:49:42Z

Thank you for tackling this; the sections of the LRM that address this are daunting which is why I had not implemented it yet. I'll have to review this quite closely.

One thing that can help inform additional tests is looking at the coverage report, which shows some big chunks that haven't been tested at all yet.

MikePopoloski · 2024-05-19T13:02:48Z

include/slang/ast/expressions/AssertionExpr.h

@@ -91,12 +96,22 @@ class SLANG_EXPORT AssertionExpr {
    /// and false otherwise.
    bool admitsEmpty() const;

+    bool isAdmitsOnlyEmpty() const { return admitsOnlyEmpty; }


Can you rework these three functions into a single one that returns the admits empty / no-match properties via a single flags enum? You can move the AdmitsEmpty enum up here and expand it to include a bit for the no-match part as well. Then you won't need the clunky extra admitsOnlyEmpty member below that is only validly set when you call admitsEmpty first, which seems like a footgun.

Thanks for suggestion, fixed)!

MikePopoloski · 2024-05-19T13:03:50Z

include/slang/ast/expressions/AssertionExpr.h

+
+    bool operator==(const SequenceRange& right) const;
+
+    bool operator>(const SequenceRange& right) const;


You can instead implement all of the comparison operators by implementing the "spaceship" operator: operator<=> to simplify this a bunch.

currently it's failed on MacOS build - I'm working with it

I chose to implement only the operator< and changed the comparison logic

Spaceship (<=>) operator requires realization for any field but for std::optional that operator marked as deleted. It requires for changing processing of SequenceRanges with unbonded maximum I don't have any good idea for resolving with another way.

MikePopoloski · 2024-05-19T13:07:29Z

source/ast/expressions/AssertionExpr.cpp

@@ -417,6 +490,71 @@ void SequenceRange::serializeTo(ASTSerializer& serializer) const {
        serializer.write("max", "$"sv);
 }

+bool SequenceRange::operator!=(const SequenceRange& right) const {


I think the logic here could just be defaulted? You're just comparing field by field right? So operator==(const SourceRange&) = default; should have the correct behavior?

it was removed in terms of fixing a previous comment

MikePopoloski · 2024-05-19T13:08:01Z

source/ast/expressions/AssertionExpr.cpp

+    return (*this == right) || (*this < right);
+}
+
+/// `SequenceRange`s intersects if max delay of one range


Documentation comments should go in the header, otherwise I don't think they'll be picked up by doxygen into the doc build.

MikePopoloski · 2024-05-19T13:11:39Z

source/ast/expressions/AssertionExpr.cpp

-        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.
+    if (bool isSeqAdmitsEmpty = expr.admitsEmpty(); isSeqAdmitsEmpty || expr.admitsNoMatch()) {


Rather than checking this again here can you rely on the bind() call above to do it by passing the right flags?

currently I don't have any idea how to correctly fix that because there is call to bind overload which accepts SequenceExprSyntax instead of PropertyExprSyntax

there are no way to fix that without changes in bind call behavior or StrongWeakPropertyExprSyntax struct

MikePopoloski · 2024-05-19T13:16:44Z

source/ast/expressions/AssertionExpr.cpp

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


You're just using the set for sorting here right? It's generally a good idea to avoid allocating containers unless strictly necessary, and in this case I think you can just store the current maximum and update it on each iteration if the new value is larger? You don't actually need to store all the items.

MikePopoloski · 2024-05-19T13:17:43Z

source/ast/expressions/AssertionExpr.cpp

@@ -1178,6 +1539,14 @@ void CaseAssertionExpr::serializeTo(ASTSerializer& serializer) const {
        serializer.write("defaultCase", *defaultCase);
 }

+/// Returns `nullopt` if `disable iff` condition is always `true` (`1`)
+std::optional<SequenceRange> DisableIffAssertionExpr::computeSequenceLengthImpl() const {
+    if (condition.constant && condition.constant->integer().countOnes())


The ConstantValue::isTrue() function is probably a nicer way to express this than calling countOnes()

MikePopoloski · 2024-05-19T13:18:41Z

include/slang/ast/expressions/AssertionExpr.h

    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);
+                                     bool isFollowedByProp = false, bool isOverlapImpl = false,


This is becoming too many boolean arguments in a row, which makes it easy to mess up the ordering of them when calling the function. I think this should be made a separate flags enum.

likeamahoney · 2024-05-22T12:54:55Z

Thank you for tackling this; the sections of the LRM that address this are daunting which is why I had not implemented it yet. I'll have to review this quite closely.

One thing that can help inform additional tests is looking at the coverage report, which shows some big chunks that haven't been tested at all yet.

At the moment I only added a few tests to increase the possible coverage but at all it still in progress

likeamahoney · 2024-05-23T11:56:02Z

Thank you for tackling this; the sections of the LRM that address this are daunting which is why I had not implemented it yet. I'll have to review this quite closely.
One thing that can help inform additional tests is looking at the coverage report, which shows some big chunks that haven't been tested at all yet.

At the moment I only added a few tests to increase the possible coverage but at all it still in progress

And also add support for checking nondegenerancy for lhs of "followed-by property" properties (e.g. #-# and #=#)

(16.12.22 SystemVerilog LRM section)

MikePopoloski · 2024-05-23T13:58:16Z

include/slang/ast/expressions/AssertionExpr.h

@@ -7,6 +7,10 @@
 //------------------------------------------------------------------------------
 #pragma once

+#include <optional>
+#include <set>


No longer need to include set here

removed all unnecessary headers which I was added early

MikePopoloski · 2024-05-23T14:00:05Z

include/slang/ast/expressions/AssertionExpr.h

-                                     bool allowSeqAdmitEmpty = false);
+    static const AssertionExpr& bind(
+        const syntax::PropertyExprSyntax& syntax, const ASTContext& context,
+        bool allowDisable = false, const NondegeneracyFlags nondegFlags = NondegeneracyFlags::None);


The const here does nothing -- since this is passed by value a copy will be made, which is fine, it's a small type.

MikePopoloski · 2024-05-23T14:01:34Z

include/slang/ast/expressions/AssertionExpr.h

@@ -239,11 +295,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 is can be evaluated as constant `false` (`0`).


"expression", -is

MikePopoloski · 2024-05-23T14:05:51Z

source/ast/expressions/AssertionExpr.cpp

@@ -7,6 +7,9 @@
 //------------------------------------------------------------------------------
 #include "slang/ast/expressions/AssertionExpr.h"

+#include <iostream>


iostream include should be unnecessary

MikePopoloski · 2024-05-23T14:11:24Z

source/ast/expressions/AssertionExpr.cpp

@@ -417,6 +471,47 @@ void SequenceRange::serializeTo(ASTSerializer& serializer) const {
        serializer.write("max", "$"sv);
 }

+bool SequenceRange::operator<(const SequenceRange& right) const {
+    // if both sequences are unbounded than check min's


s/than/then

MikePopoloski · 2024-05-23T14:43:34Z

source/ast/expressions/AssertionExpr.cpp

+    // If condition of `disable iff` can be evaluated only as `true` (`1`) than sequence property
+    // is no match
+    if (const auto evaluatedValue = context.tryEval(cond);
+        evaluatedValue.isInteger() && evaluatedValue.integer().countOnes()) {


fixed for all locations when I used countOnes

MikePopoloski · 2024-05-23T14:44:29Z

source/ast/expressions/AssertionExpr.cpp

+    std::optional<SequenceRange> 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)


Is this meant to be !max.has_value() ?

yes it's typo - fixed

MikePopoloski · 2024-05-23T14:48:19Z

source/ast/expressions/AssertionExpr.cpp

+                      : res;
+            break;
+        }
+        case BinaryAssertionOperator::And: {


You no longer set the admitsEmpty flag for the And case.

MikePopoloski · 2024-05-23T14:48:43Z

source/ast/expressions/AssertionExpr.cpp

+                      : res;
+            break;
+        }
+        case BinaryAssertionOperator::Intersect: {


MikePopoloski · 2024-05-23T14:50:21Z

source/ast/expressions/AssertionExpr.cpp

+        case BinaryAssertionOperator::Throughout: {
+            res = (rightAdmitsEmpty) ? res | NondegeneracyStatus::AdmitsEmpty : res;
+
+            // In case of `throught` full sequence is no match if right part is no match


s/throught/throughout

MikePopoloski · 2024-05-25T07:19:27Z

Ok, I think this is good enough to land -- we can tweak or improve it later if needed.

* master: (37 commits) Assertion expressions: only sequences can be nondegenerate, not properties Fix MSVC warning Be better about preserving the types of packed structs and unions used in binary operators Fix parameter default value visitor Cleanup of recent assertion expr changes; no change in behavior [slang][lang-compliance] Introduce nondegeneracy check (MikePopoloski#998) Update CHANGELOG.md Add Warith-op-mismatch, Wbitwise-op-mismatch, Wcomparison-mismatch, and Wsign-compare warnings Fix array type of cover symbol with-expression iterators Improve diagnostic location for constant conversion warnings Refactor Expression::getEffectiveSign to return a 3-state result Fix checking of sequence concat delay with single bracketed delay expression Add Wunused-import and Wunused-wildcard-import Improve parser error when encountering extra end delimiter in member list Don't add invalid generic class specializations to internal specialization map Add optional compiler directives from annex E Add optional system tasks and functions from annex D Make error for invalid state-dependent path conditions suppressible Update CHANGELOG.md v1800-2023 clarification: only specific bidi switches allow UDNT connections ...

likeamahoney changed the title ~~[slang] Introduce nondegenerancy check~~ [slang] Introduce nondegeneracy check May 17, 2024

likeamahoney changed the title ~~[slang] Introduce nondegeneracy check~~ [slang][lang-compliance] Introduce nondegeneracy check May 17, 2024

MikePopoloski reviewed May 19, 2024

View reviewed changes

likeamahoney force-pushed the feature/introduce-nondegeneracy branch from 3050cdf to 6895b51 Compare May 22, 2024 12:44

Yan Churkin and others added 9 commits May 23, 2024 15:14

[slang] Introduce nondegenerancy check

d3b8541

(16.12.22 SystemVerilog LRM section)

style: pre-commit fixes

ed2c821

MR issues fixes

eda9b2d

Fix MacOS build

e4bb52d

style: pre-commit fixes

d0fe2e7

Fix python bindings

44df591

Fix relational operator

ddb572d

style: pre-commit fixes

9fb009a

Remove redundant

85c8dae

likeamahoney force-pushed the feature/introduce-nondegeneracy branch from 0829546 to 85c8dae Compare May 23, 2024 12:15

MikePopoloski reviewed May 23, 2024

View reviewed changes

MR issue fixes

a4b2714

MikePopoloski merged commit 71c4be2 into MikePopoloski:master May 25, 2024
15 checks passed


		bool operator==(const SequenceRange& right) const;

		bool operator>(const SequenceRange& right) const;

[slang][lang-compliance] Introduce nondegeneracy check #998

[slang][lang-compliance] Introduce nondegeneracy check #998

Conversation

likeamahoney commented May 17, 2024

codecov bot commented May 17, 2024 • edited

Codecov Report

MikePopoloski commented May 18, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

likeamahoney commented May 22, 2024 • edited

likeamahoney commented May 23, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MikePopoloski commented May 25, 2024

codecov bot commented May 17, 2024 •

edited

likeamahoney commented May 22, 2024 •

edited