Amelia Dobis

[Verif] Add clocked Assert Assume Cover ops

1

This PR is in response to #6982 and adds clocked versions of assert, assume, cover. What still needs to be done: - [x] Update ExportVerilog - [x] Add Verifier that...

[Verif] Introduce a clocked assertion `verif.clocked_assert`

3

The current structure of the `verif` dialect requires the use of `ltl.clock` to associate a clock to an assertion (which is required). This means that a use-def analysis is required...

[firtool] Add an option to export SV without SVA

3

Some simulators like Verilator have very poor support for SVA syntax and will sometimes give a false positives when they are used. This PR adds an option that allows for...

[WIP] The goal of this PR is to introduce a first round of new test intent operations, for formal tests this time, to the verif dialect following [this proposal document](https://docs.google.com/document/d/1Ez6YosgVYuMtDg1MvBL8u9AMmntMARXhXofn_BcXlA4/edit?usp=sharing)....

[Verif] Allow for `disable` to be optional and infer it from property

3

This PR modifies the `verif::clocked_assertlike` ops to allow for the disable to be optional. In the case where it is omitted, it will be inferred from the property itself following...

This PR depends on #7104 . LTLToCore now folds the disable signals into their associated properties and yields clocked_assertlike ops instead of sv.assert. This follows the effort to get rid...

Current testing infrastructure in CIRCT makes it inconvenient to express test intent in the IR, these thus often rely on external tools and/or libraries implemented in the front-end languages to...

[FIRRTL] FIRRTL needs a contract interface

2

I introduced an interface for hardware contracts to the `verif` dialect. This should be exposed to FIRRTL so that we can access it via Chisel. Here is an idea of...

[Verif] Lowering from `verif.formal` to `verif.bmc`

2

The current formal test interface can be picked up by the btor2 back-end, but not the `circt-bmc` backend. It would be nice to look into whether or not this conversion...