Formality to verify sub-module

formality black box

Hi,
When I use formality to verify RTL vs netlist, I have scripts for top, but verify top is a time consuming job when I only want to verify a sub-module (after ECO), for example top/A/B.
Does the formality could do this job easily for my problem? how?

loglong

when to set black boxes in formality

Nobody help?

set black box formality

Hello friend,

Yes you can do it.

for example top/A/B. and u want to formaly verify B from both reference and implementation... the script should be as follows.

set ref_top_module "B"
set impl_top_module "B"
read_db -technology_library $target_library

create_container ref
read_verilog { ./NETLIST/design_files/<your RTL design files> }

set_top ref:/WORK/$ref_top_module
current_design ref:/WORK/$ref_top_module
set_reference_design ref:/WORK/$ref_top_module

create_container impl
read_verilog -container impl ./icarus_top_gate_converted_pad.vs

set_top impl:/WORK/$impl_top_module
current_design impl:/WORK/$impl_top_module
set_implementation_design impl:/WORK/$impl_top_module
...
....
...
You need to mention the "set_top" design as the design file u want to verify.

Hope this will solve your problem.

Regards,
Sunil Budumuru

formality for blackbox

Hi, Sunil:

I think you have some misunderstanding for the subject.

I mean I want to read full design on which the scan and jtag.. configuration based, because the scripts is ready for full design after layout.

But after ECO, I only care a small sub-module consistency, so I only want to verify this sub-module due to the full-design verification is time consuming.

So can I only verify a sub-module when I read full-design?

BTW, I tried your method, it cannot work when I set the scan and other configuration.
And I tried use script to parse the sub-module DFF and use [verify designID1 designID2] to verify, but the time is slow too because this command will execute one by one and make the efficiency down.

set_constant formality

Hi, loglong

if you want to compare submodule, you can just set root module is sub_name, even you read full design.

and another method I think you can try to set black box for rest part.

it is right my understanding?

Regards

set_top +

Hi, littlebu:

Thanks, but just as I mentioned, I could set_top for sub_name, but I cannot use the configuration which set for SE, etc any more, e.g. I [set_top top/A/B], that's right, but [set_constant -type port r:/work/top/SE 0] will be reported error due to cannot find the port because set_top for sub_name. So the scripts cannot reuse any more.

I will try black box, thanks again.

Added after 7 minutes:

Please focus on the issue:

I want to read and configure full design (it is not consume much time), but I only want to verify a small sub-module instead of whole design to save time.

Added after 1 hours 51 minutes:

I find it's simple when [set_top TOP] and [set_reference B] [set_implementation B] will solve my problem, but I have to add set_user_match to match rtl clock and layout clock tree manually.

formality eco

Hi loglong,

You can set a constant value to the internal signal.

"set_constant -type net ref:/WORKtop/A/B/SE 0"

As scan enable will be routed to all the modules, u can get the scan enable signal and force a constant value on it in the internal modules.

And you want just to concentrate on the logic cone at which you've ECOed for formal verification, please follow the document that suits to your problem.