search

ADDER X-SC Manual de usuario Pagina 52

  • Descarga
  • Añadir a mis manuales
  • Imprimir
  • Pagina
    / 87
  • Tabla de contenidos
  • MARCADORES
    • Valorado. / 5. Basado en revisión del cliente
Vista de pagina 51
52 CHAPTER 1. INTRODUCTION TO THE ALLIANCE TOOLS
Table 1.22: Options Available for the proof Tool.
Option Description
-a
This option asks proof to keep the common auxiliary signals. Proof keeps all intermediate
signals that have the same name in both descriptions (A common signal is considered as
an input and an output of each desc ription). This option can be useful for descriptions
containing large equations. It may be used when proof has failed or if you want to debug
in step by step mode the two different descriptions.
-d
The program displays errors when the behavioral desc riptions are different. Equations are
displayed when it’s possible.
original b e havioral description of our multiplexer design with that obtained with BOOM.
% proof -a -d mux mux_o
@@@@@@@ @@@
@@ @@ @ @@
@@ @@ @@ @@
@@ @@ @@@ @@@ @@@ @@@ @@
@@ @@ @@@ @@ @@ @ @ @@ @@ @@@@@@@@
@@@@@ @@ @@ @@ @@ @@ @@ @@
@@ @@ @@ @@ @@ @@ @@
@@ @@ @@ @@ @@ @@ @@
@@ @@ @@ @@ @@ @@ @@
@@ @@ @@ @@ @@ @@ @@
@@@@@@ @@@@ @@@ @@@ @@@@@@
Formal Proof
Alliance CAD System 5.0 20040928, proof 5.0
Copyright (c) 1990-2005, ASIM/LIP6/UPMC
E-mail : [email protected]
================================ Environment ================================
MBK_WORK_LIB = .
MBK_CATA_LIB =.:/usr/local/alliance/cells/sxlib:/usr/local/alliance/cells/dp_sxlib:
/usr/local/alliance/cells/rflib:/usr/local/alliance/cells/romlib:/usr/local/alliance/cells/ramlib:
/usr/local/alliance/cells/padlib
======================= Files, Options and Parameters =======================
First VHDL file = mux.vbe
Second VHDL file = mux_o.vbe
The common auxiliary signals are kept
Errors are displayed
===============================================================================
Compiling ’mux’ ...
Compiling ’mux_o’ ...
Looking for the common auxiliary signals :
---> final number of nodes = 9(3)
Running Abl2Bdd on ‘mux_o‘
--------------------------------------------------------------------------------
Formal proof with Ordered Binary Decision Diagrams between
’./mux’ and ’./mux_o’
--------------------------------------------------------------------------------
============================== PRIMARY OUTPUT ===============================
============================= AUXILIARY SIGNAL ==============================
============================== REGISTER SIGNAL ==============================
=============================== EXTERNAL BUS =================================
================================ INTERNAL BUS =================================
Formal Proof : OK
pppppppppppppppppppppppprrrrrrrrrrrrooooooooooooooooooooooooooooofffffffffffffff
--------------------------------------------------------------------------------
As could be seen from this output proof check the equivalence of primary outputs, signals and buses in that
order. Internally proof uses a ROBDD (Reduced Ordered Binary Decision Diagram) to prove the equivalence
Vista de pagina 51
1 2 ... 47 48 49 50 51 52 53 54 55 56 57 ... 86 87

Comentarios a estos manuales

Sin comentarios
  • CTS Rogerblack Zypher Oriental Weavers Electra
  • Sony Gradas de equipos AV Compaq Navegadores Sega No Canon Impresoras De Etiquetas NewAir Enfriadores De Vino
  • Whirlpool WTNF 81I X Electrolux EOB203X Philips AJ7030D-37 Sony ST-SE520
  • Panasonic AG-DVC7P Manual de usuario Whirlpool AKP 139/IX Instrucciones de uso First Alert 2040F Manual de uso y cuidado Samsung F2380 Manual de usuario BIXOLON SRP-F312 Especificaciones