Correct method to ignore assert() statements?

Users
1

Hello,

During a production synthesis run, intended to target a physical design (in this case ASIC), as opposed Formal Verification, Simulation, Design-For-Test and other non-production use cases.

When using hierarchy -check -top top_module_name -nokeep_prints -nokeep_asserts this still creates $check cells. Docs indicate that the options relate to implicit verilog attributes that annotate these pseudo cell types ?

The `read_verilog` has options to remove such items `-noassert -noassume -norestrict` does it make sense to use these options by default for any production synthesis usage ? Should `-nocover` be a option in there as well ?

Issuing a subsequent delete t:$check after the hierarchy command can then remove the cells inserted via assert usage from the design. Is this the correct and only command that needs to be used to resolve the correct view of the design for the flow ?

Are there any other scenarios which should have a similar treatment because they would insert pseudo cells if a particular non-synthesisable construct was present in the design ? For example if SVA was implemented would that also result in t:$check cell types being inserted or is there another type that exists ?

Are there any Design For Test use cases where assert() directives maybe left in circuit, for which presumably a techmap should be available to replace and manage them in the design ? For example attaching them to memory/scan-chain and cataloging them like debug symbols.

What historically are the cell types $print and $assert does a particular front-end create them, does an older Yosys version use them? Are they still in use today ?

When I use a Verilog statement $info(“info”); I get an error of not being table to lookup task. The read_verilog has a -nodisplay option, but its the hierarchy fails, and it does not seem possible to delete them in between. delete p:$info was tried, I was thinking maybe I need to read_rtlil my_null_task_$info.txt which might contain process $info\n end\n to provide a no-op, but maybe this is better available in the hierarchy command option which is the step causing error. Or maybe there is a reason this is a bad idea ? Comments welcome.

Thanks

Darryl

2

It’s correct that hierarchy’s -nokeep_prints and -nokeep_asserts options only affect implicit adding of the (* keep *) attribute.

For removing all assertion related cells, I’d recommend using chformal -remove, as that handles $check as well as $assert, $assume, … This does the same as using delete t:$check for all assertion only cell types, so that wouldn’t be wrong either, but the list of related cell types is likely to grow in the future and using chformal -remove ensures forwards compatibility in that case.

This does not remove any $print cells, so you might still want to run delete t:$print.

Removing those cells also does not automatically remove any cells generated (e.g. for the checked condition). Those would remain as unused cells, but running clean will get rid of those. If you have assertion only helper modules in the design that you want clean to remove as well it is important to use the -nokeep_{prints,asserts} option of hierarchy as clean will not remove unused submodules if they have a (* keep *) attribute.

Implementing SVA doesn’t require addition of new cell types, but it is likely that we add additional new cell types that will be used in conjunction with the current ones. (With the non-open-source SV frontend in Tabby CAD, yosys already supports SVA and only uses $assert, $assume, $live, $fair and $cover).

There are also some more non-synthesizable cell types you can expect to encounter, e.g. $scopeinfo is emitted by flatten to retain some information about the module hierarchy and it’s plausible that there will be more in the future.

We currently don’t have a way to remove all such cells in a forwards compatible way, but we will hopefully add that in the near future.

The $check cell is a newer replacement for the $assert, $assume, etc. cells, but both variants are still supported and depending on the frontend, you might get either . The chformal -lower pass can be used to convert the newer $check to the older cell types as many formal verification flows only support the older variant. The $print cell type is emitted by read_verilog for statements like $display("Hello world! a = %x, b = %x", a, b);

Exposing assertions using a scan chain sounds like a reasonable use case to me, you could write a techmap rule (see help techmap) that replaces all instances of a specific cell type like $check, with e.g. a scan chain FF primitive of your target cell library with a (* keep *) attribute so it stays around even with the output being unused.

With read_verilog, the $info, etc. severity system tasks are only supported at the module level, not within any procedural blocks (i.e. it only support the elaboration severity tasks not the run-time severity tasks). Since the frontend already supports $info, but limited to a different context, there’s no way to define the $info task yourself, so currently you would have to hide it using some `ifdef. As far as I can tell, there’s no inherent reason why the frontend couldn’t be extended to also support it in similar to how it supports $display.

The RTLIL process construct is not directly related to Verilog tasks, you would have to use the Verilog task or function module items to define your own tasks or functions, which would work for defining a no-op, if there wasn’t already partial support for $info implemented.

3

Thanks Jix I will update this thread in due course on progress.