ADDER X-SC Manual do Utilizador descarregar pdf (Página 48)

48 CHAPTER 1. INTRODUCTION TO THE ALLIANCE TOOLS

Of course, in the case of this very simple design, there will be no changes in the description already gotten

with BOOG, since the cells of it did not change.

1.18 LVX

LVX (Logical Versus eXtracted) tool of Alliance let us compare two gate-level or block-level netlists. This tool

is used to compare a speciﬁcation (logical netlist) to the netlist extracted from a physical netlist. Using this tool

we can verify if the placement and routing of a logical design has been done correctly. Since this is a one-level

hierarchical tool we must use COUGAR to extract a netlist for comparison. We use LVX with the following

command.

lvx format1 format2 filename1 filename2 [ -a ] [ -o ] [ -f ]

The options available in LVX are shown in Table 1.18. If the option -f is used the two netlists are ﬂattened

Table 1.18: Options Available for the LVX Tool.

Option Description

-a

Some routers generate layout with several physical connectors for power and ground (VDD or

VSS). If those connectors are not internally connected, they will have diﬀerent indexed names

(VDD1 , VDD2 etc...) in the extracted netlist. It is possible to perform reduction on those

power and ground connectors before comparison, using the -a option. After reduction, each

instance contains only one VDD connector and one VSS connector, as the main ﬁgure.

-o

In this case , lvx produces a modiﬁed netlist (saved with the name ﬁlename2 ), which is a copy

of netlist 2 with ordered connectors. Terminals and instance connectors are relisted in the order

of the models in net-list 1. The saved netlist is done with the MBK OUT LO(1) format, so user

has to set this variable before running lvx . If he does not, default value is used, and netlist 1

could be lost if ﬁlename are identical and input format same as output format. If -a option is

used, then the saved net-list is the reduced net-list with only one VDD and one VSS .

-f

The two netlists are ﬂattened to the leaf cells contained in the catalog ﬁle. Usually the extracted

netlist is a ﬂatten netlist, while the logical one can be a hierarchical net-list.

using the values of the environment variables MBK CATA LIB and MBK WORK LIB. MBK CATA LIB in-

dicates the path to the cell library catalog ﬁle, and MBK WORK LIB the path where the ﬁle indicated by

MBK CATAL NAME indicates the user blocks that must not be ﬂattened.

LVX compares external connectors names, instances names, names of connections and unconnected signals,

in this order. If connector or instance names do not match LVX stops with an error. It will not compare signals

if terminal or instance names diﬀer.

We have already seen an example of application of LVX in the section of COUGAR, so will skip it here.

1.19 MOKA

The MOKA (MOdel checKer Ance stor) tool of Alliance let’s check an FSM or RTL description using a list of

formulae described in a CTL (Control Temporal Logic) ﬁle. MOKA has some restrictions. It needs that all

the register in the behavioral description have the same clock condition and doesn allows the use of tristate or

multiplexed buses (The mux bit and wor bit are not supported). We use MOKA with the following command.

% moka [-VDB] fsmfile ctlfile

The options available in MOKA are s hown in Table 1.19. Let’s use MOKA on the example provided for this

Table 1.19: Options Available for the MOKA Tool.

Option Description

-V

Sets verbose mode on.

-D

Sets debug mode on. Each step of the model checking is detailed on the standard output.

In particular all states set are displayed for each CTL sub-expression.

-B

The input ﬁle is a VHDL description using the Alliance VHDL subset

1 2 ... 43 44 45 46 47 48 49 50 51 52 53 ... 86 87

Comentários a estes Manuais

Sem comentários

ADDER X-SC Manual do Utilizador Página 48

Comentários a estes Manuais