Formality : Quick tutorial
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.