diff options
Diffstat (limited to 'src/mem/slicc')
| -rw-r--r-- | src/mem/slicc/doc/SLICC_V03.txt | 307 | ||||
| -rw-r--r-- | src/mem/slicc/doc/tutorial.tex | 574 |
2 files changed, 0 insertions, 881 deletions
diff --git a/src/mem/slicc/doc/SLICC_V03.txt b/src/mem/slicc/doc/SLICC_V03.txt deleted file mode 100644 index 1c2a95a39..000000000 --- a/src/mem/slicc/doc/SLICC_V03.txt +++ /dev/null @@ -1,307 +0,0 @@ -SLICC - Version 0.3 Design Document - January 17, 1999 -Milo Martin and Dan Sorin - -Question: Rethinking of support for profiling the transactions - -Question: How do we deal with functions/methods and resources - -Comment: We need to discuss the sequencer interface so it can work now - and for the speculative version buffer. - -Overview --------- - -We are in the process of designing and implementing SLICC v0.3, an -evolution of SLICC v0.2. The new design includes capabilities for -design of multilevel cache hierarchies including the specification of -multiple protocol state machines (PSMs) and the queues which connect -these PSMs and the network. We actually believe that most of the -network and network topology, including the ordered network, can be -expressed using the new hierarchical extensions to the language. - -In addition, many implicit aspects of the language will be eliminated -in favor of explicit declarations. For example functions, queues, and -objects declarations such as "cacheMemory" and "TBETable" will be -explicitly declared. This will allow for full static type checking -and easier extension for the language. Event triggering will be part -of "in_port" declarations and not "event" declarations. Finally, many -less fundamental, but important, features and internal code -improvements will be enhanced. - -SLICC History -------------- - -v0.1 - Initially the language only handled the generation of the PSM - transition table logic. All actions and event triggering were - still coded in C++. At this point it was still called, "the - language." - -v0.2 - Extended the language to include a simple C like syntax for - specifying actions, event triggering, and manipulating queues - and state elements. This version was the first version of the - language known as SLICC (suggested by Amir) and was used for - the Multifacet ISCA 2000 submission. - -v0.3 - Development effort started January 2000. Intended features and - enhancements are described by this document. - -Specifying Hierarchical Designs -------------------------------- - -Right now all of our protocols have two tables, a processor/cache PSM -and a directory PSM. In v0.2 this is a rigid requirement and -the names are implicit. SLICC v0.3 will allow for an arbitrary number -of different PSMs. - -The most significant improvement in v0.3 is the ability for the user -to define an arbitrary set of interconnected PSMs. PSMs may include -an L1 cache controller, L2 cache controller, directory controller, -speculative version buffer, network interface, etc. There are a -couple of "primitive PSMs" such as the sequencer. - -There will be a notion of a "node" of the system. In a node, each PSM -will be instantiated and connected together with queues. For example, -assume we define a PSMs and want to create a queue of RequestMessages -to communicate between it and the network. - - machine(CacheController) { - ... - out_port(to_network, RequestMessage, "To the network", desc="..."); - ... - } - - CacheController cache, desc="..."; - - connect(cache.to_network, network.from_cache, ordered="yes", desc="..."); - -Explicit State Manipulation ---------------------------- - -As before, PSMs have states, events, and transitions. New in v0.3 each -PSM must have user defined methods for get_state(address) and -set_state(address, state), and these methods are written explicitly, -instead of being implicit functions of memory states (e.g., our -current implementation which implicitly uses the TBE state if there is -a TBE or uses the cache state). Functions have a return value, -procedures do not. Function calls are expressions, procedure calls -are statements. All function and procedure parameters are considered -pass-by-value. - - procedure set_state(Address addr, State state) { - ... - } - - function State get_state(Address addr) { - ... - } - -Explicit Declaration --------------------- - -PSMs reference or declare structures, such as queues, ports, cache -memories, main memory, TBEs, write buffers, etc. These primitive -types and structures are written in C++, and their semantics are still -specified by the C++ coder. Examples of these primitive types include -"CacheMemory," "TBETable," as well as various types of queues. - -One major difference is that in v0.3 the interface for all of these -primitive objects will be declared (but not defined) in the SLICC -language. This also allows adding primitive structures by defining a -C++ implementation and a SLICC interface specification. This will -make the language much more extensible. Specifying the interface of -these primitive types, structures, and queues in SLICC will eliminate -much of the implicit semantics that is currently hiding in the -controllers. - -The interface declaration might be in one file and shared between all -protocols. The object instantiation would be internal to each PSM -that requires a cache memory. The syntax for messages will also be -enhanced by using this new syntax. Notice the support for default -values. - - structure(CacheMemory, "Cache memory", desc="...") { - void cache_change_state(Address addr, State state), desc="..."; - Data dataBlk, default="", desc=""; - bool cache_avail(Address addr), desc="..."; - Address cache_probe(Address addr), desc="..."; - void cache_allocate(Address addr), desc="..."; - } - - CacheMemory L1cacheMemory, desc="..."; - -Structure specification is going to require the introduction of an -object model in the language. The "." (dot) operator is going to be -extended beyond the use as structure element access, but also allow -for a object method call syntax similar to C++ and Java. - - L1cacheMemory.cache_allocate(addr); - -Polymorphism ------------- - -We are also going to want to allow for polymorphism for many of the -structures. We already have a limited degree of polymorphism between -different protocols by using the same cache memory structure with -different "CacheEntry" types in each protocol. Now that we are going -to have multiple levels of cache, each requiring slightly different -state bits, we are going to want to specify cache memory structures -which have different "CacheEntry" types in the same protocol. To do -this right, this is going to require adding full polymorphism support -to the language. Right now we imagine something like C++'s templates, -since they are a more natural fit to hardware synthesis in the future. - -Type Checker ------------- - -All of the above substantially complicates our type system by -requiring more types and scoping rules. As a step towards -understanding the implications of the type system, a type checking -system will be implemented. This is a hard requirement if we are ever -to distribute the system since receiving compile time errors in the -generated code is not acceptable. In order to ensure that we don't -accidentally design a language that is not statically type checkable, -it is important to add the type checker sooner rather than later. - -Event Triggering ----------------- - -In v0.2, PSM events were individually specified as sets of conditions. -The following SLICC v0.2 code is a simplified example from the origin -protocol. - - event(Dir_data_ack_0, "Data ack 0", desc="... ack count == 0") { - if (queue_ready(responseNetwork)) { - peek(responseNetwork, ResponseMsg) { - if(in_msg.NumPendingAcks == 0) { - trigger(in_msg.Address); - } - } - } - } - - event(Dir_data_ack_not_0, "Data ack not 0", desc="... ack count != 0") { - if (queue_ready(responseNetwork)) { - peek(responseNetwork, ResponseMsg) { - if(in_msg.NumPendingAcks != 0) { - trigger(in_msg.Address); - } - } - } - } - -The above code defines the exact conditions for the events to be -triggered. This type of event specification led to redundant code and -numerous bugs where conditions for different events were not -completely orthogonal. - -In v0.3, events will be declared with no accompanying code (similar to -how states are specified). Instead, the code that determines which -event is triggered will be part of each incoming port's declaration. -This approach should eliminate redundancy and bugs in trigger -conditions. The v0.3 code for the above would look like: - - event(Dir_data_ack_0, "Data ack 0", desc="... ack count = 0"); - event(Dir_data_ack_not_0, "Data ack not 0", desc="... ack count != 0"); - - in_port(responseNetwork, ResponseMsg, "Response Network", desc="...") { - if(in_msg.NumPendingAcks == 0) { - trigger(Dir_data_ack_0, in_msg.Address); - } else { - trigger(Dir_data_ack_not_0, in_msg.Address); - } - } - -Notice that one no longer needs to explicitly check if the queue is -ready or to perform the peek operation. - -Also notice that the type of messages that arrives on the port is -explicitly declared. All ports, incoming and outgoing, are now -explicitly type channels. You will still be required to include the -type of message when manipulating the queue. The type specified will -be statically type checked and also acts as self-documenting code. - -Other Improvements ------------------- - -There will be a number of other improvements in v0.3 such as general -performance tuning and clean up of the internals of the compiler. The -compiler will be modified to operate on multiple files. In addition, -the abstract syntax tree internal to the code will need to be extended -to encompass more information, including information parsed in from -multiple files. - -The affiliates talk and the document for the language should also be -updated to reflect the changes in the new version. - -Looking Forward ---------------- - -When designing v0.3 we are keeping future plans in mind. - -- When our designs of the multilevel cache hierarchy are complete, we - expect to have a large amount of replication between the protocols - and caches controllers within a protocol. For v0.4 we hope to look - at the patterns that have evolved and look for ways in which the - language can capture these patterns. Exploiting reuse will provide - quicker protocol development and maintainability. - -- By keeping the specification structural, we are looking towards - generating VHDL/Verilog from SLICC. The type system will help this, - as will more explicit instantiation and declaration of types and - structures. The structures now written in C++ (sequencer, network, - cache arrays) will be ported to the HDL we select. The rest of the - controllers will be generated by the compiler. At first the - generated controller will not be optimized. I believe that with - more effort we can automatically generate reasonably optimized, - pipelined implementation of the controllers. - -Implementation Plan -------------------- - -- HTML generator -- Extend internal parser AST nodes -- Add get_state function and set_state procedure declarations -- Move trigger logic from events to in_ports -- Types - - Change type declaration syntax - - Declare primitive types and corresponding C++ types - - Add default values to structures and types - - Add object method call syntax - - Write type checker -- Documentation - - Revise document - - Update presentation - -Document History ----------------- - -$Id: SLICC_V03.txt,v 3.0 2000/09/12 20:27:59 sorin Exp $ - -$Log: SLICC_V03.txt,v $ -Revision 3.0 2000/09/12 20:27:59 sorin -Version 3.0 signifies a checkpoint of the source tree right after the -final draft of the ASPLOS '00 paper. - -Revision 1.1.1.1 2000/03/09 10:18:38 milo -Initial import - -Revision 2.0 2000/01/19 07:21:13 milo -Version 2.0 - -Revision 1.5 2000/01/18 10:26:24 milo -Changed the SLICC parser so that it generates a full AST. This is the -first step in moving towards v0.3 - -Revision 1.4 2000/01/17 18:36:15 sorin -*** empty log message *** - -Revision 1.3 2000/01/15 10:30:16 milo -Added implementation list - -Revision 1.2 2000/01/15 08:11:44 milo -Minor revisions - -Revision 1.1 2000/01/15 07:14:17 milo -Converted Dan's first draft into a text file. Significant -modifications were made. - diff --git a/src/mem/slicc/doc/tutorial.tex b/src/mem/slicc/doc/tutorial.tex deleted file mode 100644 index c20dba156..000000000 --- a/src/mem/slicc/doc/tutorial.tex +++ /dev/null @@ -1,574 +0,0 @@ -%& latex -\documentclass[11pt]{article} -\usepackage{graphics} -\usepackage{color} - -\textheight 9.0 in -\topmargin -0.5 in -\textwidth 6.5 in -\oddsidemargin -0.0 in -\evensidemargin -0.0 in - -\begin{document} - -\definecolor{dark}{gray}{0.5} - -\newcommand{\syntax}[1]{% -\begin{center} -\fbox{\tt \small -\begin{tabular}{l} -#1\end{tabular}}\end{center}} - -\begin{center} -{\LARGE Tutorial for SLICC v0.2} \\ -\vspace{.25in} -{\large Milo Martin} \\ -{\large 8/25/1999} -\end{center} - -\section*{Overview} - -This document attempts to illustrate the syntax and expressiveness of -the cache coherence protocol specification language through a small -example. A ``stupido'' cache coherence protocol is described in prose -and then expressed in the language. - -The protocol used as the running example is described. Then each of -the elements of the protocol is discussed and expressed in the -language: states, events, transitions, and actions. - -\section*{Protocol Description} - -In order to make this example a simple as possible, the protocol -described is a simple as possible and makes many simplifying -assumptions. These simplifications were made only to clarify the -exposition and are not indications of limitations of the -expressiveness of the description language. We have already specified -a more complicated MSI broadcast snooping protocol, a multicast -snooping protocol, and a directory protocol. The simplifying -assumptions are listed below. The remaining details of the protocol -are described in the sections where we give the syntax of the -language. - -\begin{itemize} - -\item -The protocol uses broadcast snooping that assumes that a broadcast can -only occur if all processors have processed all of their incoming -address transactions. In essence, when a processor issue an address -request, that request will be next in the global order. This allows -us to avoid needed to handle the cases before we have observed our -request in the global order. - -\item -The protocol has only Modified and Idle stable states. (Note: Even -the Shared state is omitted.) - -\item -To avoid describing replacement (PutX's) and writebacks, the caches -are in treated as infinite in size. - -\item -No forward progress bit is used, so the protocol as specified does not -guarantee forward progress. - -\item -Only the mandatory request queue is used. No optional or prefetch -queue is described. - -\item -The above simplifications reduce the need for TBEs (Translation Buffer -Entries) and thus the idea of a TBE is not include. - -\item -Each memory module is assumed to have some state associated with each -cache block in the memory. This requires a simple directory/memory -state machine to work as a compliment to the processor state machine. -Traditional broadcast snooping protocols often have no ``directory'' -state in the memory. - -\end{itemize} - -\section*{Protocol Messages} - -Cache coherence protocols communicate by sending well defined -messages. To fully specify a cache coherence protocol we need to be -able to specify the message types and fields. For this protocol we -have address messages ({\tt AddressMsg}) which are broadcast, and data -messages ({\tt DataMsg}) which are point-to-point. Address messages -have an address field ({\tt Address}), a request type ({\tt Type}), -and which processor made the request ({\tt Requestor}). Data message -have an address field ({\tt Address}), a destination ({\tt -Destination}), and the actual cache block being transfered ({\tt -DataBlk}). The names in parenthesis are important because those are -the names which code later in the specification will reference various -message types and fields in the messages. - -Messages are declared by creating types with {\tt new\_type()} and -adding fields with {\tt type\_field()}. The exact syntax for -declaring types and message is a bit ugly right now and is going to be -changed in the near future. If you wish, please see the appendix for -an example of the current syntax. - - - -\section*{Cache States} - -Idle and Modified are the two stable states in our protocol. In -addition the we have a single transient processor state. This state -is used after a processor has issued a request and is waiting for the -data response to arrive. - -Declaring states in the language is the first of a number of -declarations we will be using. All of these declarations have a -similar format. Below is the format for a state declaration. - -\syntax{ -{\tt state({\em identifier}, {\em shorthand}, {\em pair1}, {\em pair2}, ...);} -} - -{\em identifier} is a name that is used later to -refer to this state later in the description. It must start with a -letter and after than can have any combination of letters, numbers, -and the underscore character. {\em shorthand} is a quoted string -which contains the shorthand that should be used for the state when -generating tables and such. - -The {\em pair}'s are used to associate arbitrary information with each -state. Zero or more pairs can be included in each declaration. For -example we want to have a more verbose description of each state when -we generate the table which contains the states and descriptions. -This information is encoded in the language by adding a {\tt desc} -parameter to a declaration. The name of the parameter is followed by -an equal sign and a string with the description. The {\tt desc} pair -technically optional, however the table generation tool will complain -about a missing description if it is not present. - -The three states for our protocol are expressed as follows: - -\begin{verbatim} -state(I, "I", desc="Idle"); -state(M, "M", desc="Modified"); -state(IM, "IM", desc="Idle, issued request but have not seen data yet"); -\end{verbatim} - -\section*{Cache Events} - -Events are external stimulus that cause the state machine to take -action. This is most often a message in one of the queues from the -network or processor. Events form the columns of the protocol table. -Our simple protocol has one event per incoming queue. When a message -is waiting in one of these queues and event can occur. We can see a -request from the processor in the mandatory queue, another processor's -request, or a data response. - -Events are declared in the language similarly to states. The {\em -identifier}, {\em shorthand}, and {\em pair}'s have the same purpose -as in a state declaration. - -\syntax{ -event({\em identifier}, {\em shorthand}, {\em pair1}, {\em pair2}, ...) \{ \\ -\hspace{.1in} {\em statement\_list} \\ -\} \\ -} - -Events are different in that they have a list of statements which -allows exact specification of when the event should ``trigger'' a -transition. These statements are mini-programming language with -syntax similar to that of C. For example the {\tt peek} construct in -this context checks to see if there is a message at the head of the -specified queue, and if so, conceptually copies the message to a -temporary variable accessed as {\tt in\_msg}. The language also -supports various procedure calls, functions, conditional statements, -assignment, and queue operations such as peek, enqueue and dequeue. -The {\tt trigger()} construct takes an address as the only parameter. -This is the address that should be triggered for the event. To give -you a feel for what this code looks like, the three events for our -simple protocol are below. - -\begin{verbatim} -event(LoadStore, "LoadStore", desc="Load or Store request from local processor") { - peek(mandatoryQueue_ptr, CacheMsg) { - trigger(in_msg.Address); - } -} - -event(Other_GETX, "Other GETX", desc="Observed a GETX request from another processor") { - peek(addressNetwork_ptr, AddressMsg) { - if (in_msg.Requestor != id) { - trigger(in_msg.Address); - } - } -} - -event(Data, "Data", desc="Data for this block from the data network") { - peek(dataNetwork_ptr, DataMsg) { - trigger(in_msg.Address); - } -} -\end{verbatim} - -\section*{Cache Actions} - -Actions are the privative operations that are performed by various -state transitions. These correspond (by convention) to the lower case -letters in the tables. We need several actions in our protocol -including issuing a GetX request, servicing a cache hit, send data -from the cache to the requestor, writing data into the cache, and -popping the various queues. - -The syntax of an action declaration is similar to an event -declaration. The difference is that statements in the statement list -are used to implement the desired action, and not triggering an event. - -\syntax{action({\em identifier}, {\em shorthand}, {\em pair1}, {\em pair2}, ...) \{ \\ -\hspace{.1in} {\em statement\_list} \\ -\} -} - -The actions for this protocol use more of the features of the -language. Some of the interesting case are discussed below. - -\begin{itemize} - -\item -To manipulate values we need assignment statements (notice the use of -{\verb+:=+} as the assignment operator). The action to write data -into the cache looks at the incoming data message and puts the data in -the cache. Notice the use of square brackets to lookup the block in -the cache based on the address of the block. - -\begin{verbatim} -action(w_writeDataToCache, "w", desc="Write data from data message into cache") { - peek(dataNetwork_ptr, DataMsg) { - cacheMemory_ptr[address].DataBlk := in_msg.DataBlk; - } -} -\end{verbatim} - -\item -In addition to peeking at queues, we also enqueue messages. The {\tt -enqueue} construct works similarly to the {\tt peek} construct. {\tt -enqueue} creates a temporary called {\tt out\_msg}. You can assign -the fields of this message. At the end of the {\tt enqueue} construct -the message is implicitly inserted in the outgoing queue of the -specified network. Notice also how the type of the message is -specified and how the assignment statements use the names of the -fields of the messages. {\tt address} is the address for which the -event was {\tt trigger}ed. - -\begin{verbatim} -action(g_issueGETX, "g", desc="Issue GETX.") { - enqueue(addressNetwork_ptr, AddressMsg) { - out_msg.Address := address; - out_msg.Type := "GETX"; - out_msg.Requestor := id; - } -} -\end{verbatim} - -\item -Some times we need to use both {\tt peek} and {\tt enqueue} together. -In this example we look at an incoming address request to figure out -who to whom to forward the data value. - -\begin{verbatim} -action(r_cacheToRequestor, "r", desc="Send data from the cache to the requestor") { - peek(addressNetwork_ptr, AddressMsg) { - enqueue(dataNetwork_ptr, DataMsg) { - out_msg.Address := address; - out_msg.Destination := in_msg.Requestor; - out_msg.DataBlk := cacheMemory_ptr[address].DataBlk; - } - } -} -\end{verbatim} - -\item -We also need to pop the various queues. -\begin{verbatim} -action(k_popMandatoryQueue, "k", desc="Pop mandatory queue.") { - dequeue(mandatoryQueue_ptr); -} -\end{verbatim} - -\item -Finally we have the ability to call procedures and functions. The -following is an example of a procedure call. Currently all of the -procedures and functions are used to handle all of the more specific -operations. These are currently hard coded into the generator. - -\begin{verbatim} -action(h_hit, "h", desc="Service load/store from the cache.") { - serviceLdSt(address, cacheMemory_ptr[address].DataBlk); -} -\end{verbatim} - -\end{itemize} - -\section*{Cache Transitions} - -The cross product of states and events gives us the set of possible -transitions. For example, for our example protocol the empty would -be: - -\begin{center} -\begin{tabular}{|l||l|l|l|} \hline - & LoadStore & Other GETX & Data \\ \hline \hline -I & & & \\ \hline -M & & & \\ \hline -IM & & & \\ \hline -\end{tabular} -\end{center} - - -Transitions are atomic and are the heart of the protocol -specification. The transition specifies both what the next state, and -also what actions are performed for each unique state/event pair. The -transition declaration looks different from the other declarations: - -\syntax{ -transition({\em state}, {\em event}, {\em new\_state}, {\em pair1}, {\em pair2}, ...) \{ \\ -\hspace{.1in} {\em action\_identifier\_list}\\ -\} -} - -{\em state} and {\em event} are the pair which uniquely identifies the -transition. {\em state} correspond to the row where {\em event} -selects the column. {\em new\_state} is an optional parameter. If -{\em new\_state} is specified, that is the state when the atomic -transition is completed. If the parameter is omitted there is assumed -to be no state change. An impossible transition is specified by -simply not declaring an event for that state/event pair. - -We also place list of actions in the curly braces. The {\em -action\_identifier}'s correspond to the identifier specified as the -first parameter of an action declaration. The action list is a list -of operations to be performed when this transition occurs. The -actions also knows what preconditions are necessary are required for -the action to be performed. For example a necessary precondition for -an action which sends a message is that there is a space available in -the outgoing queue. Each transition is considered atomic, and thus -the generated code ensures that all of the actions can be completed -before performing and of the actions. - -In our running example protocol it is only possible to receive data in -the {\em IM} state. The other seven cases can occur and are declared -as follows. Below are a couple of examples. See the appendix for a -complete list. - -\newpage -\begin{verbatim} -transition(I, LoadStore, IM) { - g_issueGETX; -} - -transition(M, LoadStore) { - h_hit; - k_popMandatoryQueue; -} - -transition(M, Other_GETX, I) { - r_cacheToRequestor; - i_popAddressQueue; -} -\end{verbatim} - -From the above declarations we can generate a table. Each box can -have lower case letters which corresponds to the list of actions -possibly followed by a slash and a state (in uppercase letters). If -there is no slash and state, the transition does not change the state. - -\begin{center} -\begin{tabular}{|l||l|l|l|} \hline - & LoadStore & Other GETX & Data \\ \hline \hline -I & g/IM & i & (impossible)\\ \hline -M & hk & ri/I & (impossible)\\ \hline -IM & z & z & wj/M \\ \hline -\end{tabular} -\end{center} - -There is a useful shorthand for specifying many transitions with the -same action. One or both of {\em event} and {\em state} can be a list -in curly braces. This defines the cross product of the sets in one -declaration. If no {\em new\_state} is specified none of the -transitions cause a state change. If {\em new\_state} is specified, -all of the transitions in the cross product of the sets has the same -next state. For example, in the below transitions both IM/LoadStore -and IM/Other\_GETX have the action {\tt z\_delayTrans}. -\begin{verbatim} -transition(IM, LoadStore) { - z_delayTrans; -} - -transition(IM, Other_GETX) { - z_delayTrans; -} -\end{verbatim} -These can be specified in a single declaration: -\begin{verbatim} -transition(IM, {LoadStore, Other_GETX}) { - z_delayTrans; -} -\end{verbatim} - - -\newpage -\section*{Appendix - Sample Cache Controller Specification} - -{\small -\begin{verbatim} -machine(processor, "Simple MI Processor") { - - // AddressMsg - new_type(AddressMsg, "AddressMsg", message="yes", desc=""); - type_field(AddressMsg, Address, "address", - desc="Physical address for this request", - c_type=PhysAddress, c_include="Address.hh", murphi_type=""); - type_field(AddressMsg, Type, "type", - desc="Type of request (GetS, GetX, PutX, etc)", - c_type=CoherenceRequestType, c_include="CoherenceRequestType.hh", murphi_type=""); - type_field(AddressMsg, Requestor, "requestor", - desc="Node who initiated the request", - c_type=ComponentID, c_include="ComponentID.hh", murphi_type=""); - - // DataMsg - new_type(DataMsg, "DataMsg", message="yes", desc=""); - type_field(DataMsg, Address, "address", - desc="Physical address for this request", - c_type=PhysAddress, c_include="Address.hh", murphi_type=""); - type_field(DataMsg, Destination, "destination", - desc="Node to whom the data is sent", - c_type=Set, c_include="Set.hh", murphi_type=""); - type_field(DataMsg, DataBlk, "data", - desc="Node to whom the data is sent", - c_type=DataBlock, c_include="DataBlock.hh", murphi_type=""); - - // CacheEntry - new_type(CacheEntry, "CacheEntry"); - type_field(CacheEntry, CacheState, "Cache state", desc="cache state", - c_type=CacheState, c_include="CacheState.hh", murphi_type=""); - type_field(CacheEntry, DataBlk, "data", desc="data for the block", - c_type=DataBlock, c_include="DataBlock.hh", murphi_type=""); - - // DirectoryEntry - new_type(DirectoryEntry, "DirectoryEntry"); - type_field(DirectoryEntry, DirectoryState, "Directory state", desc="Directory state", - c_type=DirectoryState, c_include="DirectoryState.hh", murphi_type=""); - type_field(DirectoryEntry, DataBlk, "data", desc="data for the block", - c_type=DataBlock, c_include="DataBlock.hh", murphi_type=""); - -\end{verbatim} -\newpage -\begin{verbatim} - // STATES - state(I, "I", desc="Idle"); - state(M, "M", desc="Modified"); - state(IM, "IM", desc="Idle, issued request but have not seen data yet"); - - // EVENTS - - // From processor - event(LoadStore, "LoadStore", desc="Load or Store request from local processor") { - peek(mandatoryQueue_ptr, CacheMsg) { - trigger(in_msg.Address); - } - } - - // From Address network - event(Other_GETX, "Other GETX", desc="Observed a GETX request from another processor") { - peek(addressNetwork_ptr, AddressMsg) { - if (in_msg.Requestor != id) { - trigger(in_msg.Address); - } - } - } - - // From Data network - event(Data, "Data", desc="Data for this block from the data network") { - peek(dataNetwork_ptr, DataMsg) { - trigger(in_msg.Address); - } - } - - // ACTIONS - action(g_issueGETX, "g", desc="Issue GETX.") { - enqueue(addressNetwork_ptr, AddressMsg) { - out_msg.Address := address; - out_msg.Type := "GETX"; - out_msg.Requestor := id; - } - } - - action(h_hit, "h", desc="Service load/store from the cache.") { - serviceLdSt(address, cacheMemory_ptr[address].DataBlk); - } - - action(i_popAddressQueue, "i", desc="Pop incoming address queue.") { - dequeue(addressNetwork_ptr); - } - - action(j_popDataQueue, "j", desc="Pop incoming data queue.") { - dequeue(dataNetwork_ptr); - } - - action(k_popMandatoryQueue, "k", desc="Pop mandatory queue.") { - dequeue(mandatoryQueue_ptr); - } - - action(r_cacheToRequestor, "r", desc="Send data from the cache to the requestor") { - peek(addressNetwork_ptr, AddressMsg) { - enqueue(dataNetwork_ptr, DataMsg) { - out_msg.Address := address; - out_msg.Destination := in_msg.Requestor; - out_msg.DataBlk := cacheMemory_ptr[address].DataBlk; - } - } - } - - action(w_writeDataToCache, "w", desc="Write data from data message into cache") { - peek(dataNetwork_ptr, DataMsg) { - cacheMemory_ptr[address].DataBlk := in_msg.DataBlk; - } - } - - action(z_delayTrans, "z", desc="Cannot be handled right now.") { - stall(); - } - - // TRANSITIONS - - // Transitions from Idle - transition(I, LoadStore, IM) { - g_issueGETX; - } - - transition(I, Other_GETX) { - i_popAddressQueue; - } - - // Transitions from Modified - transition(M, LoadStore) { - h_hit; - k_popMandatoryQueue; - } - - transition(M, Other_GETX, I) { - r_cacheToRequestor; - i_popAddressQueue; - } - - // Transitions from IM - transition(IM, {LoadStore, Other_GETX}) { - z_delayTrans; - } - - transition(IM, Data, M) { - w_writeDataToCache; - j_popDataQueue; - } -} -\end{verbatim} -} -\end{document} - |