SystemVerilog Assertion Support

[sequencer]

Core Problem:

The fundamental issue with standard SVA is that all sequence and property constructs carry implicit clocking semantics. This creates ambiguity, particularly for immediate assertions which, despite being combinational, are formally verified using a conceptual, tool-provided clock.

Proposed Design Philosophy:

To create a clearer and more explicit system, this design moves away from SVA's implicit clocking. The core principle is to make all clocking relationships explicit within the API, thereby improving type and semantic clarity:

1. Explicit Separation of Sequence and Property: Unlike SystemVerilog, this design introduces two distinct API kinds to represent the different concepts:

• ref_to_bool.S: Represents a Sequence. It is a temporal construct that is always explicitly bound to a clock.
• sequence.P: Represents a Property without any clock semantic.

2. Explicitly Clocked Sequences: Under this model, there are no "un-clocked" or implicitly clocked sequences. Every sequence (ref_to_bool.S) must be associated with an explicit clock, eliminating ambiguity.

3. Handling Immediate Assertions: The main challenge in an explicitly clocked system is how to handle immediate SVA assertions, such as those used for verifying combinational logic (always_comb). These assertions rely on a "virtual" clock provided by formal verification tools for their decision points.
   To solve this, a new, dedicated API is introduced:

• ref_to_bool.I: Represents a non-temporal, Immediate boolean expression derived from LTL. This construct is used only for clock-less, immediate assertions.

The capabilities of ref_to_bool.I are intentionally restricted to maintain semantic integrity:

• It can imply another I expression or be converted directly into a Property.
• It cannot be temporally concatenated with sequences (e.g., using ##), as it exists outside the clocked temporal domain.

[unlsycn]

import zaozi.given

[Clo91eaf]

I will take this PR. This PR is related to llvm/circt#8673, but they are independent implecation of each other. After I finish the work for issue 8673, I will open a new PR to introduce and integrate the new explicit clocking design.