[slang] Introduce clock resolution support (SystemVerilog LRM 16.13/16.16 sections).

[likeamahoney]

Closes https://github.com/MikePopoloski/slang/issues/536

In this PR, I introduce the implementation of all possible illegal situations from the SystemVerilog LRM 16.13/16.16 sections and also some additional clock checks that support VCS.

Here is the bunch of new error types such as: 1) no clock could be resolved for concurrent property (emitted if there is a property which is not mapped to any clock):

module top (input logic a, b, c, clk);

   property q1;
      $rose(a) |-> ##[1:5] b;
   endproperty

   property q5;
      @(negedge clk) b[*3] |=> !b;
   endproperty

   property q6;
      q1 and q5;
   endproperty

a5: assert property (q6); // Illegal
a6: assert property ($fell(c) |=> q6); // Illegal
endmodule

2) explicit clocking event in clocking block (see section 16.16 clocking block rules - (b.1))

module top(input clk, a, b);
    clocking sys_clk @(posedge clk);
       // no explicit event control is allowed in any property or sequence declaration
       // in clocking block
       property p_with_one_clock; @(posedge clk) a|=> b; endproperty : p_with_one_clock // illegal
    endclocking :sys_clk
endmodule // top

3) the property/sequence has clocking event not identical to that of the clocking block (see section 16.16 clocking block rules - (b.3))

module top(input clk, clk2, a, b);
   sequence s_with_one_ck;  @(posedge clk) a;
   endsequence // s_with_one_ck
   sequence s_with_one_ck2;  @(posedge clk2) b;
   endsequence // s_with_one_ck

   clocking sys_clk @(posedge clk);
      property p_ok; not s_with_one_ck; endproperty
      // If a named sequence that defined outside the clocking block is used, its clock,
      // if specified, must be identical to the clocking block's clock 
      property p_not_ok; not s_with_one_ck2; endproperty // illegal
   endclocking :sys_clk
endmodule

4) single semantic leading clock expected for top-level sequence/property expression (see 16.13.7 and 16.16.1)

module top(input logic a, b, c, clk, clk_n, req1, req2, rst_n);
   sequence seq;
      @(negedge clk) a ##1 @(posedge clk_n)b;
   endsequence // seq
   always @(posedge clk) begin
      assert property (seqX); // Illegal
   end
endmodule // top

5) no default, inferred, or explicit leading clocking event and maximal property is not an instance (see section 16.16 clocking block rules - (f))

module top(input b, input clk)
  sequence s2;
     $rose(a) ##[1:5] b;
  endsequence

  sequence s3;
     @(negedge clk) s2;
  endsequence

  c3: cover property (s3); // legal
  c4: cover property (s3 ##1 b); // Illegal
endmodule // top

6) procedural assertion (assert, assume or cover property) is not allowed after delay or event control statement (vcs check which based on 16.14.6 (and also 16.14.6.2 - "In general, procedural concurrent assertions must be used carefully when mixed with time delays.") section where delay and event controls prevents clock inference for always block assertions - I decide to make it error like VCS do but not sure)

module top(input e1, e2, reset, output dout);
   logic d1, i1, i2, i3, i4;
   logic e1N;
   logic sL, sL1, egL;
   always @(posedge e1) begin
      d1 <= i1|i2 ;
      @(posedge e2) egL <= sL & sL1;
      a1: assert property (d1 |=> i3|i4); // illegal - procedural assertion (assert, assume or cover property) is not allowed after # delay or event control statement
   end
endmodule // top

7) clocking events of binary sequence/property operands doesn't agree (see 16.13.1)

module top(input e1, e2, reset, output dout);
   reg  b1, b2;
   sequence a1;
      (@(posedge (e1 | e2)) b1) and (@(posedge (e1 | e2)) b2);
   endsequence // a1
   assert property(a1);
   sequence a2;
      (@(posedge (e1 | e2)) b1) and (@(posedge e1) b2);
   endsequence // a2
   assert property(a2);  // illegal
endmodule // top

8) clocking events of delay concatenation operands doesn't agree (see 16.13.1)

module multiclock();
   reg clk, clk1, clk2, clk3;
   reg b0, b1, b2;
   assert property (##3 (@(posedge clk1) b1) ##1 (@(posedge clk2) b2) ##2 (@(posedge clk3) b3));
endmodule

9) differently clocked sequence shall not admit any empty match (see 16.13.1)

module multiclock();
   reg clk, clk1, clk2, clk3;
   reg b0, b1, b2;
   assert property (@(posedge clk) b1[*0:1]) ##1 (@(posedge clk1) b2);  // illegal - empty match of b1
endmodule

The main data structure is ClockingEvent, which is a wrapper for SignalEventControl, it stores the event in two different forms - edge (EdgeKind) + vector of signal references (EventList) and strEvent (string representation for comparing two different clock events - in case the event is a complex expression (e.g. contains iff expr...)). This data structure is designed to accumulate clock events during AST traversal and then compare them (in the case of a complex event - they are compared as strings, otherwise the symbol vectors are simply compared together with the edge).

The algorithm starts its work immediately after the end of the elaboration of the AST. It is launched only in the absence of errors (invalid nodes) in it, as incorrect assumptions can be made during the analysis of clock signals.

A clock signal is considered to be a signal that is present in the EventList sequence or properties, as well as those signals from the sensitivity list of the always block that are not used anywhere inside except for assertions.

The algorithm is implemented as nested AST visitors. The main one is the ClockResolutionVisitor, which searches for clocking blocks (which override the clock event for the entire instance) by calling the ClockingBlockVisitor (checking the correctness of assertion sequences and properties inside it) for each instance of the module. It first calls MarkInvalidVisitor to mark invalid nodes that slang may leave even in the absence of errors. When encountering an assertion, it calls ConcurrentAssertionVisitor, which traverses the property under the assertion and tries to infer a clock event for it, which in turn calls SequenceVisitor to traverse and check clock properties of the sequence under the property.

There are also 2 separate visitors - AlwaysTimingVisitor and AlwaysTimingCheckUseVisitor, the first of which fills in inferred clocks from SignalEventControl, and the second one removes from inferred clocks those which are used outside of assertions - those that are not considered clocks according to the standard.

[codecov[bot]]

Codecov Report

Attention: Patch coverage is 96.48712% with 15 lines in your changes missing coverage. Please review.

Project coverage is 94.87%. Comparing base (73b79be) to head (751e1c7). Report is 3 commits behind head on master.

Additional details and impacted files

[](https://app.codecov.io/gh/MikePopoloski/slang/pull/1027?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=Michael+Popoloski) ```diff @@ Coverage Diff @@ ## master #1027 +/- ## ========================================== + Coverage 94.69% 94.87% +0.18% ========================================== Files 191 193 +2 Lines 47553 48023 +470 ========================================== + Hits 45031 45563 +532 + Misses 2522 2460 -62 ``` | [Files](https://app.codecov.io/gh/MikePopoloski/slang/pull/1027?dropdown=coverage&src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=Michael+Popoloski) | Coverage Δ | | |---|---|---| | [include/slang/ast/Compilation.h](https://app.codecov.io/gh/MikePopoloski/slang/pull/1027?src=pr&el=tree&filepath=include%2Fslang%2Fast%2FCompilation.h&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=Michael+Popoloski#diff-aW5jbHVkZS9zbGFuZy9hc3QvQ29tcGlsYXRpb24uaA==) | `100.00% <ø> (ø)` | | | [include/slang/driver/Driver.h](https://app.codecov.io/gh/MikePopoloski/slang/pull/1027?src=pr&el=tree&filepath=include%2Fslang%2Fdriver%2FDriver.h&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=Michael+Popoloski#diff-aW5jbHVkZS9zbGFuZy9kcml2ZXIvRHJpdmVyLmg=) | `100.00% <ø> (ø)` | | | [source/ast/Compilation.cpp](https://app.codecov.io/gh/MikePopoloski/slang/pull/1027?src=pr&el=tree&filepath=source%2Fast%2FCompilation.cpp&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=Michael+Popoloski#diff-c291cmNlL2FzdC9Db21waWxhdGlvbi5jcHA=) | `96.75% <100.00%> (+0.02%)` | :arrow_up: | | [source/driver/Driver.cpp](https://app.codecov.io/gh/MikePopoloski/slang/pull/1027?src=pr&el=tree&filepath=source%2Fdriver%2FDriver.cpp&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=Michael+Popoloski#diff-c291cmNlL2RyaXZlci9Ecml2ZXIuY3Bw) | `94.95% <80.00%> (-0.15%)` | :arrow_down: | | [source/ast/ClockResolution.cpp](https://app.codecov.io/gh/MikePopoloski/slang/pull/1027?src=pr&el=tree&filepath=source%2Fast%2FClockResolution.cpp&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=Michael+Popoloski#diff-c291cmNlL2FzdC9DbG9ja1Jlc29sdXRpb24uY3Bw) | `99.41% <99.41%> (ø)` | | | [include/slang/ast/ClockResolution.h](https://app.codecov.io/gh/MikePopoloski/slang/pull/1027?src=pr&el=tree&filepath=include%2Fslang%2Fast%2FClockResolution.h&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=Michael+Popoloski#diff-aW5jbHVkZS9zbGFuZy9hc3QvQ2xvY2tSZXNvbHV0aW9uLmg=) | `82.60% <82.60%> (ø)` | | ... and [20 files with indirect coverage changes](https://app.codecov.io/gh/MikePopoloski/slang/pull/1027/indirect-changes?src=pr&el=tree-more&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=Michael+Popoloski) ------ [Continue to review full report in Codecov by Sentry](https://app.codecov.io/gh/MikePopoloski/slang/pull/1027?dropdown=coverage&src=pr&el=continue&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=Michael+Popoloski). > **Legend** - [Click here to learn more](https://docs.codecov.io/docs/codecov-delta?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=Michael+Popoloski) > `Δ = absolute (impact)`, `ø = not affected`, `? = missing data` > Powered by [Codecov](https://app.codecov.io/gh/MikePopoloski/slang/pull/1027?dropdown=coverage&src=pr&el=footer&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=Michael+Popoloski). Last update [73b79be...751e1c7](https://app.codecov.io/gh/MikePopoloski/slang/pull/1027?dropdown=coverage&src=pr&el=lastupdated&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=Michael+Popoloski). Read the [comment docs](https://docs.codecov.io/docs/pull-request-comments?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=Michael+Popoloski).

[MikePopoloski]

Thanks for the PR. I'll do a more thorough review of the resolution logic, but to comment on the high level approach:

• It's preferable if the resolution and checking can be done alongside the normal elaboration visitation. In particular users don't like when they can't see all errors in one go, and have to fix some errors in order to enable seeing additional ones. I think this should be doable; the rest of slang gracefully ignores errors.
• The information derived here is likely to be wanted / needed by downstream logic that emits output based on the AST, like a simulator or a lint tool or whatever, so I don't think it should be a hidden internal pass. Probably the results of the various resolution steps can be computed and stored on the relevant nodes. For example, the inferred clocking event for a procedural block can be a stored value in the ProceduralBlockSymbol, each concurrent assertion instance can have a getLeadingClock method, etc. Then rather than having visitors that traverse downward through the tree, the assertion instances would look upward to their scope to resolve the nearest default clock to use.