Why is assert property wrapped in an always block?

[fabianschuiki]

Consider this simple Verilog snippet:

module Foo (input logic clock, a, b);
  assert property (@(posedge clock) a == b);
endmodule

Running this through slang --ast-json=/dev/stdout produces the following AST (trimmed down):

"kind": "ProceduralBlock",
"procedureKind": "Always",
"body": {
  "kind": "ConcurrentAssertion",
  "propertySpec": {
    "kind": "Clocking",
    "clocking": {
      "kind": "SignalEvent",
      "expr": "clock",
      "edge": "PosEdge"
    },
    "expr": {
      "kind": "Simple",
      "expr": {
        "kind": "BinaryOp",
        "type": "logic",
        "op": "Equality",
        "left": "a",
        "right": "b"
      }
    }
  }
}

Why does Slang wrap this assert property inside of an always procedure?

[MikePopoloski]

16.14.5 describes how assertions outside of procedural code are specified to behave as if they had been wrapped in an always block, so slang normalizes them to the same form.

[fabianschuiki]

Thanks for the pointer 🙌. I was trying to wrap my head around what the semantics of a concurrent assert would be under an always procedure. That section outlines it pretty nicely:

Such a concurrent assertion statement uses the always semantics, meaning that it specifies that a new evaluation attempt of the underlying property_spec begins at every occurrence of its leading clock event.

On the CIRCT side, we'll have to figure out what it even means to have multiple "threads" of checking an assert in flight in parallel. It's almost like an assert property forks the current thread and launches a separate state machine that checks whether the property holds as time progresses. Consider something like this:

module Foo(input logic a, b, c);
  always if (a) assert property (b |-> #10 c);
endmodule

The way I understand the spec, this would mean that the simulator activates the always procedure in every time step. Which then means that a == 1 in any delta step would launch a "thread" to check the assert. That assert would immediately succeed if b == 0, but if b == 1, the thread would suspend for 10 time steps and then check c == 1 at that time. This is going to be fun to capture in the IR 🤣

[MikePopoloski]

Yes indeed, it gets quite complicated, especially once local variables get involved, multiple clocks for different subsequences, recursive properties, etc. You've probably already seen but Annex F has formalized descriptions of a lot of this, though it's quite dense.

[fabianschuiki]

Our first stab at this was to try and capture the temporal expressions like b |-> #10 c almost like an AST in the IR. That's almost impossible to analyze properly though, so probably a false start. It works well for generating Verilog, but if you're actually trying to make sense of the SVAs and simulate them, it's pretty useless. I'm wondering if there's value in trying to capture the temporal logic almost like a separate thread in the IR with a bit of code that is assumed to be launched and executed in parallel. The annoying part is that we also do want to be able to take our IR and emit it as valid SVA text. And anything that captures that concurrent nature like a separate block of code running in parallel is bound to be very hard to emit back at this higher level of abstraction that the SVAs provide.

[svenka3]

Interesting thread - an orthogonal observation that maybe useful @fabianschuiki (Though maybe you already are aware):

module Foo(input logic a, b, c);
  always if (a) assert property (b |-> ##10 c);
endmodule

Your rewrite/pseudo-code makes it more interesting than just "concurrent assertions." There is a variant known as "procedural concurrent assertions" in the SV LRM, though very few users use it (as far as I have seen over last 10+ years), from a language perspective, it exists.