Import acl2_7.4dfsg.orig.tar.gz

[dgit import orig acl2_7.4dfsg.orig.tar.gz]

1 files changed, 34 insertions, 0 deletions

diff --git a/books/workshops/2009/vandenbroek-schmaltz/GeNoC/generic-modules/router.lisp b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/generic-modules/router.lisp
new file mode 100644
index 0000000..3f56311
--- /dev/null
+++ b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/generic-modules/router.lisp
@@ -0,0 +1,34 @@
+#|$ACL2s-Preamble$;
+(begin-book);$ACL2s-Preamble$|#
+
+(in-package "ACL2")
+
+(include-book "make-event/defspec" :dir :system)
+(include-book "types")#|ACL2s-ToDo-Line|#
+
+(include-book "datalink")
+(include-book "routecontrol")
+(include-book "flowcontrol")
+
+
+
+
+
+;;
+;; Router
+;;
+
+(defspec GenericRouter
+  (((Router * *) => (mv * *)))
+
+  (local (defun router (node memory)
+           ;; This function represents the router component of a Node.
+           ;; Applies the different processes in a router in the correct order.
+           (mv-let (node memory)
+                   (RouteControl (ProcessInputs node) memory)
+                   (mv-let (node memory)
+                           (Flowcontrol node memory)
+                           (mv (ProcessOutputs node) memory))))))
+
+
+