← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/flowcontrol/packet/flowcontrol.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/flowcontrol/packet/flowcontrol.lisp
 
1
#|$ACL2s-Preamble$;
 
2
(begin-book);$ACL2s-Preamble$|#
 
3
 
 
4
(in-package "ACL2")
 
5
 
 
6
(include-book "../../../generic-modules/flowcontrol")
 
7
(include-book "../../datalink/simple/datalink")
 
8
;;
 
9
;; Flowcontrol
 
10
;;
 
11
(defun switchBuffer (nst from to)
 
12
  ;; move the head of the buffer of the from port to the tail of the buffer of the to port. 
 
13
  ;;returns the update nst list. 
 
14
  ;; 
 
15
  ;; Arguments:
 
16
  ;; - nst : the list of all ports of this node
 
17
  ;; - from : The input port which is switched
 
18
  ;; - to : The output port which is switched
 
19
  (if (endp nst)
 
20
    nil
 
21
    (if (equal (port-address (car nst)) (port-address to))
 
22
      (cons (port-updateBuffer to (port-buffer from)) (switchBuffer (cdr nst) from to))
 
23
      (if (equal (port-address (car nst)) (port-address from))
 
24
        (cons (port-updateBuffer from nil) (switchBuffer (cdr nst) from to))
 
25
        (cons (car nst) (switchBuffer (cdr nst) from to))))))
 
26
 
 
27
 
 
28
(defun switch-port (portlist nst from)
 
29
  ;; Switch the input port from by looping over the nst in portlist until the port where the from port is routed to is reached. 
 
30
  ;; 
 
31
  ;; Arguments:
 
32
  ;; - portlist : The list of output ports of this node
 
33
  ;; - nst : the list of all ports of this node
 
34
  ;; - from : The input port which is switched
 
35
  (let ((to (car portlist)))
 
36
    (cond ((endp portlist)
 
37
           nst)
 
38
          ((and (equal (port-portname to) (status-route (port-status from)))
 
39
                (endp (port-buffer to)))
 
40
           (switchBuffer nst from to))
 
41
          (t (switch-port (cdr portlist) nst from)))))
 
42
 
 
43
 
 
44
(defun switch-ports (portslist nst)
 
45
  ;; Switches each port in portlist. If a port has a msg in its buffer switch the port. The switched ports are returned.
 
46
  ;;
 
47
  ;; Arguments:
 
48
  ;; - portlist : The list of input ports of this node
 
49
  ;; - nst : the list of all ports of this node
 
50
  (if (endp portslist)
 
51
    nst
 
52
    (let* ((inport (car portslist)))
 
53
      (if (not (endp (port-buffer inport)))  ;; and something to send
 
54
        (switch-ports (cdr portslist) (switch-port (ports-outputports nst) nst inport)) ;; clean
 
55
        (switch-ports (cdr portslist) nst)))))
 
56
 
 
57
(defun packet-FlowControl (nst memory)
 
58
  ;; This is the function that performs the flowcontrol in a router. This consists of scheduling the routed input nodes and switching the sheduled msg.
 
59
  ;;
 
60
  ;; Arguments:
 
61
  ;; - nst : list of ports in a node
 
62
  ;; - memory : the global memory of a node
 
63
  (mv (switch-ports (ports-inputports nst) nst) memory))
 
64
 
 
65
(definstance GenericFlowControl check-compliance-Flowcontrol                   
 
66
  :functional-substitution
 
67
  ((flowcontrol packet-FlowControl)))#|ACL2s-ToDo-Line|#
 
68
 
 
69
 
 
70