e-mail: kstevens@ece.utah.edu
MEAT -- The Most Excellent Asynchronous Tool, dudes! HISTORY This is part of a tool set that was developed here at Hewlett-Packard Labs to help with the development of a large 300,000 transistor asynchronous communication chip called the Post Office. During the initial design phase of the Post Office, Ken Stevens developed the burst-mode hazard model designed for high performance multiple-input-change and multiple-output-change asynchronous finite state machine implementation. The synthesis of these state machines was taking an inordinately large amount of time. The synthesis based on burst-mode was was done in a very "Unger-esque" style, and Ken figured the algorithms could be implemented in software. Grinding all the minimizations through by hand was also very error prone, and a tool would reduce these faults. Al Davis took the challenge and made Ken a bet that within 3 weeks given a sum of products specification as input he could output correct asynchronous covering using a Quine-McCluskey like algorithm. Well, he got it working, but tuning the performance to make it efficient took several months! Bill Coates hacked up some code that takes a state machine specification and generates the maximal compatibles. The user then selects the compatibles and his code will do the state assignment and output the unreduced logic equations. This is an Unger like reduction and uses the Tracey algorithm, and is a front end to the asynchronous logic minimizer. Ken hacked up a back-end to the Logic Minimization that does CMOS transistor minimization, and generates a schematic for the circuit. This was interfaced to the design tool we've been using called Electric(tm), and so it hasn't been included. If you are interested, we can send you the code that does the transistor minimization. Steve Nowick then came on as a summer student and interfaced the MEAT tool to Dave Dill's asynchronous verification tool called AVER. He also integrated the burst-mode hazard model into the version of AVER used at Hewlett-Packard for the implementation of the Post Office. (This version of AVER is not included with this software. Ask Ken if you want more details.) GETTING STARTED We have not compiled any of the files. To compile this system, execute the following command: (load "compile-meat") ---or--- (load "compile-meat.lisp") This will also load all of the files. After compiling the first time, you should just load all the files into your lisp environment by executing the following command: (load "load-meat") Oh, you will need to be connected to the directory that contains these files. USE We're happy to supply this code to you for your use, and feel free to call or send mail. However, as it was developed in the heat of building a prototype multiprocessor the documentation is very sparse (to say the least). However, soon this will change as we plan some papers and more general information on what we've done. The tool set contains a synchronous and asynchronous logic minimizer and state machine analyzer. USING THE MINIMIZER DIRECTLY The logic minimizer can be accessed directly by calling the functions (async-min-table) for asynchronous minimization, and (sync-min-table) for synchronous minimization. The interface to these functions is written for easy machine generation of the inputs and so that one can take the outputs from a Karnaugh map or other fully specified table. (Before Bill completed the state machine reduction, I entered all the inputs by hand using this interface! Ugh!) A logic equation interface once existed but has fallen into disrepair and totally disappeared as far as I know. The logic minimizer will reduce a single output variable at a time, so it will need to be called for each state variable or output individually. Here is a most bogus fabricated example: a \ c b \ d \ 00 01 11 10 \____________________ | | | | | 00 | 0 | X | 0 | X | |____|____|____|____| | | | | | 01 | 1 | 1 | 0 | X | |____|____|____|____| | | | | | 11 | 0 | 1 | 1 | 0 | |____|____|____|____| | | | | | 10 | 0 | X | X | 0 | |____|____|____|____| For the above Karnaugh map, the following is a transcript of a minimization session: > (async-min-table) Enter a parenthesized list of variable names for the function. -> the order is important! (a b c d) Enter the function table as a list in the order specified by the variable name list. The output function must be entered as a single list with 2**n elements, where 'n' is the number of input variables. Each element represents the output value of the function for a unique combination of inputs. Within the output vector, the elements are ordered in ascending binary sequence based on the input variable values, in the order they occur in the input list. For example, the output vector for a two-input function F = f(a,b) would be entered as (f(0,0) f(0,1) f(1,0) f(1,1)). Enter a 0 if the function is to be 0 at this point, 1 for a 1, and x for don't care. Also note that this *&^(*'ing read command limits line size... (0 x x 0 1 1 x 0 0 x 0 x 0 1 0 1) Doing Get-Pimps... Getting sync solutions..... Getting async solutions... *****The Following Are Asynchronous Solutions***** 38: C~*D + A*D + A~*B*C~ *****Asynchronous Minimization Done***** 38 > Note that the input to the minimizer is done such that the first element of the function list is the result of the output (or feedback variable) where all the inputs are zero (resulting in a logic 0 value if they were taken as a binary number). The second element of the function list is the resultant output when the the binary value of the inputs is 1, and so on increasing in value until all the inputs are 1's for the final element in the function list. Note that if you take the values from a K-map, as shown above, the values in the function list will not be the same order as displayed in the K-map. Be careful to input the values in the correct order or you will get unexpected results! Also note that the print routines specify a negated value as a variable name followed by a tilde. That is because the and terms are delimited by the asterisk and the or terms by the plus. SPECIFYING A STATE MACHINE FOR MEAT Here is a brief description of the valid entries in the state machine description file: Field documentation :fsm NAME Name of the state machine. :in LIST List of valid input names. :out LIST List of valid output names. :init-in BOOLEAN-LIST Boolean expression of value of inputs initially. Default is zero. For example, if there are four inputs and a and d are initially 1, then you could express this as either :init-in (a * d) or :init-in (a * b~ * c~ * d) :init-out BOOLEAN-LIST Same as for :init-in. :init-state NUM The initial state (a decimal integer). Default initial state is 0. :mex MEX-PAIR A pair of mutually exclusive inputs. There needs to be one of these statements for each pair of mutually exclusive inputs. These only work when the initial state of the inputs is 0 (positive logic active high). :state NUM BOOLEAN-LIST NUM BOOLEAN-LIST This defines transitions between states. The fist NUM is the initial state. When the value of the inputs makes the first BOOLEAN-LIST true, then the transition fires and moves you to the state specified by the second NUM, and the outputs are updated as specified by the second BOOLEAN-LIST. This is transition dependent -- you only need to specify inputs or outputs that *change* or may change in the boolean-list, not the complete state of the inputs and outputs. The following is a sample state machine which should clear up the usage information. ;;;============================================================= ;;; Example FSM description data file ;;; Entry is free-format. ;;; Keywords are required to be in the order shown, ;;; except for optional statements which may be omitted. ;;;============================================================= ;;; initial description and constraints ;;;============================================================= :fsm PE-Send-Ifc ;FSM that interfaces sends to the PE. :in (Req-Send TReq Rd-IQ ADBld-out Ack-Pkt) ;list of input variables :out (TAck PEAck ADBld) ;list of output variables :init-in () ;value of inputs in initial state ;(optional) ;default is all zero :init-out () ;list of output variables ;initial value of outputs (optional) ;default is all zero :init-state 0 ;initial state (optional) ;default is S0 :mex (Rd-IQ Ack-Pkt) ;pairs of mutually exclusive inputs. ;use as many :mex statements as needed. ;including 0 (optional). ;;;============================================================= ;;; Behavioral description - each :state entry corresponds to ;;; an arc in the state diagram. ;;; Only inputs and outputs which transition need to be specified - ;;; Note that inputs are specified in sum-of-products form, ;;; outputs are represented as one AND term. ;;;============================================================= :state 0 (Req-Send * TReq * Rd-IQ) 1 (ADBld) :state 1 (ADBld-out) 2 (PEAck) :state 2 (Rd-IQ~) 3 (PEAck~ * ADBld~ * TAck) :state 3 (TReq~ * Rd-IQ * ADBld-out~) 4 (ADBld) :state 4 (ADBld-out) 5 (PEAck) :state 5 (Rd-IQ~) 6 (PEAck~ * ADBld~ * TAck~) :state 6 (TReq * Rd-IQ * ADBld-out~) 1 (ADBld) :state 6 (TReq * Ack-Pkt * ADBld-out~) 7 (PEAck * TAck) :state 7 (Ack-Pkt~ * TReq~) 9 (PEAck~ * TAck~) :state 3 (TReq~ * Ack-Pkt * ADBld-out~) 8 (PEAck) :state 8 (Ack-Pkt~) 9 (PEAck~ * TAck~) :state 9 (TReq) 10 (TAck) :state 10 (TReq~) 9 (TAck~) :state 9 (Req-Send~) 0 () ;;;============================================================= RUNNING THE MOST EXCELLENT ASYNCHRONOUS TOOL Once a state machine has been specified you run the "meat" function to generate implementations of the specification. The meat function has a required argument which is the name of the file that contains the specification. An optional second argument, when not nil, causes the state specification to be more verbose, printing out initial and reduced state tables from the specified input. The optional third argument specifies the variance results that the asynchronous logic minimization will generate. If you want to see ALL the possible implementations for a given set of compatibles, you can set the third argument to a large value (eg. 999). If you have a specification that takes a very long time to generate an implementation, you may want to set the third argument to a smaller value, down to 0. (But you probably don't need to muck with this, anyway.) The meat program will read the description and generate a set of maximal compatibles. It is up to the user to select a subset of these maximal compatibles that fully covers the state machine. There can be many possible coverings. The program then generates an implementation for each valid state assignment for the given covering, and all of the valid sum of product equations that generate each implementation. As heuristics are always right (heh heh) we print a heuristic value for all of the state machine implementations generated. Like golf, the lower the heuristic value the better. (I hate golf, so this matches perfectly! I don't know why I keep playing it...) The heuristic value is intended to make the selection of the "best" implementation easier. Here is a sample run of the above state machine example (which was written into the file "pe-send-ifc.data" (slightly edited so it will print in 80 columns). This was run using the "verbose" option so you can examine the state table row merging and state assignments. > (meat "pe-send-ifc.data" t) Initial Input Table: FSM PE-SEND-IFC INPUTS (REQ-SEND TREQ RD-IQ ADBLD-OUT ACK-PKT) OUTPUTS (TACK PEACK ADBLD) IN: 00000 00001 00010 00011 00100 00101 00110 00111 01000 01001 01010 01011 01100 01101 01110 01111 10000 10001 10010 10011 10100 10101 10110 10111 11000 11001 11010 11011 11100 11101 11110 11111 S0 0 X X X 0 X X X 0 X X X 0 X X X 0 X X X 0 X X X 0 X X X 1 X X X 000 XXX XXX XXX 000 XXX XXX XXX 000 XXX XXX XXX 000 XXX XXX XXX 000 XXX XXX XXX 000 XXX XXX XXX 000 XXX XXX XXX 00X XXX XXX XXX 0 S1 X X X X X X X X X X X X X X X X X X X X X X X X X X X X 1 X 2 X XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX 001 XXX 0X1 XXX 0 S2 X X X X X X X X X X X X X X X X X X X X X X X X X X 3 X X X 2 X XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX 011 XXX 0 S3 X X X X X X X X X X X X X X X X 3 8 3 3 4 X 3 X 3 3 3 3 3 X 3 X XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX 100 1X0 100 100 10X XXX 100 XXX 100 100 100 100 100 XXX 100 XXX 0 S4 X X X X X X X X X X X X X X X X X X X X 4 X 5 X X X X X X X X X XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX 101 XXX 1X1 XXX XXX XXX XXX XXX XXX XXX XXX XXX 0 S5 X X X X X X X X X X X X X X X X X X 6 X X X 5 X X X X X X X X X XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX 111 XXX XXX XXX XXX XXX XXX XXX XXX XXX 0 S6 X X X X X X X X X X X X X X X X 6 6 6 6 6 X 6 X 6 7 6 6 1 X 6 X XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX 000 000 000 000 000 XXX 000 XXX 000 XX0 000 000 00X XXX 000 XXX 0 S7 X X X X X X X X X X X X X X X X 9 7 X X X X X X 7 7 X X X X X X XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XX0 110 XXX XXX XXX XXX XXX XXX 110 110 XXX XXX XXX XXX XXX XXX 0 S8 X X X X X X X X X X X X X X X X 9 8 X X X X X X X X X X X X X X XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XX0 110 XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX 0 S9 0 X X X X X X X X X X X X X X X 9 X X X X X X X 10 X X X X X X X 000 XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX 000 XXX XXX XXX XXX XXX XXX XXX X00 XXX XXX XXX XXX XXX XXX XXX 0 S10 X X X X X X X X X X X X X X X X 9 X X X X X X X 10 X X X X X X X XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX X00 XXX XXX XXX XXX XXX XXX XXX 100 XXX XXX XXX XXX XXX XXX XXX 0 Max Compatibles: ((0 1 2 5) (0 6) (1 2 4 5 7 8) (1 2 4 5 8 9 10) (3)) Enter State set: '((0 6) (1 5 7) (2 4 8 9 10) (3)) state assignments: 1 Merged Table FSM PE-SEND-IFC INPUTS (REQ-SEND TREQ RD-IQ ADBLD-OUT ACK-PKT) OUTPUTS (TACK PEACK ADBLD) IN: 00000 00001 00010 00011 00100 00101 00110 00111 01000 01001 01010 01011 01100 01101 01110 01111 10000 10001 10010 10011 10100 10101 10110 10111 11000 11001 11010 11011 11100 11101 11110 11111 S0 0 X X X 0 X X X 0 X X X 0 X X X 0 0 0 0 0 X 0 X 0 1 0 0 1 X 0 X 000 XXX XXX XXX 000 XXX XXX XXX 000 XXX XXX XXX 000 XXX XXX XXX 000 000 000 000 000 XXX 000 XXX 000 XX0 000 000 00X XXX 000 XXX 0010101000 S1 X X X X X X X X X X X X X X X X 2 1 0 X X X 1 X 1 1 X X 1 X 2 X XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XX0 110 XXX XXX XXX XXX 111 XXX 110 110 XXX XXX 001 XXX 0X1 XXX 1001100010 S2 0 X X X X X X X X X X X X X X X 2 2 X X 2 X 1 X 2 X 3 X X X 2 X 000 XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX 000 110 XXX XXX 101 XXX 1X1 XXX 100 XXX XXX XXX XXX XXX 011 XXX 1001000101 S3 X X X X X X X X X X X X X X X X 3 2 3 3 2 X 3 X 3 3 3 3 3 X 3 X XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX 100 1X0 100 100 10X XXX 100 XXX 100 100 100 100 100 XXX 100 XXX 0100010101 Merged Table with STATE CODES: FSM PE-SEND-IFC INPUTS (REQ-SEND TREQ RD-IQ ADBLD-OUT ACK-PKT) OUTPUTS (TACK PEACK ADBLD) IN: 00000 00001 00010 00011 00100 00101 00110 00111 01000 01001 01010 01011 01100 01101 01110 01111 10000 10001 10010 10011 10100 10101 10110 10111 11000 11001 11010 11011 11100 11101 11110 11111 S0 0 X X X 0 X X X 0 X X X 0 X X X 0 0 0 0 0 X 0 X 0 1 0 0 1 X 0 X 000 XXX XXX XXX 000 XXX XXX XXX 000 XXX XXX XXX 000 XXX XXX XXX 000 000 000 000 000 XXX 000 XXX 000 XX0 000 000 00X XXX 000 XXX 00 S1 0 X X X X X X X X X X X X X X X 2 1 0 X X X 1 X 1 1 X X 1 X 2 X 000 XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XX0 110 XXX XXX XXX XXX 111 XXX 110 110 XXX XXX 001 XXX 0X1 XXX 10 S2 0 X X X X X X X X X X X X X X X 2 2 X X 2 X 1 X 2 X 3 X X X 2 X 000 XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX 000 110 XXX XXX 101 XXX 1X1 XXX 100 XXX XXX XXX XXX XXX 011 XXX 11 S3 0 X X X X X X X X X X X X X X X 3 2 3 3 2 X 3 X 3 3 3 3 3 X 3 X 000 XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX 100 1X0 100 100 10X XXX 100 XXX 100 100 100 100 100 XXX 100 XXX 01 SOP for "Y1": Doing Get-Pimps... Getting sync solutions..... Getting async solutions... *****The Following Are Asynchronous Solutions for Y1 ***** 124: Y0*TREQ~*ADBLD-OUT~*ACK-PKT + Y0*TREQ~*RD-IQ*ADBLD-OUT~ + Y0~*TREQ*ADBLD-OUT~*ACK-PKT + Y0~*REQ-SEND*TREQ*RD-IQ*ADBLD-OUT~ + Y1*RD-IQ + Y1*REQ-SEND*ADBLD-OUT~ *****Asynchronous Minimization Done***** SOP for "Y0": Doing Get-Pimps... Getting sync solutions..... possible sync solns: 146 sync solns : 7 Getting async solutions... possible async solns: 14 async solns : 3 *****The Following Are Asynchronous Solutions for Y0 ***** 140: Y0*TREQ + Y0*REQ-SEND*ADBLD-OUT~ + Y0*REQ-SEND*RD-IQ~ + Y1*TREQ*ADBLD-OUT + Y1*REQ-SEND*TREQ~*ADBLD-OUT~*ACK-PKT~ + Y1~*Y0*ADBLD-OUT + Y1~*Y0*RD-IQ 122: Y0*RD-IQ*ADBLD-OUT~ + Y0*TREQ + Y0*REQ-SEND*RD-IQ~ + Y1*TREQ*ADBLD-OUT + Y1*REQ-SEND*TREQ~*ADBLD-OUT~*ACK-PKT~ + Y1~*Y0*REQ-SEND 102: Y0*TREQ + Y0*REQ-SEND*ADBLD-OUT~ + Y1*TREQ*ADBLD-OUT + Y1*REQ-SEND*TREQ~*ADBLD-OUT~*ACK-PKT~ + Y1~*Y0*REQ-SEND *****Asynchronous Minimization Done***** SOP for TACK: Doing Get-Pimps... Getting sync solutions..... possible sync solns: 2606 sync solns : 18 Getting async solutions... possible async solns: 40 async solns : 6 *****The Following Are Asynchronous Solutions for TACK ***** 108: Y0*ACK-PKT + Y0*TREQ*RD-IQ~ + Y0*TREQ~*RD-IQ + Y1*ACK-PKT + Y1*TREQ*RD-IQ~ + Y1*TREQ~*ADBLD-OUT + Y1~*Y0*REQ-SEND 110: Y0*ACK-PKT + Y0*TREQ*ADBLD-OUT~ + Y0*TREQ~*RD-IQ + Y1*ACK-PKT + Y1*TREQ*RD-IQ~ + Y1*TREQ~*ADBLD-OUT + Y1~*Y0*REQ-SEND 106: Y0*ACK-PKT + Y0*TREQ*RD-IQ~ + Y0*TREQ~*RD-IQ + Y1*ACK-PKT + Y1*TREQ*RD-IQ~ + Y1*TREQ~*RD-IQ + Y1~*Y0*REQ-SEND 108: Y0*ACK-PKT + Y0*TREQ*ADBLD-OUT~ + Y0*TREQ~*RD-IQ + Y1*ACK-PKT + Y1*TREQ*RD-IQ~ + Y1*TREQ~*RD-IQ + Y1~*Y0*REQ-SEND 130: Y0*ACK-PKT + Y0*RD-IQ*ADBLD-OUT~ + Y0*TREQ*RD-IQ~ + Y0*TREQ~*ADBLD-OUT + Y1*ACK-PKT + Y1*TREQ*RD-IQ~ + Y1*TREQ~*RD-IQ + Y1~*Y0*REQ-SEND 130: Y0*ACK-PKT + Y0*RD-IQ*ADBLD-OUT~ + Y0*TREQ*ADBLD-OUT~ + Y0*TREQ~*ADBLD-OUT + Y1*ACK-PKT + Y1*TREQ*RD-IQ~ + Y1*TREQ~*RD-IQ + Y1~*Y0*REQ-SEND *****Asynchronous Minimization Done***** SOP for PEACK: Doing Get-Pimps... Getting sync solutions..... possible sync solns: 46 sync solns : 11 Getting async solutions... possible async solns: 11 async solns : 6 *****The Following Are Asynchronous Solutions for PEACK ***** 50: Y1*ACK-PKT + Y1*ADBLD-OUT + Y1*Y0~*REQ-SEND*RD-IQ~ 50: Y1*ACK-PKT + Y1*ADBLD-OUT + Y1*Y0~*TREQ*RD-IQ~ 74: Y1*ACK-PKT + Y1*Y0*TREQ*RD-IQ + Y1*Y0~*REQ-SEND*RD-IQ~ + Y1*Y0~*REQ-SEND*TREQ~ 74: Y1*ACK-PKT + Y1*Y0*TREQ*RD-IQ + Y1*Y0~*TREQ~*RD-IQ + Y1*Y0~*REQ-SEND*RD-IQ~ 74: Y1*ACK-PKT + Y1*Y0*TREQ*RD-IQ + Y1*Y0~*TREQ*RD-IQ~ + Y1*Y0~*REQ-SEND*TREQ~ 72: Y1*ACK-PKT + Y1*Y0*TREQ*RD-IQ + Y1*Y0~*TREQ*RD-IQ~ + Y1*Y0~*TREQ~*RD-IQ *****Asynchronous Minimization Done***** SOP for ADBLD: Doing Get-Pimps... Getting sync solutions..... possible sync solns: 3 sync solns : 2 Getting async solutions... possible async solns: 2 async solns : 1 *****The Following Are Asynchronous Solutions for ADBLD ***** 12: Y1*RD-IQ *****Asynchronous Minimization Done***** HEURISTIC TOTAL FOR THIS ASSIGNMENT: 394 (394) REFERENCES: Stevens, Kenneth S. "Automatic synthesis of Fast, Compact Self-Timed State Machines", University of Calgary Research Report No. 92/495/33, December, 1992. W. S. Coates, A. L. Davis, and K. S. Stevens. "Automatic Synthesis of Fast Compact Asynchronous Control Circuits", IFIP Working Conference on Asynchronous Design Methodologies, March 1993. Unger, Steven H. "Asynchronous Sequential Switching Circuits", 1983 Reprint by Robert E. Krieger Publishing Company, Inc., Krieger Drive, Malabar, Florida 32950 (originally published by Wiley, 1969) Tracey, James H. "Internal State Assignments for Asynchronous Sequential Machines", IEEE Transactions on Electronic Computers, Vol. EC-15, No. 4, pages 551-560, August 1966. K. S. Stevens, S. V Robison, and A. L. Davis. "The Post Office -- Communication Support for Distributed Ensemble Architectures", Proceedings of 6th International Conference on Distributed Computing Systems}, pages 160-166, May 1986. COMPLIMENTS OF: Ken Stevens kstevens@ece.utah.edu Al Davis ald@cs.utah.edu Bill Coates coates@eng.sun.com