Black Boxes: hdlin_unresolved_modules
Formality tcl variable that determines how to
handle instances that are not resolved
Possible values are ‘error’ and ‘black_box’
‘error’ means no design is created (default value)
‘black_box’ means Formality creates a black box
The default value of error
Prevents you creating black boxes by mistake
Prevents verification from proceeding
Set_top will error out if there is an unresolved module
If set_top errors out all subsequent steps error out too
Formality 2005.09
4a- 10
12
Black Boxes: why is an instance unresolved?
Formality cannot find a corresponding module/entity
File is missing or you typed in wrong file name
File name and VCS options don’t match
The file for the module or entity contains
syntax errors
unsupported constructs
The instance and the module/entity are inconsistent
Pinout doesn’t match
Formality analysis shows risk of simulation/synthesis
mismatch
(By default) Formality will not create a model
See Section 4b for details
Formality 2005.09
4a- 11
13
Setting a Black Box property
You can set/unset the black_box property on a
design in either the REF or IMP or both
Inputs will become new compare points, outputs will
become new cone inputs
set_black_box r:/WORK/mod
remove_black_box r:/WORK/mod
report_black_boxes “mod” is the
design name, not
the instance name
Formality 2005.09
4a- 12
14
Black Boxes: Specifying Pin Directions
Tell Formality about the directions of black box pins:
Find the code for the missing cell and read it in
Find the code for the missing cell and read in only the
interface information (hdlin_interface_only)
Alternative: create a dummy definition for the black box cell
containing the input and output port declarations but
containing no logic
Read this cell into Formality so that it knows the directions of
the pins
Last Resort: Use the set_direction command to set the pin
directions on unresolved modules
set_direction r:/WORK/mAlu/reg[0] out
Formality 2005.09
4a- 13
15
Finding Black Boxes using fm_shell
fm_shell (setup)> report_black_box
Information: Reporting black boxes for current reference and implementation designs.
(FM-184)
__________________________________________________
| |
| Legend: |
| Black Box Attributes |
| s = Set with set_black_box command |
| i = Module read with -interface_only |
| u = Unresolved design module |
| e = Empty design module |
| * = Unlinked design module |
|___________________________________________________|
##################################################################
#### DESIGN LIBRARY - i:/WORK
##################################################################
Design Name Attributes
----------- ----------
sRAM01 s
##################################################################
#### DESIGN LIBRARY - r:/WORK
##################################################################
Design Name Attributes
----------- ----------
sRAM01 i
Formality 2005.09
4a- 14
17
Finding Black Boxes with the GUI
Formality 2005.09
4a- 15
19
Black Box Summary
Method Command / Variable report_black_box
shows as
Read a Empty Module
Wrapper
Read in the hdlin_interface_only Interface Only
interface only
Set a property set_black_box Set with command
after reading in
(remove_black_box undoes)
Don’t read in hdlin_unresolved_modules Unresolved Design
the design Module
(may need set_direction too?)
Formality 2005.09
4a- 16
21
Review Questions
1. List 4 ways of creating a black box model
2. Which commands or variables would you use for
each of these 4 ways?
3. Give two reasons why allowing Formality to create
black boxes for unresolved modules can result in
a failing verification
4. How would you find black boxes from the
command line?
5. How would you find black boxes using the GUI?
Formality 2005.09
4a- 17
22
Command/Variable Summary
set hdlin_interface_only Following read operations
<Design Name(s)> will read only the interface
declaration for the design
set hdlin_unresolved_modules Determines how unresolved
<error | black_box > modules are handled
set_black_box <design> Set a black box property on
a design
remove_black_box <design> Removes a black box
property from a design
report_black_box Lists black boxes and
shows source of black box
set_direction <pin> Set pin direction on a black
box (use on unresolved
modules)
Formality 2005.09
4a- 18
23
Day 1 Agenda
DAY 1 Introduction to Formality
1
2 Getting Started with Formality
3 Basic Formality Flow
4b Reading Designs: Sim/Synth Warnings
5 Matching
6 Verification
Formality 2005.09
4b- 1
Unit Objectives
After completing this unit, you should be able to:
List the three categories of causes for simulation/synthesis
differences
Name three tools that will warn you of potential
simulation/synthesis differences
Override simulation/synthesis mismatch warnings in
Formality
Name the DC and Formality variable that controls how out of
range array accesses are handled and explain its operation
Name the two DC pragmas that can give simulation/synthesis
differences when used inappropriately
Explain when/how these two pragmas can give
simulation/synthesis differences
Explain how you would check Formality warnings of
simulation/synthesis mismatches
4b- 2