[slang] Add an inputs/edges combination coverage check for udp

[likeamahoney]

Closes #936

Hi, all!

That PR add a new check which specified by SystemVerilog LRM: "If the behavior of the UDP is sensitive to edges of any input, the desired output state shall be specified for all edges of all inputs."

[codecov]

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 94.78%. Comparing base (6e18236) to head (b417058).

Additional details and impacted files

@@            Coverage Diff             @@
##           master    #1087      +/-   ##
==========================================
+ Coverage   94.77%   94.78%   +0.01%     
==========================================
  Files         191      191              
  Lines       47757    47861     +104     
==========================================
+ Hits        45260    45364     +104     
  Misses       2497     2497              

Files with missing lines	Coverage Δ
include/slang/ast/symbols/MemberSymbols.h	97.46% <ø> (ø)
source/ast/symbols/MemberSymbols.cpp	97.65% <100.00%> (+0.18%)	⬆️

---

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 6e18236...b417058. Read the comment docs.

[likeamahoney]

The controversial point is the number of possible edge variants that need to be checked, I took the maximum (i checks also 0x/1x/x1/x0 edge presence), although some can be removed (x edges I think) - the LRM clearly does not say about this - which ones need to be checked and which ones do not. All edges should be checked it says.

Below an example of my checker error output for such code sample:

primitive d_edge_ff (q, clock, data);
output q; reg q;
input clock, data;
table
// clock data q q+
p ? : ? : 1 ;
endtable
endprimitive

err output:

udptest.sv:1:11: error: if the behavior of the UDP is sensitive to edges of any input, the desired output state shall be specified for all edges of all inputs.
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for '(1x) 0' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for '(x0) 0' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for '(10) 1' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for '(1x) 1' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for '(x0) 1' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for '(10) x' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for '(1x) x' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for '(x0) x' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for '0(01)' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for '0(0x)' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for '0(10)' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for '0(1x)' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for '0(x0)' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for '0(x1)' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for '1(01)' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for '1(0x)' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for '1(10)' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for '1(1x)' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for '1(x0)' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for '1(x1)' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for 'x(01)' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for 'x(0x)' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for 'x(10)' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for 'x(1x)' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for 'x(x0)' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);
          ^
udptest.sv:1:11: note: missed desired output for 'x(x1)' edge-sensitive input specification
primitive d_edge_ff (q, clock, data);

[MikePopoloski]

Can you break this PR into two, one for the bug fixes and one for the new check? It's hard to see which parts are for which.

[likeamahoney]

Can you break this PR into two, one for the bug fixes and one for the new check? It's hard to see which parts are for which.

Separated in #1097.

1097 PR fixes only exist UDP analysis bugs.

The current request contains 2 commits (the first is a commit from 1097) - the second adds coverage analysis. The first commit is left because the quality of the analysis depends on these changes. I remove first commit from this PR when 1097 will be merged.

[likeamahoney]

Can you break this PR into two, one for the bug fixes and one for the new check? It's hard to see which parts are for which.

Separated in #1097.

1097 PR fixes only exist UDP analysis bugs.

The current request contains 2 commits (the first is a commit from 1097) - the second adds coverage analysis. The first commit is left because the quality of the analysis depends on these changes. I remove first commit from this PR when 1097 will be merged.

first commit with UDP overlap bug fixes was removed from current branch cause of #1097 was merged

[MikePopoloski]

I found some time to look at the behavior here. It seems like there aren't any commercial tools that implement this check. Furthermore even the LRM seems inconsistent about it; some of their examples don't follow the rule. I'm wondering whether even want to have this check in the first place -- this might be one of the cases where the LRM is just poorly specified and shouldn't have this sentence in it. Do you have any first hand experience that makes you think having this check would be a good idea, or were you just going off the existence of the issue in my tracker?

[likeamahoney]

I found some time to look at the behavior here. It seems like there aren't any commercial tools that implement this check. Furthermore even the LRM seems inconsistent about it; some of their examples don't follow the rule. I'm wondering whether even want to have this check in the first place -- this might be one of the cases where the LRM is just poorly specified and shouldn't have this sentence in it. Do you have any first hand experience that makes you think having this check would be a good idea, or were you just going off the existence of the issue in my tracker?

Thank you for your response! I have been investigating a few examples of sequential trigger technological cells developed as part of the technological core library. These cells are designed as Verilog primitives for simulating semantic property testing, similar to industrial Liberty cells. In these primitives, it is common practice to ignore or marking it's illegal data oscillations on all signals, including non-clock signals. For example:

// clk data reset_notifier
...
    ?     *     ?  :    ?     :     -
    ?     ?     *  :    ?     :     x
...

The developers also add “pessimistic” paths for specific ‘x’ input edges. Although most users do not utilize them. Checking the completeness property may be relevant only for developers of industrial libraries. Therefore, I propose wrapping this functionality in an option and issuing a warning.

[MikePopoloski]

Ok, we should make this a warning then, and probably put it in the pedantic group instead of the default one.

[likeamahoney]

Ok, we should make this a warning then, and probably put it in the pedantic group instead of the default one.

I made this a warning in a pedantic group

[MikePopoloski]

The reason I've been hesitating to merge this is that I'm concerned about the potential performance impact when run against primitives with large numbers of inputs. The complexity requirements of the checking algorithm seem high, and there's a lot of std::vector copying and comparing going on. Also when there are large numbers of inputs I'd expect the diagnostic output to grow comically large. It's probably worth thinking about those cases more.

[likeamahoney]

The reason I've been hesitating to merge this is that I'm concerned about the potential performance impact when run against primitives with large numbers of inputs. The complexity requirements of the checking algorithm seem high, and there's a lot of std::vector copying and comparing going on. Also when there are large numbers of inputs I'd expect the diagnostic output to grow comically large. It's probably worth thinking about those cases more.

Hi! Solution was optimized. As it can be seen in last commit:

1. Now there is no full copying of the vector anywhere
2. Reduce number of vector compares.
3. Reduce number of nested cycles
4. Optimize algorithm by ahead checking the presence of any value input ((??) for edge input an ? for simple input) at first position to ignore checking of concrete values at this position which will optimize number of iterations and reduce output .
5. Reformat output. Now it looks like this:

primitive p1 (q, clock, data);
          ^
udp.sv:1:11: note: missed desired output for rows:
(0x) 0
(10) 0
(1x) 0
(x0) 0
(x1) 0
(0x) 1
(10) 1
(1x) 1
(x0) 1
(x1) 1
(0x) x
(10) x
(1x) x
(x0) x
(x1) x
? (01)
? (0x)
? (10)
? (1x)
? (x0)
? (x1)

primitive p1 (q, clock, data);
          ^

For such example:

primitive p1 (q, clock, data);
    output q; reg q;
    input clock, data;
    table
        // clock data q q+
        (01) ? : ? : 0 ;
    endtable
endprimitive

Or like this:

degee.sv:1:11: warning: if the behavior of the UDP is sensitive to edges of any input, the desired output state shall be specified for all edges of all inputs. [-Wudp-coverage]
primitive d_edge_ff (q, clock, data);
          ^
degee.sv:1:11: note: missed desired output for rows:
(10) 0
(1x) 0
(x0) 0
(10) 1
(1x) 1
(x0) 1
(10) x
(1x) x
(x0) x
? (01)
? (0x)
? (10)
? (1x)
? (x0)
? (x1)

primitive d_edge_ff (q, clock, data);
          ^

for example from first this PR comment:

primitive d_edge_ff (q, clock, data);
  output q; reg q;
  input clock, data;
  table
  // clock data q q+
  p ? : ? : 1 ;
  endtable
endprimitive

Without optimizations everything looked much worse and large, as you can see from the comment above.

Obviously, this is a dynamic programming problem, so as not to be solved by exhaustive search. In the future, other optimizations are also possible (for example - checking ? not only in the first position).

[likeamahoney]

mark as draft due to founded bug

[likeamahoney]

mark as draft due to founded bug

bugs were fixed

[likeamahoney]

The reason I've been hesitating to merge this is that I'm concerned about the potential performance impact when run against primitives with large numbers of inputs. The complexity requirements of the checking algorithm seem high, and there's a lot of std::vector copying and comparing going on. Also when there are large numbers of inputs I'd expect the diagnostic output to grow comically large. It's probably worth thinking about those cases more.

Hi! Solution was optimized. As it can be seen in last commit:

1. Now there is no full copying of the vector anywhere
2. Reduce number of vector compares.
3. Reduce number of nested cycles
4. Optimize algorithm by ahead checking the presence of any value input ((??) for edge input an ? for simple input) at first position to ignore checking of concrete values at this position which will optimize number of iterations and reduce output .
5. Reformat output. Now it looks like this:

primitive p1 (q, clock, data);
          ^
udp.sv:1:11: note: missed desired output for rows:
(0x) 0
(10) 0
(1x) 0
(x0) 0
(x1) 0
(0x) 1
(10) 1
(1x) 1
(x0) 1
(x1) 1
(0x) x
(10) x
(1x) x
(x0) x
(x1) x
? (01)
? (0x)
? (10)
? (1x)
? (x0)
? (x1)

primitive p1 (q, clock, data);
          ^

For such example:

primitive p1 (q, clock, data);
    output q; reg q;
    input clock, data;
    table
        // clock data q q+
        (01) ? : ? : 0 ;
    endtable
endprimitive

Or like this:

degee.sv:1:11: warning: if the behavior of the UDP is sensitive to edges of any input, the desired output state shall be specified for all edges of all inputs. [-Wudp-coverage]
primitive d_edge_ff (q, clock, data);
          ^
degee.sv:1:11: note: missed desired output for rows:
(10) 0
(1x) 0
(x0) 0
(10) 1
(1x) 1
(x0) 1
(10) x
(1x) x
(x0) x
? (01)
? (0x)
? (10)
? (1x)
? (x0)
? (x1)

primitive d_edge_ff (q, clock, data);
          ^

for example from first this PR comment:

primitive d_edge_ff (q, clock, data);
  output q; reg q;
  input clock, data;
  table
  // clock data q q+
  p ? : ? : 1 ;
  endtable
endprimitive

Without optimizations everything looked much worse and large, as you can see from the comment above.

Obviously, this is a dynamic programming problem, so as not to be solved by exhaustive search. In the future, other optimizations are also possible (for example - checking ? not only in the first position).

comment was updated