diff options
Diffstat (limited to 'books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations')
22 files changed, 1167 insertions, 0 deletions
diff --git a/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/datalink/simple/datalink.lisp b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/datalink/simple/datalink.lisp new file mode 100644 index 0000000..fb42997 --- /dev/null +++ b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/datalink/simple/datalink.lisp @@ -0,0 +1,129 @@ +#|$ACL2s-Preamble$; +(begin-book);$ACL2s-Preamble$|# + +(in-package "ACL2") + +(include-book "../../../generic-modules/datalink") + +;; +;; Inputs +;; + +(defun status-ackrx (status) + ;; get the ack recieve flag + (car (mv-nth 0 status))) + +(defun status-rx (status) + ;; get the recieve flag + (car (mv-nth 1 status))) + +(defun port-updateAckRX (port flag) + ;; Update the ack recieve flag + (update-nth 1 (update-nth 0 (list flag) (port-status port)) port)) + +(defun port-updateRX (port flag) + ;; Update the recieve flag + (update-nth 1 (update-nth 1 (list flag) (port-status port)) port)) + +(defun port-bufferFull (port) + ;; Move the data to the buffer field + (> (len (port-buffer port)) 2)) + +(defun port-Data2buffer (port) + ;; Move the data to the buffer field + (port-bufferMsg port (port-data port))) + +(defun readData (port) + ;; Move the data to the buffer field and set the ack recieve flag. + (port-updateAckRX (port-Data2Buffer port) t)) + +(defun simple-processInputs (ports) + ;; Process the input ports. There are 3 cases. + ;; if processing the local input port and the recieve flag is set and the ack flag is not set read the data and clear the port. + ;; if recieve flag is set and not the ack flag read the data. + ;; if there is an ack, but there is nothing to send clear the input port + ;; else do nothing + (if (endp ports) + nil + (if (equal (port-dir (car ports)) 'in) + (cond + + ((and (equal (port-portname (car ports)) 'loc) + (status-rx (port-status (car ports))) + (not (status-ackrx (port-status (car ports)))) + (not (port-bufferFull (car ports)))) + (cons (port-updateRX (port-updateData (readData (car ports)) nil) nil) (simple-processInputs (cdr ports)))) + + ((and (status-rx (port-status (car ports))) + (not (status-ackrx (port-status (car ports)))) + (not (port-bufferFull (car ports)))) + (cons (readData (car ports)) (simple-processInputs (cdr ports)))) + + ((status-ackrx (port-status (car ports))) + (cons (port-updateAckRX (car ports) nil) (simple-processInputs (cdr ports)))) + + (t (cons (car ports) (simple-processInputs (cdr ports))))) + (cons (car ports) (simple-processInputs (cdr ports)))))) + + +;; +;; Outputs +;; + +(defun status-tx (status) + ;;Set the transmission flag + (car(mv-nth 0 status))) + +(defun status-acktx (status) + ;;Get the response flag + (car(mv-nth 1 status))) + + +(defun port-updateTX (port flag) + ;;Set the transmission flag + (update-nth 1 (update-nth 0 (list flag) (port-status port)) port)) + +(defun port-Buffer2Data (port) + ;;Move the buffer to the data field + (port-popBuffer (port-updateData port (port-bufferHead port) ))) + +(defun status-route (status) + ;; Return the value of the local state of an port. This is used the route value. + (car (mv-nth 2 status))) + +(defun sendData (port) + ;;Move the buffer to the data field and set the transmission flag. + (port-updateTx (port-Buffer2Data port) t)) + + + +(defun simple-processOutputs (ports) + ;; Process the output ports. There are 3 cases. + ;; if sending but there is an ack and there is a msg is ready in the buffer send msg. + ;; if not sending but msg is ready in the buffer send msg. + ;; if there is an ack, but there is nothing to send clear the output port + ;; else do nothing + (if (endp ports) + nil + (if (equal (port-dir (car ports)) 'out) + (cond + + ((and (status-tx (port-status (car ports))) + (status-acktx (port-status (car ports))) + (port-bufferHead (car ports))) + (cons (sendData (car ports)) (simple-processOutputs (cdr ports)))) + + ((and (not (status-tx (port-status (car ports)))) + (port-bufferHead (car ports))) + (cons (sendData (car ports)) (simple-processOutputs (cdr ports)))) + + ((and (status-acktx (port-status (car ports)))) + (cons (port-updatedata (port-updateTX (car ports) nil) nil) (simple-processOutputs (cdr ports)))) + (t (cons (car ports) (simple-processOutputs (cdr ports))))) + + (cons (car ports) (simple-processOutputs (cdr ports)))))) + +(definstance GenericDatalink check-compliance-datalink + :functional-substitution + ((processInputs simple-processInputs) + (processOutputs simple-processOutputs))) diff --git a/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/departure/simple/departure.lisp b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/departure/simple/departure.lisp new file mode 100644 index 0000000..0230a56 --- /dev/null +++ b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/departure/simple/departure.lisp @@ -0,0 +1,29 @@ +#|$ACL2s-Preamble$; +(begin-book);$ACL2s-Preamble$|# + +(in-package "ACL2") + +(include-book "../../../generic-modules/departure") +(include-book "../../../generic-modules/types") + +(defun simple-depart (ntkst transactions time) + ;; This function splits the list of transactions into a list of delayed and departing transmissions depending on the current time of the simulation + ;; + ;; Arguments: + ;; - ntkst : a list of ports. + ;; - transactions : a list of transactions. + ;; - time : the time of the simulation step. + (if (endp transactions) + (mv ntkst nil) + (let ((transaction (car transactions))) + (if (and (>= time (timeT transaction)) + (ntkst-canDepart ntkst transaction)) + (simple-depart (ntkst-depart ntkst transaction) (cdr transactions) time) + (mv-let (newntkst delayed) + (simple-depart ntkst (cdr transactions) time) + (mv newntkst (cons transaction delayed))))))) + +(definstance GenericDeparture check-compliance-simple-departure + :functional-substitution + ((depart simple-depart))) + diff --git a/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/flowcontrol/circuit/flowcontrol.lisp b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/flowcontrol/circuit/flowcontrol.lisp new file mode 100644 index 0000000..1d2ca35 --- /dev/null +++ b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/flowcontrol/circuit/flowcontrol.lisp @@ -0,0 +1,159 @@ +#|$ACL2s-Preamble$; +(begin-book);$ACL2s-Preamble$|# + +(in-package "ACL2") + +(include-book "../../../generic-modules/flowcontrol") +(include-book "../../datalink/simple/datalink") + +;; +;; Flowcontrol +;; +;; A circuit consist of a tuple consisting of (port_id, state) +;; In this implementation the circuit is the seccond position of the locate state of a port. + +(defun port-circuitState (port) + (mv-nth 1 (mv-nth 2 (mv-nth 1 port)))) + +(defun port-circuitId (port) + (mv-nth 2 (mv-nth 2 (mv-nth 1 port)))) + + +(defun port-updateCircuit (port cstate id) + ;; Updates a virtual channel. + ;; + ;; Arguments: + ;; - port : a port + ;; - cstate : the state to which the the circuit should be set. most often 'booked + ;; - id : the id of the port the circuit is connected to. + (port-updateStatus port (status-updatelocal (port-status port) (update-nth 2 id (update-nth 1 cstate (port-statusLocal port)))))) + + +(defun clearCircuit (nst portname1 portname2) + ;; Clears the state of the virtual channel + ;; + ;; Arguments: + ;; - nst : list of ports in the node + ;; - portname1 : name of the from port of the circuit + ;; - portname2 : name of the to port of the circuit + (if (endp nst) + nil + (cond ((equal (port-portname (car nst)) portname1) + (cons (port-updateCircuit (car nst) nil nil) (clearCircuit (cdr nst) portname1 portname2 ))) + ((equal (port-portname (car nst)) portname2) + (cons (port-updateCircuit (car nst) nil nil) (clearCircuit (cdr nst) portname1 portname2 ))) + (t (cons (car nst) (clearCircuit (cdr nst) portname1 portname2 )))))) + +(defun updateCircuit (nst portname1 portname2 cstate) + ;; This function updates and/or creates the state of the virtual channel + ;; + ;; Arguments: + ;; - nst : list of ports in the node + ;; - portname1 : name of the from port of the circuit + ;; - portname2 : name of the to port of the circuit + ;; - cstate : Virtual channel state. + (if (endp nst) + nil + (cond ((equal (port-portname (car nst)) portname1) + (cons (port-updateCircuit (car nst) cstate portname2) (updateCircuit (cdr nst) portname1 portname2 cstate))) + ((equal (port-portname (car nst)) portname2) + (cons (port-updateCircuit (car nst) cstate portname1) (updateCircuit (cdr nst) portname1 portname2 cstate))) + (t (cons (car nst) (updateCircuit (cdr nst) portname1 portname2 cstate))))))#|ACL2s-ToDo-Line|# + + +(defun sendack (nst portname) + (if (endp nst) + nil + (if (and (equal (port-portname (car nst)) portname) + (equal (port-dir (car nst)) 'out)) + (cons (port-BufferMsg (car nst) '(ack)) (cdr nst)) + (cons (car nst) (sendack (cdr nst) portname))))) + + +(defun switchBuffer (nst from to) + ;; move the head of the buffer of the from port to the tail of the buffer of the to port. + ;;returns the update ports list. + ;; + ;; Arguments: + ;; - nst : the list of all ports of this node + ;; - from : The input port which is switched + ;; - to : The output port which is switched + (if (endp nst) + nil + (if (equal (port-address (car nst)) (port-address to)) + (cons (port-BufferMsg to (port-bufferHead from)) (switchBuffer (cdr nst) from to)) + (if (equal (port-address (car nst)) (port-address from)) + (cons (port-popBuffer from) (switchBuffer (cdr nst) from to)) + (cons (car nst) (switchBuffer (cdr nst) from to)))))) + + +(defun switch-port (portlist nst from) + ;; This funtion loops over the portlist until the output port that the from port is routed to is found. + ;; Depending on the state of the output port and the virtual channel the port is switched. + ;; There are five possible cases. + ;; 1) Its a tail flit and the circuit can be switched and cleared. + ;; 2) Its a data flit and the flit can be swtiched. + ;; 3) Its a ack flit and the circuit state can be changes from 'request to 'booked + ;; 4) Its an arived header flit and a ack can be send back. + ;; 5) Its a header flit not a the destination and the circuit can be requested. + ;; + ;; Arguments: + ;; - portlist : list of output ports of the node + ;; - nst : list of pors in the node + ;; - from : input port trying to switch + (let ((to (car portlist))) + (cond ((endp portlist) + nst) + ((and (equal (port-portname to) (status-route (port-status from))) ;booked + (not (port-bufferFull to)) ;; and space in buffer + (equal (port-circuitState to) 'booked) + (equal (port-circuitId to) (port-portname from)) + (equal (flitT (port-buffer from)) 0)) + (clearCircuit (switchBuffer nst from to) (port-portname to) (port-portname from))) + + ((and (equal (port-portname to) (status-route (port-status from))) ;booked + (not (port-bufferFull to)) ;; and space in buffer + (equal (port-circuitState to) 'booked) + (equal (port-circuitId to) (port-portname from))) + (switchBuffer nst from to)) + + ((and (equal (port-buffer from) '(ack)) ;request to booked + (not (port-bufferFull to)) ;; and space in buffer + (equal (port-circuitState to) 'request) + (equal (port-circuitId to) (port-portname from))) + (updateCircuit (switchBuffer nst from to) (port-portname to) (port-portname from) 'booked)) + + ((and (equal (port-portname to) (status-route (port-status from))) ; send ack + (not (port-bufferFull to)) ;; and space in buffer + (equal (port-portname to) 'loc) + (not (port-circuitState to))) + (sendack (updateCircuit (switchBuffer nst from to) (port-portname to) (port-portname from) 'booked) + (port-portname from))) + + ((and (equal (port-portname to) (status-route (port-status from))) ;request + (not (port-bufferFull to)) ;; and space in buffer + (not (port-circuitState to))) + (updateCircuit (switchBuffer nst from to) (port-portname to) (port-portname from) 'request)) + + (t (switch-port (cdr portlist) nst from))))) + + +(defun switch-ports (portslist nst) + ;; Switches each port in portlist. + ;; if a port is routed and has a msg in its buffer switch the port + (if (endp portslist) + nst + (let* ((inport (car portslist))) + (if (not (endp (port-bufferHead inport))) ;; and something to send + (switch-ports (cdr portslist) (switch-port (ports-outputports nst) nst inport)) ;; clean + (switch-ports (cdr portslist) nst))))) + +(defun circuit-FlowControl (nst memory) + ;; This is the function that performs the flowcontrol in a router. This consists of scheduling the routed input nodes and switching the sheduled msg. + (mv (switch-ports (ports-inputports nst) nst) memory)) + +(definstance GenericFlowControl check-compliance-Flowcontrol + :functional-substitution + ((flowcontrol circuit-FlowControl))) + + diff --git a/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/flowcontrol/packet/flowcontrol.lisp b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/flowcontrol/packet/flowcontrol.lisp new file mode 100644 index 0000000..cff37f7 --- /dev/null +++ b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/flowcontrol/packet/flowcontrol.lisp @@ -0,0 +1,70 @@ +#|$ACL2s-Preamble$; +(begin-book);$ACL2s-Preamble$|# + +(in-package "ACL2") + +(include-book "../../../generic-modules/flowcontrol") +(include-book "../../datalink/simple/datalink") +;; +;; Flowcontrol +;; +(defun switchBuffer (nst from to) + ;; move the head of the buffer of the from port to the tail of the buffer of the to port. + ;;returns the update nst list. + ;; + ;; Arguments: + ;; - nst : the list of all ports of this node + ;; - from : The input port which is switched + ;; - to : The output port which is switched + (if (endp nst) + nil + (if (equal (port-address (car nst)) (port-address to)) + (cons (port-updateBuffer to (port-buffer from)) (switchBuffer (cdr nst) from to)) + (if (equal (port-address (car nst)) (port-address from)) + (cons (port-updateBuffer from nil) (switchBuffer (cdr nst) from to)) + (cons (car nst) (switchBuffer (cdr nst) from to)))))) + + +(defun switch-port (portlist nst from) + ;; Switch the input port from by looping over the nst in portlist until the port where the from port is routed to is reached. + ;; + ;; Arguments: + ;; - portlist : The list of output ports of this node + ;; - nst : the list of all ports of this node + ;; - from : The input port which is switched + (let ((to (car portlist))) + (cond ((endp portlist) + nst) + ((and (equal (port-portname to) (status-route (port-status from))) + (endp (port-buffer to))) + (switchBuffer nst from to)) + (t (switch-port (cdr portlist) nst from))))) + + +(defun switch-ports (portslist nst) + ;; Switches each port in portlist. If a port has a msg in its buffer switch the port. The switched ports are returned. + ;; + ;; Arguments: + ;; - portlist : The list of input ports of this node + ;; - nst : the list of all ports of this node + (if (endp portslist) + nst + (let* ((inport (car portslist))) + (if (not (endp (port-buffer inport))) ;; and something to send + (switch-ports (cdr portslist) (switch-port (ports-outputports nst) nst inport)) ;; clean + (switch-ports (cdr portslist) nst))))) + +(defun packet-FlowControl (nst memory) + ;; This is the function that performs the flowcontrol in a router. This consists of scheduling the routed input nodes and switching the sheduled msg. + ;; + ;; Arguments: + ;; - nst : list of ports in a node + ;; - memory : the global memory of a node + (mv (switch-ports (ports-inputports nst) nst) memory)) + +(definstance GenericFlowControl check-compliance-Flowcontrol + :functional-substitution + ((flowcontrol packet-FlowControl)))#|ACL2s-ToDo-Line|# + + + diff --git a/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/flowcontrol/wormhole/flowcontrol.lisp b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/flowcontrol/wormhole/flowcontrol.lisp new file mode 100644 index 0000000..065bff4 --- /dev/null +++ b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/flowcontrol/wormhole/flowcontrol.lisp @@ -0,0 +1,134 @@ +#|$ACL2s-Preamble$; +(begin-book);$ACL2s-Preamble$|# + +(in-package "ACL2") + +(include-book "../../../generic-modules/flowcontrol") +(include-book "../../datalink/simple/datalink") + +;; +;; Flowcontrol +;; +;; VC stands for Virtualchannel +;; A VC consist of a tuple consisting of (port_id, state) +;; In this implementation the VC is the seccond position of the locate state of a port. + +(defun port-VCState (port) + (mv-nth 1 (mv-nth 2 (mv-nth 1 port)))) + +(defun port-VCId (port) + (mv-nth 2 (mv-nth 2 (mv-nth 1 port)))) + + +(defun port-updateVC (port cstate id) + ;; Updates a virtual channel. + ;; + ;; Arguments: + ;; - port : a port + ;; - cstate : the state to which the the vc should be set. most often 'booked + ;; - id : the id of the port the vc is connected to. + (port-updateStatus port (status-updatelocal (port-status port) (update-nth 2 id (update-nth 1 cstate (port-statusLocal port)))))) + + +(defun clearVC (nst portname1) + ;; Clears the state of the virtual channel + ;; + ;; Arguments: + ;; - nst : list of nst in the node + ;; - portname1 : name of the from port of the VC + ;; - portname2 : name of the to port of the VC + (if (endp nst) + nil + (cond ((equal (port-portname (car nst)) portname1) + (cons (port-updateVC (car nst) nil nil) (clearVC (cdr nst) portname1 ))) + (t (cons (car nst) (clearVC (cdr nst) portname1 )))))) + +(defun updateVC (nst portname1 portname2 cstate) + ;; This function updates and/or creates the state of the virtual channel + ;; + ;; Arguments: + ;; - nst : list of nst in the node + ;; - portname1 : name of the from port of the VC + ;; - portname2 : name of the to port of the VC + ;; - cstate : Virtual channel state. + (if (endp nst) + nil + (cond ((equal (port-portname (car nst)) portname1) + (cons (port-updateVC (car nst) cstate portname2) (updateVC (cdr nst) portname1 portname2 cstate))) + (t (cons (car nst) (updateVC (cdr nst) portname1 portname2 cstate)))))) + + +(defun switchBuffer (nst from to) + ;; move the head of the buffer of the from port to the tail of the buffer of the to port. + ;;returns the update nst list. + ;; + ;; Arguments: + ;; - nst : the list of all nst of this node + ;; - from : The input port which is switched + ;; - to : The output port which is switched + (if (endp nst) + nil + (if (equal (port-address (car nst)) (port-address to)) + (cons (port-BufferMsg to (port-bufferHead from)) (switchBuffer (cdr nst) from to)) + (if (equal (port-address (car nst)) (port-address from)) + (cons (port-popBuffer from) (switchBuffer (cdr nst) from to)) + (cons (car nst) (switchBuffer (cdr nst) from to)))))) + + +(defun switch-port (portlist nst from) + ;; This funtion loops over the portlist until the output port that the from port is routed to is found. + ;; Depending on the state of the output port and the virtual channel the port is switched. + ;; There are three possible cases. + ;; 1) Its a tail flit and the virtual channel can be switched and cleared. + ;; 2) Its a data flit and the flit can be swtiched. + ;; 3) Its a header flit and the virtual channel can be booked. + ;; + ;; Arguments: + ;; - portlist : list of output nst of the node + ;; - nst : list of pors in the node + ;; - from : input port trying to switch + (let ((to (car portlist))) + (cond ((endp portlist) + nst) + ((and (equal (port-portname to) (status-route (port-status from))) ;booked + (not (port-bufferFull to)) ;; and space in buffer + (equal (port-VCState to) 'booked) ;was booked + (equal (port-VCId to) (port-portname from)) + (equal (flitT (port-bufferHead from)) 0)) + (clearVC (switchBuffer nst from to) (port-portname to))) + + ((and (equal (port-portname to) (status-route (port-status from))) ;booked + (not (port-bufferFull to)) ;; and space in buffer + (equal (port-VCState to) 'booked) + (equal (port-VCId to) (port-portname from))) + (switchBuffer nst from to)) + + ((and (equal (port-portname to) (status-route (port-status from))) ;request + (not (port-bufferFull to)) ;; and space in buffer + (not (port-VCState to))) + (updateVC (switchBuffer nst from to) (port-portname to) (port-portname from) 'booked)) + + (t (switch-port (cdr portlist) nst from))))) + + +(defun switch-ports (portslist nst) + ;; Switches each port in portlist. + ;; if a port is routed and has a msg in its buffer switch the port + (if (endp portslist) + nst + (let* ((inport (car portslist))) + (if (not (endp (port-bufferHead inport))) ;; and something to send + (switch-ports (cdr portslist) (switch-port (ports-outputports nst) nst inport)) ;; clean + (switch-ports (cdr portslist) nst))))) + +(defun wormhole-FlowControl (nst memory) + ;; This is the function that performs the flowcontrol in a router. This consists of scheduling the routed input nodes and switching the sheduled msg. + (mv (switch-ports (ports-inputports nst) nst) memory)) + + +(definstance GenericFlowControl check-compliance-Flowcontrol + :functional-substitution + ((flowcontrol wormhole-FlowControl)))#|ACL2s-ToDo-Line|# + + + diff --git a/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/genoc/circuit-XY-2Dmesh/GeNoC.lisp b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/genoc/circuit-XY-2Dmesh/GeNoC.lisp new file mode 100644 index 0000000..c8e1655 --- /dev/null +++ b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/genoc/circuit-XY-2Dmesh/GeNoC.lisp @@ -0,0 +1,15 @@ +#|$ACL2s-Preamble$; +(begin-book);$ACL2s-Preamble$|# + +(in-package "ACL2") + +(include-book "../../../generic-modules/GeNoC") +(include-book "../../network/2Dmesh/network") +(include-book "../../departure/simple/departure")#|ACL2s-ToDo-Line|# + +(include-book "../../router/XY-circuit/router") + +(instantiateStepnetwork_t INST XY-circuit) +(instantiateStepnetwork INST) +(instantiateGenoc_t INST simple) +(instantiateGenoc INST 2dmesh)
\ No newline at end of file diff --git a/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/genoc/packet-XY-2Dmesh/GeNoC.lisp b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/genoc/packet-XY-2Dmesh/GeNoC.lisp new file mode 100644 index 0000000..ca50876 --- /dev/null +++ b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/genoc/packet-XY-2Dmesh/GeNoC.lisp @@ -0,0 +1,14 @@ +#|$ACL2s-Preamble$; +(begin-book);$ACL2s-Preamble$|# + +(in-package "ACL2") + +(include-book "../../../generic-modules/GeNoC") +(include-book "../../network/2Dmesh/network") +(include-book "../../departure/simple/departure") +(include-book "../../router/XY-packet/router") + +(instantiateStepnetwork_t INST XY-packet) +(instantiateStepnetwork INST) +(instantiateGenoc_t INST simple) +(instantiateGenoc INST 2dmesh)#|ACL2s-ToDo-Line|# diff --git a/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/genoc/spidergon/GeNoC.lisp b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/genoc/spidergon/GeNoC.lisp new file mode 100644 index 0000000..c2a15e2 --- /dev/null +++ b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/genoc/spidergon/GeNoC.lisp @@ -0,0 +1,15 @@ +#|$ACL2s-Preamble$; +(begin-book);$ACL2s-Preamble$|# + +(in-package "ACL2")#|ACL2s-ToDo-Line|# + + +(include-book "../../../generic-modules/GeNoC") +(include-book "../../network/spidergon/network") +(include-book "../../departure/simple/departure") +(include-book "../../router/spidergon/router") + +(instantiateStepnetwork_t INST spidergon) +(instantiateStepnetwork INST) +(instantiateGenoc_t INST simple) +(instantiateGenoc INST spidergon)
\ No newline at end of file diff --git a/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/genoc/wormhole-XY-2Dmesh/GeNoC.lisp b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/genoc/wormhole-XY-2Dmesh/GeNoC.lisp new file mode 100644 index 0000000..2300ffe --- /dev/null +++ b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/genoc/wormhole-XY-2Dmesh/GeNoC.lisp @@ -0,0 +1,15 @@ +#|$ACL2s-Preamble$; +(begin-book);$ACL2s-Preamble$|# + +(in-package "ACL2") + +(include-book "../../../generic-modules/GeNoC")#|ACL2s-ToDo-Line|# + +(include-book "../../network/2Dmesh/network") +(include-book "../../departure/simple/departure") +(include-book "../../router/XY-wormhole/router") + +(instantiateStepnetwork_t INST XY-wormhole) +(instantiateStepnetwork INST) +(instantiateGenoc_t INST simple) +(instantiateGenoc INST 2dmesh)
\ No newline at end of file diff --git a/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/network/2Dmesh/network.lisp b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/network/2Dmesh/network.lisp new file mode 100644 index 0000000..8d6275f --- /dev/null +++ b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/network/2Dmesh/network.lisp @@ -0,0 +1,75 @@ +#|$ACL2s-Preamble$; +(begin-book);$ACL2s-Preamble$|# + +(in-package "ACL2") + +(include-book "../../../generic-modules/network"); + +;;2 nodeset generator +;;x-dim-gen generates the nodes along a y coordinate +(defun x-dim-gen (X y max) + ;; generate the nodes along the x-dim, y is a constant + (if (zp X) + nil + (let* ((curX (1- X)) + (conn (acons (list (list curX y) 'loc ) (list (list curX y) nil ) nil)) + (conn (if (< y max) + (acons (list (list curX y) 'S ) (list (list curX (1+ Y)) 'N) conn) + conn)) + (conn (if (< curX max) + (acons (list (list curX y) 'E ) (list (list X Y) 'W) conn) + conn)) + (conn (if (> y 0) + (acons (list (list curX y) 'N ) (list (list curX (1- Y)) 'S) conn) + conn)) + (conn (if (> curX 0) + (acons (list (list curX y) 'W ) (list (list (1- curX) Y) 'E) conn) + conn))) + (append conn (x-dim-gen curX y max))))) + +(defun coord-generator (X Y max) + ;; generate a list of coordinates + (if (zp Y) + nil + (append (x-dim-gen X (1- y) max) + (coord-generator X (1- Y) max)))) + +(defun 2Dmesh-topology (x) + ;; Generates a list of the connection pressent in the network. + ;; Example: + ;; (((0 0) LOC) (0 0) NIL) + ;; (((0 0) S) (0 1) N) + ;; ... + ;; (((1 1) LOC) (1 1) NIL) + ;; (((1 1) N) (1 0) S) + ;; (((1 1) W) (0 1) E)) + ;; + ;; Arguments: + ;; - topo : Initialisation argument of the model. Often this is the size of the network. + (reverse (coord-generator x x (1- x)))) + + + +(defun mem-gen-Y (x y) + (if (zp y) + nil + (acons (list (1- x) (1- y)) nil (mem-gen-Y x (1- y))))) + + +(defun mem-gen (x y) + (if (zp x) + nil + (append (mem-gen-Y x y) (mem-gen (1- x) y)))) + + +(defun 2Dmesh-nodeMemory (x) + (reverse (mem-gen x x)))#|ACL2s-ToDo-Line|# + + +(definstance GenericNetwork check-compliance-2dmesh-network + :functional-substitution + ((topology 2Dmesh-topology) + (nodeMemory 2Dmesh-nodeMemory))) + + + diff --git a/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/network/ring/network.lisp b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/network/ring/network.lisp new file mode 100644 index 0000000..55f6f90 --- /dev/null +++ b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/network/ring/network.lisp @@ -0,0 +1,46 @@ +#|$ACL2s-Preamble$; +(begin-book);$ACL2s-Preamble$|# + +(in-package "ACL2") + +(include-book "../../../generic-modules/network"); +(include-book "../../../generic-modules/types"); + + +(defun node-connections (id max topo) + ;; Build a list with node ids the node with id x is connected to. + ;; This first value will be nil since the local port is not connected to another node. + ;; examples: (connections 2 3) = (nil 1 3), (connections 3 3) = (nil 2 0) + ;; + ;; Arguments: + ;; - node : a node + ;; - ports : alist of ports + (if (zp id) + topo + (let* ((nodeid (1- id)) + (cw (if (equal nodeid (1- max)) + (acons (list nodeid 'cw ) (list 0 'ccw ) topo) + (acons (list nodeid 'cw ) (list (1+ nodeid) 'ccw ) topo))) + (ccw (if (equal nodeid 0) + (acons (list nodeid 'ccw ) (list (1- max) 'cw ) cw ) + (acons (list nodeid 'ccw ) (list (1- nodeid) 'cw ) cw))) + + (local (acons (list nodeid 'loc ) (list nodeid nil ) ccw))) + + (node-connections (1- id) max local)))) + +(defun ring-topology (x) + (node-connections x x nil)) + +(defun nodeMemory_t (x y) + (if (zp x) + (acons x y nil) + (acons x y (nodeMemory_t (1- x) y)))) + +(defun ring-nodeMemory (x) + (nodeMemory_t (1- x) x)) + +(definstance GenericNetwork check-compliance-ring-network + :functional-substitution + ((topology ring-topology) + (nodeMemory ring-nodeMemory)))
\ No newline at end of file diff --git a/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/network/spidergon/network.lisp b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/network/spidergon/network.lisp new file mode 100644 index 0000000..3a32984 --- /dev/null +++ b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/network/spidergon/network.lisp @@ -0,0 +1,47 @@ +#|$ACL2s-Preamble$; +(begin-book);$ACL2s-Preamble$|# + +(in-package "ACL2") + +(include-book "../../../generic-modules/network"); +(include-book "../../../generic-modules/types"); + +(defun node-connections (id n topo) + ;; Build a list with node ids the node with id x is connected to. + ;; This first value will be nil since the local port is not connected to another node. + ;; examples: (connections 2 3) = (nil 1 3), (connections 3 3) = (nil 2 0) + ;; + ;; Arguments: + ;; - node : a node + ;; - ports : alist of ports + (if (zp id) + topo + (let* ((nodeid (1- id)) + (cw (if (equal nodeid (1- (* 4 n))) + (acons (list nodeid 'cw ) (list 0 'ccw ) topo) + (acons (list nodeid 'cw ) (list (1+ nodeid) 'ccw ) topo))) + (ccw (if (equal nodeid 0) + (acons (list nodeid 'ccw ) (list (1- (* 4 n)) 'cw ) cw ) + (acons (list nodeid 'ccw ) (list (1- nodeid) 'cw ) cw))) + (acr (acons (list nodeid 'acr ) (list (mod (+ (* 2 n) nodeid) (* 4 n)) 'acr ) ccw)) + (local (acons (list nodeid 'loc )(list nodeid nil ) acr))) + + (node-connections (1- id) n local)))) + +(defun spidergon-topology (x) + (node-connections (* 4 x) x nil)) + +(defun nodeMemory_t (x y) + (if (zp x) + (acons x y nil) + (acons x y (nodeMemory_t (1- x) y)))) + +(defun spidergon-nodeMemory (x) + (nodeMemory_t (1- (* 4 x)) x)) + +(definstance GenericNetwork check-compliance-spidergon-network + :functional-substitution + ((topology spidergon-topology) + (nodeMemory spidergon-nodeMemory)))#|ACL2s-ToDo-Line|# + + diff --git a/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/routecontrol/spidergon/routecontrol.lisp b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/routecontrol/spidergon/routecontrol.lisp new file mode 100644 index 0000000..a59251e --- /dev/null +++ b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/routecontrol/spidergon/routecontrol.lisp @@ -0,0 +1,79 @@ +#|$ACL2s-Preamble$; +(begin-book);$ACL2s-Preamble$|# + +(in-package "ACL2")#|ACL2s-ToDo-Line|# + + +(include-book "../../../generic-modules/routecontrol") +; +;; RouteControl +;; + +(defun msg-header (msg) + (DestT msg)) + +(defun msg-tail (msg) + (not (FlitT msg))) + + +(defun portUpdateRoute (port out-port-id) + ;; Update the value of the localstatus. Which is the routing field with the out-port-id. + ;; + ;; Arguments: + ;; - port : a port + ;; - out-put-id : Port id of the port should be routed to. + (if (port-bufferHead port) + (port-updateStatus port (status-updatelocal (port-status port) (update-nth 0 out-port-id (port-statusLocal port)))) + (port-updateStatus port (status-updatelocal (port-status port) (update-nth 0 out-port-id (port-statusLocal port)))))) + + + +(defun spidergonRoutingLogic (s d n) + ;; calculate the the output port. + ;; + ;; Arguments: + ;; - s : current node id + ;; - d : destination node id + ;; - n : number of nodes mod 4 + + (cond ((equal s d) + 'loc) + ((and (< 0 (mod (- d s) (* 4 n))) + (<= (mod (- d s) (* 4 n)) n)) + 'cw) + ((<= (* 3 n) (mod (- d s) (* 4 n))) + ;;we go ccw + 'ccw) + (t ;; we go accross + 'acr))) + + +(defun routePorts (ports size) + ;; If a input port is has a msg in its buffer that has as destination this node route it to the local output port, else + ;; Route it to the clockwize output port. + ;; + ;; Arguments: + ;; - ports : a list ports + ;; - id : node id + ;; - size : number of nodes in the network + (if (endp ports) + nil + (let* ((port (car ports)) + (dest_id (destT (port-bufferHead port)))) + (if (and (equal (port-dir port) 'in) + (msg-header (port-bufferHead port))) + ;;If the message is at its destination route to local output port + ;; else route clockwize + (cons (portUpdateRoute port (SpidergonRoutingLogic (port-id port) dest_id size)) (RoutePorts (cdr ports) size)) + (cons port (RoutePorts (cdr ports) size)))))) + +(defun spidergon-routeControl (node memory) + ;; Route a node by trying to route its input ports. + (mv (routePorts node memory) memory)) + + +(definstance GenericRouteControl check-compliance-routecontrol + :functional-substitution + ((routecontrol spidergon-routeControl ))) + + diff --git a/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/routecontrol/xy/routecontrol.lisp b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/routecontrol/xy/routecontrol.lisp new file mode 100644 index 0000000..88d0415 --- /dev/null +++ b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/routecontrol/xy/routecontrol.lisp @@ -0,0 +1,75 @@ +#|$ACL2s-Preamble$; +(begin-book);$ACL2s-Preamble$|# + +(in-package "ACL2") + +(include-book "../../../generic-modules/routecontrol") +; +;; RouteControl +;; + +(defun msg-header (msg) + ;; Return the destination of the message + (DestT msg)) + +(defun portUpdateRoute (port out-port-id) + ;; Update the value of the localstatus. Which is the routing field with the out-port-id. + ;; + ;; Arguments: + ;; - port : a port + ;; - out-put-id : Port id of the port should be routed to. + (if (port-bufferhead port) + (port-updatestatus port (status-updateLocal (port-status port) (list out-port-id))) + (port-updatestatus port (status-updateLocal (port-status port) (list nil))))) + + +(defun XYRoutingLogic (current to) + ;; Compute the output port in order to reach the destination node. + ;; In XY routing first the horizontal distinance is reduced (x coord) + ;; If there is no horizaontal diffrence the vertical distance is reduced. + ;; Finaly if the message is a the destination node the message is routed to the local output. + + ;; Arguments: + ;; - current : coords of the current node. + ;; - to : coords of the destination node. + (let ((x_d (car to)) + (y_d (cadr to)) + (x_o (car current)) + (y_o (cadr current))) + (if (equal current to) + 'loc + (if (not (equal x_d x_o)) + (if (< x_d x_o) + 'W + 'E) + (if (< y_d y_o) + 'N + 'S)))))#|ACL2s-ToDo-Line|# + + +(defun routePorts (ports) + ;; If a input port is has a msg in its buffer that has as destination this node route it to the local output port, else + ;; Route it to the clockwize output port. + ;; + ;; Arguments: + ;; - ports : a list ports + (if (endp ports) + nil + (let* ((port (car ports)) + (dest_id (destT (port-bufferhead port)))) + (if (and (equal (port-dir port) 'in) + (msg-header (port-bufferHead port))) + (cons (portUpdateRoute port (XYRoutingLogic (port-id port) dest_id )) + (RoutePorts (cdr ports))) + (cons port (RoutePorts (cdr ports))))))) + +(defun xy-routeControl (node memory) + + ;; Route a node by trying to route its input ports. + (mv (routePorts node) memory)) + +(definstance GenericRouteControl check-compliance-routecontrol + :functional-substitution + ((routecontrol xy-routeControl ))) + + diff --git a/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/router/XY-circuit/router.lisp b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/router/XY-circuit/router.lisp new file mode 100644 index 0000000..a7090ab --- /dev/null +++ b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/router/XY-circuit/router.lisp @@ -0,0 +1,28 @@ +#|$ACL2s-Preamble$; +(begin-book);$ACL2s-Preamble$|# + +(in-package "ACL2") + +(include-book "../../../generic-modules/router") +(include-book "../../datalink/simple/datalink") +(include-book "../../routecontrol/xy/routecontrol") +(include-book "../../flowcontrol/circuit/flowcontrol") + +(defun XY-circuit-router (node memory) + ;; This function represents the router component of a Node. + ;; Applies the different processes in a router in the correct order. The RouterControl and FlowControl get as arguments the memory. + ;; + ;; Arguments: + ;; - node : list of ports in a node + ;; - memory : the global memory of a node + (mv-let (node memory) + (xy-RouteControl (simple-ProcessInputs node) memory) + (mv-let (node memory) + (circuit-Flowcontrol node memory) + (mv (simple-ProcessOutputs node) memory)))) + +(definstance GenericRouter check-compliance-router + :functional-substitution + ((router XY-circuit-router))) + + diff --git a/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/router/XY-packet/router.lisp b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/router/XY-packet/router.lisp new file mode 100644 index 0000000..a533ede --- /dev/null +++ b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/router/XY-packet/router.lisp @@ -0,0 +1,28 @@ +#|$ACL2s-Preamble$; +(begin-book);$ACL2s-Preamble$|# + +(in-package "ACL2") + +(include-book "../../../generic-modules/router") +(include-book "../../datalink/simple/datalink") +(include-book "../../routecontrol/xy/routecontrol") +(include-book "../../flowcontrol/packet/flowcontrol") + +(defun XY-packet-router (node memory) + ;; This function represents the router component of a Node. + ;; Applies the different processes in a router in the correct order. The RouterControl and FlowControl get as arguments the memory. + ;; + ;; Arguments: + ;; - node : list of ports in a node + ;; - memory : the global memory of a node + (mv-let (node memory) + (xy-RouteControl (simple-ProcessInputs node) memory) + (mv-let (node memory) + (packet-Flowcontrol node memory) + (mv (simple-ProcessOutputs node) memory)))) + +(definstance GenericRouter check-compliance-router + :functional-substitution + ((router XY-packet-router))) + + diff --git a/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/router/XY-wormhole/router.lisp b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/router/XY-wormhole/router.lisp new file mode 100644 index 0000000..fbdf671 --- /dev/null +++ b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/router/XY-wormhole/router.lisp @@ -0,0 +1,28 @@ +#|$ACL2s-Preamble$; +(begin-book);$ACL2s-Preamble$|# + +(in-package "ACL2") + +(include-book "../../../generic-modules/router") +(include-book "../../datalink/simple/datalink") +(include-book "../../routecontrol/xy/routecontrol") +(include-book "../../flowcontrol/wormhole/flowcontrol") + +(defun XY-wormhole-router (node memory) + ;; This function represents the router component of a Node. + ;; Applies the different processes in a router in the correct order. The RouterControl and FlowControl get as arguments the memory. + ;; + ;; Arguments: + ;; - node : list of ports in a node + ;; - memory : the global memory of a node + (mv-let (node memory) + (xy-RouteControl (simple-ProcessInputs node) memory) + (mv-let (node memory) + (wormhole-Flowcontrol node memory) + (mv (simple-ProcessOutputs node) memory)))) + +(definstance GenericRouter check-compliance-router + :functional-substitution + ((router XY-wormhole-router))) + + diff --git a/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/router/spidergon/router.lisp b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/router/spidergon/router.lisp new file mode 100644 index 0000000..57510dc --- /dev/null +++ b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/router/spidergon/router.lisp @@ -0,0 +1,28 @@ +#|$ACL2s-Preamble$; +(begin-book);$ACL2s-Preamble$|# + +(in-package "ACL2") + +(include-book "../../../generic-modules/router") +(include-book "../../datalink/simple/datalink") +(include-book "../../routecontrol/spidergon/routecontrol") +(include-book "../../flowcontrol/wormhole/flowcontrol") + +(defun spidergon-router (node memory) + ;; This function represents the router component of a Node. + ;; Applies the different processes in a router in the correct order. The RouterControl and FlowControl get as arguments the memory. + ;; + ;; Arguments: + ;; - node : list of ports in a node + ;; - memory : the global memory of a node + (mv-let (node memory) + (spidergon-RouteControl (simple-ProcessInputs node) memory) + (mv-let (node memory) + (wormhole-Flowcontrol node memory) + (mv (simple-ProcessOutputs node) memory)))) + +(definstance GenericRouter check-compliance-router + :functional-substitution + ((router spidergon-router))) + + diff --git a/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/simulation/circuit-XY-2dmesh/mybook.lsp b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/simulation/circuit-XY-2dmesh/mybook.lsp new file mode 100644 index 0000000..cbcf0e7 --- /dev/null +++ b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/simulation/circuit-XY-2dmesh/mybook.lsp @@ -0,0 +1,29 @@ +(include-book "misc/file-io" :dir :system) +(include-book "../../genoc/circuit-XY-2Dmesh/GeNoC") + +(set-state-ok t) +(set-ignore-ok t) + +(defun demo (Trlst size timelimit filename state ) + (declare (xargs :stobjs state :mode :program)) + (mv-let (Responses Aborted accup) + (INST-genoc Trlst ; Compute missives from travel list + size ; param + timeLimit; number of simulation steps + ) + (write-list (list (cons 'RESPONSES Responses) + (cons 'ABORTED Aborted) + accup) filename 'top-level state))) + +(defconst *size* 2) +(defconst *TransactionList* '((1 (0 0) "hallo1" (1 1) 1 0))) + + + +(defconst *TimeLimit* 10) +(demo *TransactionList* *size* *TimeLimit* "demo.txt" state)#|ACL2s-ToDo-Line|# + + + + + diff --git a/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/simulation/packet-XY-2Dmesh/mybook.lsp b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/simulation/packet-XY-2Dmesh/mybook.lsp new file mode 100644 index 0000000..c09b05c --- /dev/null +++ b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/simulation/packet-XY-2Dmesh/mybook.lsp @@ -0,0 +1,34 @@ +(include-book "misc/file-io" :dir :system) +(include-book "../../genoc/packet-XY-2Dmesh/GeNoC") + +(set-state-ok t) +(set-ignore-ok t) + +(defun demo (Trlst size timelimit filename state ) + (declare (xargs :stobjs state :mode :program)) + (mv-let (Responses Aborted accup) + (INST-genoc Trlst ; Compute missives from travel list + size ; param + timeLimit; number of simulation steps + ) + (write-list (list (cons 'RESPONSES Responses) + (cons 'ABORTED Aborted) + accup) filename 'top-level state))) + +(defconst *size* 2) +(defconst *TransactionList* '((1 (0 0) "hallo1" (1 1) 1 0) + (1 (1 1) "hallo1" (0 0) 1 0))) +(defconst *TimeLimit* 10) + +(demo *TransactionList* *size* *TimeLimit* "demo.txt" state)#|ACL2s-ToDo-Line|# + + + + + + + + + + + diff --git a/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/simulation/spidergon/mybook.lsp b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/simulation/spidergon/mybook.lsp new file mode 100644 index 0000000..09cf730 --- /dev/null +++ b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/simulation/spidergon/mybook.lsp @@ -0,0 +1,45 @@ +(include-book "misc/file-io" :dir :system) +(include-book "../../genoc/spidergon/GeNoC") + +(set-state-ok t) +(set-ignore-ok t) + +(defun demo (Trlst size timelimit filename state ) + (declare (xargs :stobjs state :mode :program)) + (mv-let (Responses Aborted accup) + (INST-genoc Trlst ; Compute missives from travel list + size ; param + timeLimit; number of simulation steps + ) + (write-list (list (cons 'RESPONSES Responses) + (cons 'ABORTED Aborted) + accup) filename 'top-level state))) + +(defconst *size* 2) +(defconst *TransactionList* '((1 0 "header" 2 2 0) + (1 0 "data" nil 1 0) + (1 0 "tail" nil 0 0) + (2 1 "header" 5 2 0) + (2 1 "data" nil 1 0) + (2 1 "data" nil 1 0) + (2 1 "data" nil 1 0) + (2 1 "tail" nil 0 0))) + + +(defconst *TimeLimit* 10) + +(trace* genoc) + + +(demo *TransactionList* *size* *TimeLimit* "demo.txt" state)#|ACL2s-ToDo-Line|# + + + + + + + + + + + diff --git a/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/simulation/wormhole-XY-2dmesh/mybook.lsp b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/simulation/wormhole-XY-2dmesh/mybook.lsp new file mode 100644 index 0000000..6dc4581 --- /dev/null +++ b/books/workshops/2009/vandenbroek-schmaltz/GeNoC/instantiations/simulation/wormhole-XY-2dmesh/mybook.lsp @@ -0,0 +1,45 @@ +(include-book "misc/file-io" :dir :system) +(include-book "../../genoc/wormhole-XY-2Dmesh/GeNoC") + +(set-state-ok t) +(set-ignore-ok t) + +(defun demo (Trlst size timelimit filename state ) + (declare (xargs :stobjs state :mode :program)) + (mv-let (Responses Aborted accup) + (INST-genoc Trlst ; Compute missives from travel list + size ;Generate topology + timeLimit; 10 attempts + ) + (write-list (list (cons 'RESPONSES Responses) + (cons 'ABORTED Aborted) + accup) filename 'top-level state))) + +(defconst *size* 2) +(defconst *TransactionList* '((1 (0 0) "header" (1 1) 2 0) + (1 (0 0) "data" nil 1 0) + (1 (0 0) "tail" nil 0 0) + (2 (1 0) "header" (1 1) 2 0) + (2 (1 0) "data" nil 1 0) + (2 (1 0) "data" nil 1 0) + (2 (1 0) "data" nil 1 0) + (2 (1 0) "tail" nil 0 0) + )) + + + +(defconst *TimeLimit* 20) + +(demo *TransactionList* *size* *TimeLimit* "demo.txt" state)#|ACL2s-ToDo-Line|# + + + + + + + + + + + + |