( ESNUG 356 Item 3 ) --------------------------------------------- [8/03/00]
Subject: ( ESNUG 355 #3 ) Verplex, Synopsys Formality, and Scan/BIST/JTAG
> I was considering using formal verification. However some questions came
> to mind on how it actually works.
>
> Internal scan and boundary scan were inserted into the design using Test
> Compiler. At this point is it not true that the RTL and the gate netlist
> are no longer functionally equivalent? Does formal verification handle
> this effectivively. Also my ASIC vendor required that the ATPG vectors
> and a subset of the functional vectors be simulated at gate level using
> estimated pre-route delay for min and max conditions. So I had to spent
> a lot of CPU time doing simulations anyway. Is top level design
> verification the proper place for formal verification?
>
> - Lou Villarosa, Jr.
> Paradyne Corporation
From: Scott Evans <scott@sonicsinc.com>
When I used the Verplex software it handled it just fine. You had to tie
off the scan enable so functionally it becomes equivalent to the original
circuit. Not sure how the other formal tools handle this but I'm sure it
is similar.
- Scott Evans
Sonics Inc. Mountain View, CA
---- ---- ---- ---- ---- ---- ----
From: London Jin <jinl@taec.toshiba.com>
Hi John,
There are three modes in a design with JTAG and internal scan. They are
mission mode, JTAG mode, and scan mode.
Mission mode, namely, this is the mode you do not see JTAG logic and
internal scan paths. In other words, JTAG logic and scan paths are
transparent. How to get you to this mode? JTAG logic should be
transparent by default (IEEE 1149.1 Standard). You better verify your
TAP controller if your design does not behave in that way. You can force
your design to the mission mode by A) controlling the TRST pin (TRST =0)
if you have this pin, asynchronous reset; or B) controlling TMS = 11111
with 5 TCK's (synchronous reset) if you do not have TRST pin.
The way to control internal scan to get you to mission varies from scan
style to scan style. You need to control the scan enable pin if you use
MUXed-scan style so that it selects system data on the MUXed-scan cells.
With the above control, the design with both JTAG & internal scan should
be functional equivalent to the design without JTAG & internal scan.
That is how you run formal verification.
Regarding to ATPG vector simulation, please note that: 1) ATPG vectors
are generated in scan mode, not in mission mode; 2) ATPG vectors are
generated with the goal of fault detection, not the goal of functional
verification, although ATPG has to understand your logic to simulate the
fault effect.
- London Jin
Toshiba San Jose, CA
---- ---- ---- ---- ---- ---- ----
From: Erik Jessen <Erik.Jessen@Vixel.com>
Hi, John,
1) The final netlist should be logically equivalent to RTL, if scan/JTAG/
/nand-tree/BIST are all disabled. So you just need to do that in your
equivalency-checker script (my Verplex script for comparing a million-
gate ASIC (RTL v. final gates, with NAND-tree, JTAG, 8-chains of scan
with multiple clock domains is about 20 lines long, with 1 line per
JTAG/NAND/etc. to disable them).
2) You still need to simulate a subset of functional vectors, to make sure
that you didn't blow it in your static timing analyzer (it happens, esp.
if you missed a clock-domain interface)
3) You need to simulate a subset of scan vectors for the same reason
4) Definitely do equivalency checking! Our runs are around an hour, and
100% verify that the entire chip. How long would it take for you to
run ALL your sims at gate level? Days? Weeks? And you still would
only catch the bugs that you simulated, and watched for (so maybe 70%
of your design is tested).
We've caught problems with EC due to synthesis bugs, or due to places where
somebody had `ifdef in their RTL, hardcoding what gates to use, and the
gates didn't exactly match the functionality of the RTL. We might not have
caught this in sims, but Verplex definitely did.
- Erik Jessen
Vixel Corp.
---- ---- ---- ---- ---- ---- ----
From: Shamai Eisenmann <shamai@tiogatech.com>
Hi John,
You can set an input to a specific value in most EC tools. Set your
scan_enable and/or scan_mode pins to 0 (i.e. disable the scan chain) and
then your deign should be equivalent to the RTL.
- Shamai Eisenmann
Tioga Technologies
---- ---- ---- ---- ---- ---- ----
From: Pierre Monteil <pierre.monteil@st.com>
Hi John,
You have just to remove your scan outputs, and to force your scan_enable to
logic 0.... If you use Synopsys Formality, it can be a good way to reduce
run-time to remove local scan on each sub-bloc:
foreach all_blocs [ find_references CONT:/LIB_NAME/* -hier ] {
current_design $all_blocs
echo "design : $all_blocs
foreach scan_port [find_ports $scan_enable] {
set_constant -type port $scan_port 0
}
foreach scan_port [find_ports $scan_out] {
remove_object -type port $scan_port
}
}
On core design, we earn weeks of simulation... More than that, equivalence
checking is very fast for verifying automated/manual IPO.
- Pierre Monteil
ST Microelectronics Grenoble, France
---- ---- ---- ---- ---- ---- ----
From: [ Synopsys Support ]
John,
In response to this (ESNUG 355 Item 3), since I have done it may a time:
Set up your formal verification run so it is checking mission mode (Disable
scan & JTAG logic by setting proper values on SCAN_ENABLE and TMS/TDI)
using set_constant on the implementation design (POST SCAN netlist) then
perform the formal verification. This will verify that the mission mode
logic was not upset by the scan/JTAG insertion. JTAG & Scan functionality
will still have to be verified with vectors.
After this pass do not set any constants this will perform formal
verification on test mode & mission mode. Setting the constants is only
required for pre-scan vs. post-scan verification.
- [ Synopsys Support ]
|
|
