Example of write_aiger working with assert

[gjasper]

I am fairly new to Yosys, so let me start by expressing my gratitude for this amazing tool and support. =)

So far I was unable to find a working example that reads a verilog with simple asserts and writes an aiger file. My own tries are always running into:

ERROR: Unsupported cell type: $check

Can I find the simplest example for it somewhere? More generally, is there a recommended place to look for examples?

[KrystalDelusion]

I would recommend checking out how SBY does it (or use SBY directly, depending on what you need).

[gjasper]

Thanks! I did looked into it but was still unable to avoid the error above.

I also found an example on the repo itself that errors out with the same message.

yosys/examples/aiger/demo.sh

I tested with some earlier versions and found that with a build from 20240101 both my test and the example work fine. Though the example errors out with another message that is fixed with dffunmap.

[georgerennie]

the specific $check issue can be solved by running chformal -lower which converts $check cells into assert/assume etc that the aiger backend supports. a few months back some of the internal code moved from generating assert/assume directly to generating $check cells instead

[KrystalDelusion]

Thanks George!