
                 @@@     @@@                       @           
                  @@     @@                       @@@          
                  @@@   @@@                        @           
                  @@@   @@@    @@@@      @@@@@@           @@@  
                  @ @@ @ @@   @@   @    @@  @@  @@@@    @@   @@
                  @ @@ @ @@   @@   @@   @   @@    @@   @@     @
                  @ @@@  @@     @@@@@   @   @     @@   @@      
                  @  @@  @@   @@   @@    @@@      @@   @@      
                  @  @   @@  @@    @@   @@        @@   @@     @
                  @      @@  @@   @@@   @@@@@@    @@    @@   @@
                 @@@    @@@@  @@@@  @@ @@   @@@ @@@@@@    @@@  
                                        @     @                
                                         @@@@@                 

                      Behavioural formal proof is not Magic

                   Alliance CAD System 3.0,       magic 1.160
                   Copyright (c) 1995-96, MASI, CAO-VLSI Team
                   E-mail support:       cao-vlsi@masi.ibp.fr


============================ Command line and files =========================

---> Command line : magic -d exemplea exemplea 
---> Using './exemplea.vbe' as first VHDL input file (fig1)
---> Using './exemplea.vbe' as first VHDL input file (fig2)
---> Using 'reset' as RESET signal. (Reset active HI)


============================ Loading Beh Figures ============================

===> Compiling 'exemplea' ...
     Stats :
          Fig type : Sequential
            Inputs : 3
         Registers : 2
           Outputs : 1
   Generation func : 3
   Transition func : 12
Befig 'exemplea(fig1)' (exemplea.vbe) loaded.

===> Compiling 'exemplea' ...
     Stats :
          Fig type : Sequential
            Inputs : 3
         Registers : 2
           Outputs : 1
   Generation func : 3
   Transition func : 12
Befig 'exemplea(fig2)' (exemplea.vbe) loaded.

===> Using sequential formal proof.

============================ Verifying Ports ================================

===> Verifying Port declaration.

exemplea(fig1) befig :
################################# BEPOR list
BEPOR : o, 	 dir : O, 	 type : B
BEPOR : i, 	 dir : I, 	 type : B
BEPOR : reset, 	 dir : I, 	 type : B
BEPOR : ck, 	 dir : I, 	 type : B
################################# BERIN list
BERIN : ck'delayed
BERIN : cs 1
BERIN : cs 0
BERIN : i
BERIN : reset
BERIN : ck
################################# BEOUT list
BEOUT : o
################################# BEREG list
BEREG : cs 1
BEREG : cs 0
################################# BEAUX list
################################# BEBUS list
################################# BEBUX list
################################# BEDLY list
BEDLY : ck'delayed


===> Verifying Delayed signals.

============================ Renaming fig2 Rgisters =========================

===> Renamed 2 registers in 'exemplea(fig2)' whith prefix 'fig2_'.

============================ Making Bdds ====================================

===> Making Bdds, removing auxiliary signals.
===> Bdd system created (59 bdd nodes).

============================ Verifying Conditions ============================

===> Verifying Condition on registers.
cs 1 [fig 1] <= (NOT((ck'STABLE)) AND ck)
cs 0 [fig 1] <= (NOT((ck'STABLE)) AND ck)
fig2_cs 1 [fig 2] <= (NOT((ck'STABLE)) AND ck)
fig2_cs 0 [fig 2] <= (NOT((ck'STABLE)) AND ck)

============================ Searching Initial State ========================

===> Using signal 'reset' to compute initial state. (Reset active HI)
'reset' a '1' implique  'cs 1' <= '0'
'reset' a '1' implique  'cs 0' <= '1'
'reset' a '1' implique  'fig2_cs 1' <= '0'
'reset' a '1' implique  'fig2_cs 0' <= '1'

Initial state of product machine :
(NOT(cs(1)) AND cs(0) AND NOT(fig2_cs(1)) AND fig2_cs(0))


============================ Running Formal Proof ============================

===> Running Formal Proof.
TransFunc
  MAX_VAR    : 4
  NUMBER_VAR : 4
  VAR_FUNC[ 0 ] : 
VAR : cs(1)
FUNC: ((((cs(1) OR cs(0)) AND NOT(i)) OR (NOT(cs(1)) AND i)) AND NOT(reset))
  VAR_FUNC[ 1 ] : 
VAR : cs(0)
FUNC: (((NOT(cs(1)) OR NOT(cs(0))) AND NOT(i)) OR (NOT(cs(1)) AND NOT(cs(0))) OR 
reset)
  VAR_FUNC[ 2 ] : 
VAR : fig2_cs(1)
FUNC: ((((NOT(reset) AND NOT(fig2_cs(1))) OR (NOT(i) AND NOT(reset))) AND fig2_cs(0))
 OR (i AND NOT(reset) AND NOT(fig2_cs(1))) OR (NOT(i) AND NOT(reset) AND 
fig2_cs(1)))
  VAR_FUNC[ 3 ] : 
VAR : fig2_cs(0)
FUNC: (((NOT(i) OR reset OR NOT(fig2_cs(1))) AND NOT(fig2_cs(0))) OR ((NOT(i) OR 
reset) AND NOT(fig2_cs(1))) OR reset)
######## 
nodes proof debut : 41

Image disjointe 0 :
*01***01
(NOT(cs(1)) AND cs(0) AND NOT(fig2_cs(1)) AND fig2_cs(0))

Image Set 1 :
*11***11
*01***01
*10***10
((cs(1) AND NOT(cs(0)) AND fig2_cs(1) AND NOT(fig2_cs(0))) OR (((NOT(cs(1)) AND
 cs(0) AND NOT(fig2_cs(1))) OR (cs(1) AND cs(0) AND fig2_cs(1))) AND fig2_cs(0))
)

Image disjointe 1 :
*11***11
*10***10
((cs(1) AND NOT(cs(0)) AND fig2_cs(1) AND NOT(fig2_cs(0))) OR (cs(1) AND cs(0) 
AND fig2_cs(1) AND fig2_cs(0)))


Image Set 2 :
*11***11
*01***01
*10***10
*00***00
((((NOT(cs(1)) AND NOT(cs(0)) AND NOT(fig2_cs(1))) OR (cs(1) AND NOT(cs(0)) AND
 fig2_cs(1))) AND NOT(fig2_cs(0))) OR (((NOT(cs(1)) AND cs(0) AND NOT(fig2_cs(1)
)) OR (cs(1) AND cs(0) AND fig2_cs(1))) AND fig2_cs(0)))

Image disjointe 2 :
*00***00
(NOT(cs(1)) AND NOT(cs(0)) AND NOT(fig2_cs(1)) AND NOT(fig2_cs(0)))


Image Set 3 :
*11***11
*01***01
(((NOT(cs(1)) AND cs(0) AND NOT(fig2_cs(1))) OR (cs(1) AND cs(0) AND fig2_cs(1)
)) AND fig2_cs(0))

nodes proof fin : 46

============================ Result Summary =================================

===> Formal proof between figures
     exemplea(fig1) : ./exemplea.vbe [Sequential]
     exemplea(fig2) : ./exemplea.vbe [Sequential]

===> Formal Proof OK

===> Started on Sat Sep 14 02:47:25 1996
     Total elapsed time : 0.08 sec
        Time Making Abl : 0.00 sec
       Time Making Bdds : 0.00 sec
     Time Running Proof : 0.08 sec
   Time Making Patterns : 0.00 sec
      Time Max Bdd Node : 183 nodes

===> Total number of warning : 0

                   @@@@@@@          @        @@@@ @    @@@@ @ 
                     @@   @@        @       @    @@   @    @@ 
                     @@    @@      @@@     @@     @  @@     @ 
                     @@    @@      @@@     @@@       @@@      
                     @@   @@      @  @@     @@@@      @@@@    
                     @@@@@        @  @@       @@@@      @@@@  
                     @@          @    @@        @@@       @@@ 
                     @@          @@@@@@@   @      @@ @      @@
                     @@         @      @@  @@     @@ @@     @@
                     @@         @      @@  @@@    @  @@@    @ 
                   @@@@@@     @@@@    @@@@ @  @@@@   @  @@@@  

