Continue to Site

Welcome to EDAboard.com

Welcome to our site! EDAboard.com is an international Electronics Discussion Forum focused on EDA software, circuits, schematics, books, theory, papers, asic, pld, 8051, DSP, Network, RF, Analog Design, PCB, Service Manuals... and a whole lot more! To participate you need to register. Registration is free. Click here to register now.

Logic synthesis with assertions?

Status
Not open for further replies.

mliu66

Newbie level 3
Joined
Jun 13, 2006
Messages
3
Helped
0
Reputation
0
Reaction score
0
Trophy points
1,281
Activity points
1,313
synopsys_translate_off

Anyone knows the tools that can synthesize the HDL to gate-level but preserve all the assertions? I need the assertion constraints at gate-level. I am new at design. Thanks
 

Assertions are a feature HDL of used by simulator for Functional verification.
Normally assertion are aplied on expression or on nets.
But After synthesis the net names are modified by the synthesis tools also assertion are ignored by sunthesis tool.
so i don't think same assertion can be used after synthesis provided u keep assertions in Test Bench.
In that case also the Net names and path has to be modffied.
Any other views on this.
 

This is exactly my problem. I want to keep tracing the constraints imposed by the assertions (in HDL) at gate level. But after synthesis these net names are modified. How can I preserve my assertion constraints at gate level?

I am trying to do this for test purpose, since ATPG can only be done at gate level. If I need to apply the assertion constraints in ATPG, how can I find them after synthesis?

Thanks
 

Which Synthesis tool you are using,
I know in DC Shell i had written SVA and i put under synopsys_translate_off directive.
and in magma it is "synthesis off" directive.
 

Assertions are only for simulation and formal verification. "Translate_on" and "Translate_of" are only pragmas (directives for synthesiser to translate or not to translate code).
 

No tool will preserve assertions as assertions are not synthsizable
 

mliu66 said:
This is exactly my problem. I want to keep tracing the constraints imposed by the assertions (in HDL) at gate level. But after synthesis these net names are modified. How can I preserve my assertion constraints at gate level?

I am trying to do this for test purpose, since ATPG can only be done at gate level. If I need to apply the assertion constraints in ATPG, how can I find them after synthesis?

Thanks

Couple of notes:

1. This signal name change is more of Synthesis issue and has been known for long now. Nothing new with assertions.
2. Typically FF/latch elements tend to stay around even after synthesis and only combo logic gets optimized away. So in our book we recommend that for those assertions that are likely to be reused at gate level, write them on state elements (FF, latches) and use `define so that we can redfine them for gate level - exactly addressing this issue that you are bringining in.

3. I didn't understand how you want to use them as "constraints" in ATPG etc.

4. Assertions are synthesizable - or atleast there is a subset of them that are. That's how some formal tools do it - Just FYI

HTH
Ajeetha, CVC
www.noveldv.com
 

I use in assertions net within block and I want to run this assertion at gate level. How we can solve changing names of nets at netlist?
 

Status
Not open for further replies.

Part and Inventory Search

Welcome to EDABoard.com

Sponsor

Back
Top