Not able to understand the format of the signal in SMTC

[rajoogupta]

Hi,
I am not able to understand how yosys is defining some signals which are of the format hierarchy1.hierarchy2.$auto$verificsva.cc:1762:import$21094 in smtc file.

Kindly let me know how to figure out the signal or how to decode this pattern in SMTC file.

Thanks & Regards
Rajoo

[cliffordwolf]

Hi. How did you create this netlist? The flatten command should never create a name that combines internal names (starting with $) and public names (without $ prefix). Is this smtbmc on an unflattened netlist?

In general there is no method for predicting internal names.

It would help if you could describe what you are trying to do, and how to reproduce the results you are seeing.

[rajoogupta]

Hi,
I have run yosys-smtbmc on the RTL written in SV, which created a trace.smtc in which I saw the format similar to hierarchy1.hierarchy2.$auto$verificsva.cc:1762:import$21094.
I had issue in figuring out what the particular signal is , as the final signal name is not mentioned in hierarchy.

Thanks
Rajoo