how to annotations to ltl properties

[doofin]

Hi, I'm trying to annotate ltl properties, however it seems that the Property class lacks the toNamed, toTarget and other methods, and it's also not a Data type, so the current annotation methods don't work. Is there a recommended way to annotate ltl properties in ChiselProve?

[seldridge]

We've been generally trying to move away from annotations. That said, I think these could be attached to assertions (AssertProperty) as they have a label, but not arbitrary property expressions.

Do you have some more information on what you're working on?

[doofin]

Thanks, we are working to enhance the formal verification support in Chisel, so we need to mark Property with more information, and annotations seem to be a good fit, there's also a related issue : https://github.com/chipsalliance/chisel/issues/**5078**