How to route input of $assert cell to newly created port

[Topi-ab]

Hi,

I am trying to find a way to automatically convert GHDL's PSL asserts to a HW-ready checker.

I can import VHDL file with embedded PSL to yosys, and it seems that all asserts are routed to $assert cells.

As the $assert prototype doesn't have any output, I cannot just map it to another representation with output (or can I ?)

The wanted outcome is to route the inputs (assert and enable) of $assert to a wire (through and port) and route that wire to a new external port.

Can this be achieved without manual intervention?

[jix]

The expose -evert command can in fact do that, and I think the following yosys script using it might do what you're asking for:

# Flatten the hierarchy, so we don't need to route new signals through multiple
# hierarchy levels
flatten

# Ensure that the formal cells have a public name, required for the expose command
rename -enumerate -pattern unnamed_assert_% t:$assert
rename -enumerate -pattern unnamed_assume_% t:$assume
rename -enumerate -pattern unnamed_cover_% t:$cover
# ... and $fair, $live if required

# Turn inputs to formal cells into output ports of the containing module
expose -evert t:$assert t:$assume t:$cover

[Topi-ab]

Thanks a lot !!!

This definitely did the trick.

[nakengelhardt]

By the way, #3610 adds a pass to do the same thing while keeping the hierarchy intact and routing the signals up through multiple levels to outputs on the top module.