search

ADDER X-SC Instrukcja Użytkownika Strona 41

  • Pobierz
  • Dodaj do moich podręczników
  • Drukuj
  • Strona
    / 87
  • Spis treści
  • BOOKMARKI
    • Oceniono. / 5. Na podstawie oceny klientów
Przeglądanie stron 40
1.12. FSP 41
1.12 FSP
The FSP (Finite State machine Proof) tool checks the equivalence of two FSM descriptions. It does it formally
using a product based algorithm. We use this tool with the following command.
% fsp [-V] format1 format2 file1 file2
The options available in FSP are shown in Table 1.13. Let’s apply it to the fsm descriptions we got in the
Table 1.13: Options Available for the FSP Tool.
Option Description
-V
Verbose mode. Each step of the formal proof is displayed.
examples using B2F and FMI.
% fsp -V fsm fsm rwgraph rwmin
@@@@@@@@@ @@@@ @ @@@@@@@
@@ @ @ @@ @@ @@
@@ @ @@ @ @@ @@
@@ @@@ @@ @@
@@ @ @@@@ @@ @@
@@@@@@ @@@@ @@@@@
@@ @ @@@ @@
@@ @ @@ @@
@@ @@ @@ @@
@@ @@@ @ @@
@@@@@@ @ @@@@ @@@@@@
FSM formal Proof
Alliance CAD System 5.0 20040928, fsp 5.0
Copyright (c) 1999-2005, ASIM/LIP6/UPMC
Author(s): Ludovic Jacomme
E-mail : [email protected]
--> Run FSM Compiler
--> Compile file rwgraph
--> Run FSM Compiler
--> Compile file rwmin
--> Formal proof between "rwgraph.fsm" and "rwmin.fsm"
==> "rwgraph.fsm" and "rwmin.fsm" are identicals
As could be noticed from the above output, the original FSM description obtained with B2F and the one
obtained with FMI are identical.
1.13 GENPAT
GENPAT (GENerator of PATterns) is a tool that is used to create a file of input patterns for ASIMUT. It is a C
interface (set of functions) that ease the creation of the input patterns. This tool inputs a C file describing the
input patterns and generates as output a .pat file. As in other tools the extension is not given at the command
input. As we explained in the section describing ASIMUT a .pat file can be easily edited for small circuits,
but it becomes complicated for complex design. GENPAT is intended to automate this editing work. We use
GENPAT with the following command.
% genpat [-v] [-k] [file]
The options available in GENPAT are shown in Table 1.14. We will try genpat generating the input patterns
Przeglądanie stron 40
1 2 ... 36 37 38 39 40 41 42 43 44 45 46 ... 86 87

Komentarze do niniejszej Instrukcji

Brak uwag
  • Crofton Legrand Seaboater Raynor Quirky
  • JVC Cyfrowe odtwarzacze multimedialne Hitachi Nawigatory FIELD CONTROLS Wentylatory domowe NEC Telewizory projekcyjne Roland Pompy wodne
  • Rane RPM 2 LG NB4530A Sony NEX-C3A SYBA SD-PCI15029 Electrolux ESF8585ROX
  • Brother IntelliFax-2820 Instrukcja Użytkownika Philips QC5350/80 Instrukcja Użytkownika Ariston ATD 104 Instrukcja Użytkownika Casio CDP-220R Podręcznik Hotpoint 25 Instrukcja Użytkownika