CS 3220 Processor Design
Fall 2002

Instructor: Pete Manolios

Project 2, Due 11/1/2002 (before midnight)

Note: Make sure that you allocate enough time to the project.

A netlist language

For this part of the assignment, you will define a netlist language (using ACL2). The language will allow you to describe combinational functions (circuits) at the gate level. You can define combinational functions, give them names, and use those functions to define other, more complex functions. Combinational functions can have any natural number of inputs, and any positive number of outputs. Here is an example of how one can define a 2-bit adder.

(defconst *defs1*
  '((maj (a b c)
	 ((0 (and a b))
	  (1 (and a c))
	  (2 (and b c))
	  (d (or 0 1 2))))

    (fa (a b cin) 
	(s cout)
	((s    (xor a b cin))
	 (cout (maj a b cin))))

    (adder-2-bit (a1 a0 b1 b0 cin)
		 (cout c1 c0)
		 (((c0 0)    (fa a0 b0 cin))
		  ((c1 cout) (fa a1 b1 0))))))

Above we defined maj, a function that has three inputs, a, b, and c, and one output, d. Wire 0 corresponds to a AND b, wire 1 to a AND c, wire 2 to b AND c, and the output wire d corresponds to the OR of wires 0, 1, and 2. This is the majority function we have already seen. We then define a full adder, fa, which has the inputs a, b, and cin and the outputs s and cout using the function maj, just defined. Note that the functions and, or, and xor are built-in and can have 2 or more inputs, but functions that are defined can only have a fixed number of inputs and outputs (specified at definition time). The 2-bit adder function shows how to assign values to wires when using functions with multiple outputs.

Here is the specification for the syntax of the language. It will probably help to look at the above example as you go through it. The constant *defs1* is an example of a net definition list.

The above specification allows for various implementations. When you have a design decision to make, try to make a decision that makes sense, e.g., I do not explicitly prohibit multiple net definitions with the same name in a net definition list, but, obviously, one should not allow this. Document such design decisions in your code.

We now define the semantics of the netlist language. Consider the following example.

(net-val *defs1*
         '(((out d1 d0)
           (adder-2-bit e1 e0 a1 a0 in)))
         '(out d1 d0)
         '((e1 . 1) (e0 . 0) 
           (a1 . 1) (a0 . 1)
                    (in . 1)))

It returns

(1 1 0)

Notice that bits, wire values, are either 1 or 0 (instead of t or nil). The function net-val evaluates the netlist expression, its second argument, given the definitions in its first argument, given values to the inputs specified in the fourth argument and returns the values in the wires identified in the third argument. So, this is a function that evaluates netlist expressions, given some definitions and input values. In more detail, we evaluate the adder-2-bit function on inputs e1, e0, a1, a0, and in (notice that the names here differ from the names of the inputs of adder-2-bit). The result is bound to wires out, d1, and d0 and since these are the wires identified as output wires, the result is output.

How to evaluate the builtin functions and, or, xor, and not should be obvious. The builtin function wire assigns the value of the input wire to the output wire, so you can think of it as an assignment operator. The built-in function const creates a constant by assigning the sequence of bits (0s and 1s) that are its arguments to the output wires.

Here is what you have to hand in.

  1. Write a function net-defs that given input nds returns t if nds is a net definition list and nil otherwise.
  2. Write a function net-val that given inputs net-defs, a net definition list, net-exp, a netlist expression, outputs, a list of wire names, and alist, an alist mapping wire names to bits, returns a bit vector corresponding to the values of the wires in outputs (in the same order the wire names appear in outputs).
  3. Write an ACL2 function, ripple-carry-alu to generate the netlist description of an n-bit ALU for any n>=2 that operates like the final ripple carry ALU in section 4.5, page 240, of P&H, except that you do not have to detect overflow. In more detail, for any n>=2, (ripple-carry-alu n) should generate a net definition list whose last net definition is named ALU-n-bit (the n in the name should match the n given as input to ripple-carry-alu). The first n inputs correspond to the first n-bit word, with high-order bit first, the next n inputs correspond to the second n-bit word, the next input corresponds to the bnegate wire and the last two to the ALU control lines (see figure 4.20 of P&H). The order of the outputs is: carry-out (instead of overflow), high-order bit, ..., low-order bit (Result31, ..., Result0 in figure 4.19), and Zero.
  4. Design the above 32-bit ALU using the Altera toolkit. Use of hierarchical design is strongly encouraged.
  5. Write a function flatten-net that given inputs net-defs, a net definition list, and net-exp, a netlist expression, returns a net-list expression that is equivalent to net-exp, except that all function calls are to built-in functions. This is refered to as "flattening" the netlist.
  6. Write a function wire-exp that given inputs net-defs, a net definition list, net-exp, a netlist expression, and wire, a wire name (appearing in net-exp), returns a netlist expression that computes the value of wire. The resulting netlist should be flat (see above) and should be as minimal as you can get it. That is, it should not compute the values of wires that do not affect wire.
  7. Write a function time-net that given inputs net-defs, a net definition list, and net-exp, a netlist expression, returns a natural number corresponding to how long it takes to evaluate net-exp. Imagine flattening the netlist and looking at all the paths from inputs, through built-in functions to wires. The length of the longest such path is what you should return.


  1. If you have trouble proving termination of functions, use skip-proofs.
  2. Here are some more netlist examples. As I get questions, I will update this file, so check it if you have questions and before submitting your solutions.

For extra credit, you can do the following.

  1. Write an ACL2 function to generate the netlist description of an n-bit ALU for any n>=2 that operates like the ALU above, except that it uses a carry-lookahead adder (described at the end of section 4.5 of P&H).

    Design the ALU using the Altera toolkit.

Submission Instructions

Create an archive of the files using tar or winzip (if you want to use something else, ask Vernard first to make sure we can unarchive it) and send us the archive (as a single attachment) via email. The email should be sent both to me and to Vernard (vernard@cc). Read the instructions on turning in assignments carefully.