Formality : Quick tutorial
Aviral Mittal, comments on formality@vlsiip.com
Connect @ https://www.linkedin.com/in/avimit/

Download Formality User Guide Here:

This tutorial has been designed into independent sections, so that
you can visit, read the one you think you need. For example if
you know what formality is, and you just want to use it, you may
go to section #, on the other hand if you would like to first know
what formality is, you may start from the appropriate section.


Pls Note this tutorial is being updated.

Introduction:

Why Use Formality:

How To Run Formality:

Some Commands:

Log Messages: Explanation

Tutorial Downloads:
RTL design files for synthesis subband filter used in mp3 decoder.
Design Compiler synthesis script for sdram controller
Script containing formality commands.
Single tar.gz file containing all above
Assumptions:
1. Design Compiler has been used for Synthesis




Notes about constant registers:

Once formality has matched two registers(by name or connections or any other way...),
It then tries to establish that two register will load same value, when all the nets/ports
which its D input depends upon, are the same.

Now consider a case where a design is being compared RTL(ref) vs Netlist(impl)
RTL may have registers which are classed as 'constants', which means that they will
never change their value, and hence the synthesis tool removes them during optimization.

Now in RTL say a regA is a constant, and RegB is f(RegA, x,y,z). i.e f=funcion of
Formality wont remove regA, and will try to put '0' and '1' both values to it, and evaluate
D of RegA. But as said regA is a constant, say it was a constant tied to '0'. Now here is a
problem. Formality will try to evaluate D of regB, putting Q of regA to '1', and it is very well
possible, that D of regB will get a different value due to Q of regA being '1' than what it would
be when Q of regA is '0'.
In reality Q of regA never goes to a '1' because its a constant '0'. In netlist, while comparing,
Q of regA doesn't appear, because it has been optimized away by synthesis tool.
Formality reports a failure under these circumstances.