next up previous
Next: Results Up: MINIMALIST: An Environment for Previous: Verifier

A Synthesis Session

$ MinShell# Start the MINIMALIST shell

minimalist> help# Show list of commands

    assign-states            break             call               cd

         continue           define             echo             expr

              for             help               if    impymin-logic

    make-testable        min-logic       min-states              pwd

             quit        read-spec              set     set-encoding

  set-state-cover    show-encoding       show-logic           source

     verify-logic            while       write-flow    write-instant

       write-spec   write-symbolic      write-trans

 

minimalist> pwd# Show current directory

/u/minimalist/demo

 

minimalist> ls# Run 'ls'

bin  ex   lib

 

minimalist> ls ex

dme-e        dram-ctrl    pe-send-ifc  scripts      stetson

dme-fast-e   hp-ir        pscsi        scsi-iccd92

 

minimalist> cd ex/dme-e# Move to another directory

 

minimalist> ls

dme-e.bms

 

minimalist> help read-spec# Show syntax of 'read-spec'

        read-spec [-v] <file> [<spec-var>]

Read the Burst-Mode specification in <file> and store it in <spec-var>,

or, if <spec-var> is not specified, 'theSpec'.

 

minimalist> read-spec dme-e.bms# Read the Burst-Mode specification

Specification passed validity check.

Specification has 3 inputs, 3 outputs, and 8 states.

 

minimalist> plot_graph dme-e.bms

[... a window displays the burst-mode graph; press Ctrl-Q or the Quit button to dismiss it ...]

 

minimalist> min-states# Perform state minimization

*** Performing state minimization... ***

State cover: { { S0 S1 S4 }, { S2 S3 }, { S5 S6 S7 } }

Machine has 3 states after minimization.

 

minimalist> assign-states -F# Assign states with a CRF encoding

No encoding style specified; defaulting to critical race-free

*** Performing state assignment... ***

Invoking 'chasm' as 'chasm -C DME_E-F.func DME_E-F.trans'

*** Machine encoded by CHASM ***

State S0': 11

State S1': 10

State S2': 00

 

minimalist> min-logic -F -L# Produce the logic implementation

*** Performing logic minimization... ***

Invoking 'hfmin' as 'hfmin -P -C -l -S -o DME_E-FL.sol DME_E-FL.pla DME_E-FL.btrans'

*** Final PLA ***

# PLA file for machine DME_E-FL

.i 8

.o 5

.ilb LIN RIN UIN LOUT_i ROUT_i UOUT_i Y0 Y1

.ob y0 y1 LOUT ROUT UOUT

.type fr

.p 7

10---1 00010

-01--1 00010

-0---1 01000

10---0 10100

00--1- 11000

-0--1- 10000

-01--0 00001

.e

Number of products:       7                       Total number of literals: 28

Number of products implementing outputs:      4   Literals in products implementing outputs: 17

Literals in products implementing next-state: 16  Average literals per output:          5.66667

Result stored in 'DME_E-FL.sol'.

 

minimalist> verify-logic -F -L# Verify the implementation

Using logic implementation stored in 'DME_E-FL.sol'.

*** Starting Burst-Mode machine simulation. ***

*** Implementation verified successfully! ***

 

minimalist> plot_graph DME_E-FL.sol# Display the implementation

[... a window displays the 2-level logic; press Ctrl-Q or the Quit button to dismiss it ...]

# Run the above synthesis steps using a script

 

minimalist> source ../scripts/script-FBO.MOL-CRF dme-e.bms

[... same results as above, without interaction ...]

 

minimalist> quit


next up previous
Next: Results Up: MINIMALIST: An Environment for Previous: Verifier
Steven Nowick
1999-07-28