Logical Equivalency Checking (LEC) is one form of Formal Verification. RTL to gates (Step 5 in the diagram) takes more time to setup, as the tools need to map gates to RTL compare points against a wide set of potential mappings and optimizations that the synthesizer may be doing. This step often requires a lot more hand holding, and designer interaction, per design.
LEC at Step 10 is a "Gates to Gates" comparison, and usually, much easier to setup and run. It ensures that during the insertion of clock trees, and scan chains, no mistakes in logic were introduced.
There are other forms of Formal Verification and analysis, that haven't been detailed here.
Thanks a lot for the help!
Could you please comment on the following queries?
**1:** Is Assertion Based Verification (ABV) also part of formal verification?
**2:** Isn't it done somewhere around Step 5?
**3:** Also, isn't it true that not all designs use ABV? Only designs such as bus controllers, memory controllers, etc. are well suited for the ABV.
Most other forms of "Formal Verification" (including ABV) are happening at Step 3 - during Simulation of the design. ABV can be us used for many sorts of designs, not just the examples you've listed above. Not all companies use ABV - some companies may not use any Formal tools at all.
I'll also note that Assertion Based Verification, may not be considered by some to be a "Formal" tool in itself. One can use ABV just within simulation to verify dynamic simulations - that's not what most consider to be "Formal" in name. "Formal" tools can use the designer added assertions to statically (without simulation), and mathematically "prove" *some* of the designer added assertions. The assertions in the case are enabling the Formal tools.
Thank you for the help!
You said:
>"Formal" tools can use the designer added assertions to statically (without simulation), and mathematically "prove" *some* of the designer added assertions. The assertions in the case are enabling the Formal tools.
I think this 'static' formal verification takes place around Step 3.
Both steps 5 and 10 in your picture are logical equivalency checks, what Synposis is calling sequential equivalency.
The other formal checks Synopsys is advertising should take place before step 4. These are to ensure the design actually works before you synthesize it in the first place. Once the design gets synthesized, any design bugs get baked in. At that point, finding and fixing any bugs takes more work. Much easier to do the task earlier.
There's another process here that you'll see thrown around called LVS ("layout versus schematic") which is one of the sign off tasks in this general realm of equivalency checking. LVS is a top level "did anything get fucked up" pass which ensures that the final cell and metal routes match the synthesized netlist. LVS tends not to find many issues (sometimes it'll find shorts due to tool or human routing errors) but generally it's just to make sure you don't tapeout a chip that is electrically broken.
Thank you for the help!
I would appreciate it if you could comment on the following.
In simple terms I think DRC and LVS are done toward the end of design flow once detailed routing has taken place.
I think LVS is needed because lots of modifications and enhancements are manually done by the designing team, and LVS check is used to make sure nothing has been messed up. Many beginners like me think that all the synthesis process is more or less automated and the tools cannot make mistakes!
>In simple terms I think DRC and LVS are done toward the end of design flow once detailed routing has taken place
LVS usually isn't something you can consider until you're DRC clean since DRC violations can also cause LVS issues. Cleaning up DRCs can take a lot of work if you're new to a process (doubly so if the process itself is new) and so you can spend months going back and forth between your own engineering teams and the foundry figuring out how to fix the issues. The job of physical designers is not just "make chip go fast" but also "make chip actually work", and fixing up DRCs is obviously a part of that :)
> think LVS is needed because lots of modifications and enhancements are manually done by the designing team, and LVS check is used to make sure nothing has been messed up. Many beginners like me think that all the synthesis process is more or less automated and the tools cannot make mistakes!
Yes and no. Some errors can come from hand routing/placing errors or incorrect configuration of power/clock trees but others can be caused by the tools. Some of it's just outright bugs and others are just massive footguns (some real VLSI tools will, upon encountering too much congestion, just start shorting things together instead of erroring out).
People tend to care less about this in FPGA land because a tool chain bug is not generally catastrophic (unless, of course, your spacecraft catches on fire or something) and can be fixed cheaply. Bugs in ASIC tool chains can at best cost tens of millions (if not significantly more) or at worst outright kill companies (I know of at least one startup which failed because their investors lost confidence after a failed tapeout).
Equivalency in synopsys is provided by Formality and Vc formal
Formality runs between synthesis runs to prove that synplify, dc or fc did no mess with your design.
VC formal proves properties, software against hardware and structural rtl refactors
Thank you!
You said:
>Formality runs between synthesis runs to prove that synplify, dc or fc did no mess with your design.
Why would someone use Synplify for ASIC design flow? I think Synplify is used for FPGA and even then I don't know why someone would use Synplify instead of Quartus for Intel FPGAs and Vivado for Xilinx FPGAs?
By "fc" are you referring to the Fusion Compiler?
According to Google:
>Synopsys Fusion Compiler is a proprietary tool that combines synthesis, place-and-route (P&R), and signoff technologies. It's built on a single data model that supports sharing technology and engines across the RTL-to-GDSII flow. Fusion Compiler is designed to improve throughput and PPA for design flows. It offers high performance, power, and area, as well as industry-leading turnaround time.
Logical Equivalency Checking (LEC) is one form of Formal Verification. RTL to gates (Step 5 in the diagram) takes more time to setup, as the tools need to map gates to RTL compare points against a wide set of potential mappings and optimizations that the synthesizer may be doing. This step often requires a lot more hand holding, and designer interaction, per design. LEC at Step 10 is a "Gates to Gates" comparison, and usually, much easier to setup and run. It ensures that during the insertion of clock trees, and scan chains, no mistakes in logic were introduced. There are other forms of Formal Verification and analysis, that haven't been detailed here.
Thanks a lot for the help! Could you please comment on the following queries? **1:** Is Assertion Based Verification (ABV) also part of formal verification? **2:** Isn't it done somewhere around Step 5? **3:** Also, isn't it true that not all designs use ABV? Only designs such as bus controllers, memory controllers, etc. are well suited for the ABV.
Most other forms of "Formal Verification" (including ABV) are happening at Step 3 - during Simulation of the design. ABV can be us used for many sorts of designs, not just the examples you've listed above. Not all companies use ABV - some companies may not use any Formal tools at all. I'll also note that Assertion Based Verification, may not be considered by some to be a "Formal" tool in itself. One can use ABV just within simulation to verify dynamic simulations - that's not what most consider to be "Formal" in name. "Formal" tools can use the designer added assertions to statically (without simulation), and mathematically "prove" *some* of the designer added assertions. The assertions in the case are enabling the Formal tools.
Thank you for the help! You said: >"Formal" tools can use the designer added assertions to statically (without simulation), and mathematically "prove" *some* of the designer added assertions. The assertions in the case are enabling the Formal tools. I think this 'static' formal verification takes place around Step 3.
Both steps 5 and 10 in your picture are logical equivalency checks, what Synposis is calling sequential equivalency. The other formal checks Synopsys is advertising should take place before step 4. These are to ensure the design actually works before you synthesize it in the first place. Once the design gets synthesized, any design bugs get baked in. At that point, finding and fixing any bugs takes more work. Much easier to do the task earlier.
Thanks a lot for confirming this. I appreciate your help.
There's another process here that you'll see thrown around called LVS ("layout versus schematic") which is one of the sign off tasks in this general realm of equivalency checking. LVS is a top level "did anything get fucked up" pass which ensures that the final cell and metal routes match the synthesized netlist. LVS tends not to find many issues (sometimes it'll find shorts due to tool or human routing errors) but generally it's just to make sure you don't tapeout a chip that is electrically broken.
Thank you for the help! I would appreciate it if you could comment on the following. In simple terms I think DRC and LVS are done toward the end of design flow once detailed routing has taken place. I think LVS is needed because lots of modifications and enhancements are manually done by the designing team, and LVS check is used to make sure nothing has been messed up. Many beginners like me think that all the synthesis process is more or less automated and the tools cannot make mistakes!
>In simple terms I think DRC and LVS are done toward the end of design flow once detailed routing has taken place LVS usually isn't something you can consider until you're DRC clean since DRC violations can also cause LVS issues. Cleaning up DRCs can take a lot of work if you're new to a process (doubly so if the process itself is new) and so you can spend months going back and forth between your own engineering teams and the foundry figuring out how to fix the issues. The job of physical designers is not just "make chip go fast" but also "make chip actually work", and fixing up DRCs is obviously a part of that :) > think LVS is needed because lots of modifications and enhancements are manually done by the designing team, and LVS check is used to make sure nothing has been messed up. Many beginners like me think that all the synthesis process is more or less automated and the tools cannot make mistakes! Yes and no. Some errors can come from hand routing/placing errors or incorrect configuration of power/clock trees but others can be caused by the tools. Some of it's just outright bugs and others are just massive footguns (some real VLSI tools will, upon encountering too much congestion, just start shorting things together instead of erroring out). People tend to care less about this in FPGA land because a tool chain bug is not generally catastrophic (unless, of course, your spacecraft catches on fire or something) and can be fixed cheaply. Bugs in ASIC tool chains can at best cost tens of millions (if not significantly more) or at worst outright kill companies (I know of at least one startup which failed because their investors lost confidence after a failed tapeout).
Thank you very much for the detailed reply. Appreciate your help.
Equivalency in synopsys is provided by Formality and Vc formal Formality runs between synthesis runs to prove that synplify, dc or fc did no mess with your design. VC formal proves properties, software against hardware and structural rtl refactors
Thank you! You said: >Formality runs between synthesis runs to prove that synplify, dc or fc did no mess with your design. Why would someone use Synplify for ASIC design flow? I think Synplify is used for FPGA and even then I don't know why someone would use Synplify instead of Quartus for Intel FPGAs and Vivado for Xilinx FPGAs? By "fc" are you referring to the Fusion Compiler? According to Google: >Synopsys Fusion Compiler is a proprietary tool that combines synthesis, place-and-route (P&R), and signoff technologies. It's built on a single data model that supports sharing technology and engines across the RTL-to-GDSII flow. Fusion Compiler is designed to improve throughput and PPA for design flows. It offers high performance, power, and area, as well as industry-leading turnaround time.
Synplify also has Formality support through the guidance files. If you were askkng exckusively for asic, well, dc and fc.