Model Soc
Model Soc
Model Soc
2.1 Introduction
Modeling plays a central role in design automation of SoC architectures. The formal
modeling can not only help designers accurately describe the syntax and semantics
of a design, but can also enable the automatic analysis using corresponding tools.
This section presents two widely used formal models: the graph model for structure
modeling and the FSM model for behavior modeling. The combination of both
models can be used to capture the high-level abstraction of various complex SoC
designs.
Although the graph model can be used to describe the structural information, it is not
suitable to capture behavioral details. FSM is widely used for describing the internal
behavior of software/hardware components. For example, in hardware design, FSM
2.2 Modeling of Complex Systems 21
Instruction
PC Fetch Memory
RegFile Decode
MUL2 FADD2
Main
FADD3 Memory
MUL7 FADD4
Data
MEM Memory
Data Transfer
Instruction Flow
WriteBack Unit Storage
can be used to describe the state change of registers. In software design, FSM can
be used to describe the execution of a piece of sequential code. FSM models can be
derived from system-level specifications (e.g. ADL [7], SystemC TLM, UML).
Definition 2.2 A finite state machine M is a seven-tuple (I, O, S, , , si , s F ) where
I is a finite set of inputs.
O is a finite set of outputs.
S is a finite set of states.
is the state transition function : S I S.
is the output function : S I O.
si is an initial state, an element of S.
s F is the set of final states, a subset of S.
When the model M is in the state s (s S) and receives an input a (a I ), it
moves to the next state specified by (s, a) and produces an output given by (s, a).
For an initial state s1 , an input sequence x = a1 , . . . , ak takes the M successively to
states si+1 = (si , ai ), i = 1, . . . , k with the final state sk+1 .
22 2 Modeling and Specification of SoC Designs
As a framework built on C++, SystemC [10] mimics the hardware description lan-
guages such as VHDL and Verilog. With an event-driven simulation kernel, SystemC
can be used to simulate the behavior of concurrent processes which can commu-
nicate with each other using procedure calls or other mechanisms offered by the
SystemC library. Generally, SystemC is often associated with TLM [1, 11], because
SystemC TLM provides a wrapper to facilitate the process of communication model-
ing. Since SystemC TLM provides a rapid prototyping platform for the architecture
exploration and hardware/software integration [12], it is widely used to enable early
exploration for both hardware and software designs. It can reduce the overall design
and validation efforts of complex SoC architectures.
To enable automated analysis, various researchers have tried to extract formal rep-
resentations from SystemC TLM specifications. Abdi et al. [13] introduced Model
Algebra, a formalism for representing SoC designs at system level. The work by
Kroening et al. [14] formalized the semantics of SystemC by means of labeled Kripke
structures. Moy et al. [15] provided a compiler front-end that can extract architec-
ture and synchronization information from SystemC TLM designs using HPIOM.
Karlsson et al. [16] translated SystemC models into a Petri-Net based representation
PRES+. This model can be used for model checking of properties expressed in a
timed temporal logic. Habibi et al. [17] proposed a method that adopts the formal
model AsmL. A state machine generated from AsmL can be verified, and then can be
translated into both SystemC code and properties for low-level validation. All these
modeling techniques focus on the formal modeling of SystemC specifications. This
section discusses how to extract the formal models from SystemC TLM specifications
to enable automated test generation.
(i.e., C++ objects). The initial process starts a communication, and the target process
passively responds to the communication. Similar to the producer/consumer mod-
els, each process does the following tasks: consuming data, processing data, and
producing data.
Since SystemC is based on C++, it supports various programming constructs
(e.g., template, inheritance, etc.). Although the concept of some TLM components
(signals, ports, etc.) is easy, their C++ implementation details are really complex.
Therefore, it is difficult to directly translate their behaviors to enable automated vali-
dation. In this chapter, abstraction of certain SystemC components is used to hide the
implementation details using the predefined SMV constructs. The underlying com-
plex SystemC scheduler aggravates the modeling complexity. For SystemC TLM,
to mimic the parallel execution of processes, the SystemC scheduler activates the
ready-to-run processes in a non-deterministic way. Depending on the target model,
translation of SystemC scheduler may or may not be required. For example, while
translating SystemC TLM specification into SMV model, it is not necessary to model
the SystemC scheduler explicitly since SMV inherently supports parallel execution.
For TLM, two most important factors are the transaction data token and the
transaction flow. So the extracted formal model of TLM specifications should reflect
both information. The extracted models should not only guide the generation of
SMV specification, but should also enable automatic generation of properties and
tests. Definition 2.3 provides the formal model of SystemC TLM designs.
Definition 2.3 The formal model of a SystemC TLM design is an eight-tuple
(, P, T, A, E, M, I, F) where
is a set of transaction data tokens.
P = { p1 , p2 , . . . , pm } is a set of places.
T = {t1 , t2 , . . . , tn } is a set of transitions.
A {P T } {T P} is a set of arcs between places and transitions.
E = {e1 , e2 , . . . , ek } is a set of arc expressions. The mapping Expression (ai ) = ei
(ai A, 1 i k) provides the enable condition ei for ai . A token can pass arc
ai only when ei is true.
M : 2 P T 2 P is a function that describes the internal operations on
input transaction data and output transaction data of a transition.
I 2 P specifies the initial state.
F 2 P specifies the final states.
Graph model can be used as an immediate form to capture the execution as well
as interconnection of processes.
Figure 2.2a shows an interconnection of six modules. Each arrow indicates a port
binding between two modules. Figure 2.2b shows the graph representation of its
corresponding formal model. In the graph model, each circle (node) is called a place
that is used to indicate the input or output buffer of a module. It can temporarily
hold the transaction data for later processing. The edges (vertical bars with incoming
and outgoing arrow lines) are transitions, which are used to indicate modules that
contain processes to manipulate input and output transaction data tokens. The places
24 2 Modeling and Specification of SoC Designs
(a) (b)
t1 t5
M5
M1 t3
M3
t6
t2
M2 M6
t4
M4
Fig. 2.2 Mapping from a SystemC structure to corresponding graph model. a Interconnection of
modules. b Graph model of the module interconnections
without incoming arcs are initial places which start a transition. The places without
outgoing arcs are target places. A transaction data token flows from the initial places
to the target places and token values may change in transitions when necessary. The
internal logic of a transition determines the flow of the transaction. It is a piece of
code which can be modeled by an FSM model.
In TLM, the content of a transaction data token indicates the transaction flow and the
output of each component. Generally, a transaction token consists of several attributes
of different types. Because data type determines the size of the specified variable
which in turn affects the model checking performance, it is necessary to figure out
the data type of a token. Besides all native C++ types, SystemC defines a set of data
type classes within the namespace sc_dt to represent values with application-specific
word lengths applicable to digital hardware. SMV also supports various data types
such as array, Boolean, integer, struct, and so on. Such data type definitions facilitate
the mapping of data types between SystemC TLM and SMV specification. During
the transformation, the word lengths of user-defined type need to be considered.
Figure 2.3 shows an example of the router packet in the form of SystemC TLM and
SMV respectively. For example, sc_uint < 2 > has 2 bits and will be transformed
into a range 03 in SMV.
Derived from the base class sc_module, TLM modules are the main processing
units for the transaction data. Generally each sc_module contains the definitions of
processes whose types are SC_M E T H O D or SC_T H R E AD. Modules commu-
nicate with each other by sending and receiving transaction data tokens via output
and input ports. SystemC provides a communication wrapper for the system compo-
nents (modules). Various binding mechanisms exist in SystemC (e.g., port to export
binding, export to export binding, and port to channel binding) to establish inter-
connection between modules. Usually each binding corresponds to a channel (e.g.,
a FIFO channel) to temporarily hold transaction tokens.
26 2 Modeling and Specification of SoC Designs
Figure 2.4 shows the TLM module structure of a router. The class sc_ex por t
can be used as a port to communicate with other modules. Because the interface
type of port packet_in is tlm_ put_i f < packet>, it is an input port. In contrast,
packet_out x (x = 0, 1, 2) have the interface tlm_ f i f o_get_i f < packet>, so they
are output ports. During the router communication, each connection between a port
and an export uses a FIFO channel to temporarily hold a packet.
Structurally similar to SystemC TLMs, SMV specification is also modularized
and hierarchically organized. So the extraction of structure information needs to map
the TLM constructs in the right place of the SMV specification. Figure 2.5 shows
the SMV module skeleton corresponding to example in Fig. 2.4 after the structure
extraction. In SMV, a module uses the parameters as the input and output ports to
both communicate with other modules and configure the system status defined in
the main module. In the example of Fig. 2.5, the SMV module has one input port
and three output ports. The type of the input and output ports is packet. All the
declarations of member variables except for the FIFO channels are declared in the
SMV specification. Because a FIFO channel together with its port pairs are abstracted
as an SMV parameter, it is not necessary to create a variable in SMV explicitly. Based
on context during the elaboration, some of the declared variables will be initialized.
In SMV specification, each output ports and local variables need to be initialized.
For example, packet_out0 is a parameter which refers to an output port, so it will be
initialized with a value 0. During the translation, it is required that all such module
connections should be defined in the module sc_top.
TLM behavior describes the run-time information of TLM including transaction cre-
ation, transaction manipulation, and module communication. Transaction creation
initializes a transaction by creating a data token (i.e., a C++ object) with proper
2.3 Specification Using SystemC TLMs 27
values. Transaction execution describes the transaction flow among the modules. A
module is a container which has a cluster of relevant processes. Such processes will
handle the incoming transaction tokens and decide where to send them according
to the specified conditions. Thus, a different value of a token will lead to different
transaction flows. The following two types of process communication are widely
supported in transaction flows: (1) direct procedure call from one process to another
process, and (2) channel-based events triggered by the procedure call. For example,
in the blocking mode, a process can fetch a transaction data token from the specified
input port only when the corresponding channel is not empty. Otherwise, the opera-
tion get will be blocked until there is an event triggered by the put operation by
other processes.
Figure 2.6 shows the module process r oute of the router example. The process
receives a packet from the driver via channel input_, and then it decides where to
send data based on the packet header information to_chan.
TLM modeling provides some synchronization mechanism for the communica-
tions between modules. As shown in Fig. 2.6, the router can fetch the data from the
28 2 Modeling and Specification of SoC Designs
FIFO queue input_ only when the driver puts a package and the FIFO channel event
ok_to_get is triggered. Thus the synchronization between two modules is implicitly
achieved.
SMV supports many constructs similar to the common programming language
such as ifthen-else, switch-case and for loop. So these constructs facilitate the
behavior modeling of processes from TLMs to SMV specifications. Figure 2.7
shows the translated SMV specification of the TLM example presented in Fig. 2.6.
During the translation from TLM into SMV, a channel is abstracted as an implicit
buffer between two ports. So an SMV module will get the input data from its input
ports. There is no mapping of the channel in the transformed SMV specification. For
example, the tmp_ packet is assigned the value of the packet_in instead of the value
of input_ shown in the TLM example in Fig. 2.6.
Router Slave 0
get_data
FIFO
Master Slave 1
route
put_data get_data
FIFO FIFO
Slave 2
FIFO get_data
At the beginning of a transaction, the master module creates a packet. Then, the
driver sends the packet to the router for package distribution. The router has one input
port and three output ports. Each port is connected to a FIFO buffer (channel) which
temporarily stores packets. The router has one process r oute which is implemented
as an SC_M E T H O D. The r oute first collects a packet from the channel connected
to the driver, decodes the header of the packet to get the target address of a slave,
and then sends the packet to the channel connected to the target slave. Finally, the
slave modules read the packets when data are available in the respective FIFOs. The
transaction data (i.e. packet) flows from the master to its target slave via the router.
The flow is controlled by the address to_chan in the packet header. By using the
proposed approach in Sect. 2.3.2, the automatically generated SMV model contains
four modules and 145 lines of code.
...
Decision/Merge Fork Join
In this section, UML 2.1.2 [26] is used as the SoC specification. To reduce the
complexity of the testing work, we restrict the testing target and investigate a subset
of activity diagrams. The subset mainly contains action nodes, control nodes, object
nodes, and control and data flow. Especially for the object node, we assume that it
can hold at most one object at a time and it does not support competition and data
store.
UML activity diagram is used to coordinate the execution of actions. An action takes
a set of inputs and converts them into corresponding outputs. An activity (behavior)
consists of a set of actions and flow edges. The actions are connected by object flow
edges to show how object tokens flow through and connected by control flow edges
to indicate the execution order.
UML activity diagrams adopt the semantics like Petri-net [27]. It is a type of
directed graphical representation. Tokens which indicate control or data values flow
along the edges from the source node to the sink nodes driven by the actions and
conditions. An activity diagram has two kinds of modeling elements: activity nodes
and activity edges. More specially, there are three kinds of nodes in activity diagrams:
Action Node. Action nodes consume all input data/control tokens when they are
ready; generate new tokens; and send them to output activity edges.
Object Node. Object nodes provide and accept data tokens, and may act as buffers,
collecting data tokens as they wait to move downstream.
Control Node. Control nodes route tokens through the graph. The control nodes
include constructs to choose between alternative flows (decision/ merge), to split
or merge the flow for concurrent processing ( fork/ join).
2.4 Specification Using UML Activity Diagrams 31
Figure 2.9 shows the basic constructs of activity nodes. An action node is denoted
by a round cornered box. It represents an execution of operations on input tokens,
and the generated new tokens will be delivered to outgoing edges. An object node
denoted by a rectangle box is used to temporarily hold the data tokens waiting to be
processed or delivered. For simplicity, it is assumed that object nodes do not support
competition and data store for test case generation. A flow in an activity starts from
the initial node. When a token arrives at a flow final node, it will be destroyed. The
flow final node has no outgoing edges, so there is no downstream effect. When no
tokens exist in an activity diagram, the activity will be terminated. The activity final
nodes are similar to flow final nodes, except that when a token reaches one activity
final node, the entire flow will be terminated. Decision nodes and merge nodes use the
same shape of diamond. Decision nodes choose one of the outgoing flows according
to the value of Boolean expressions labeled on the outgoing edge. Merge nodes select
only one of the incoming flows to deliver to the next activity node. Forks or joins are
shown by multiple arrows leaving or entering the synchronization bar, respectively,
to describe the concurrent behavior of a system. When a token arrives at a fork node,
it will be duplicated across the outgoing edges. Join nodes synchronize multiple
flows. The tokens must be available on every incoming edge in order to be passed to
outgoing edges.
Activity nodes are connected by activity edges along which tokens may flow under
some condition. Activity edges include control and data flow edges as follows:
Control Flow Edge. Control flow edges indicate the execution sequence of actions.
Object Flow Edge. Object flow edges indicate the relation of data token transmis-
sions. It provides the inputs to actions.
To simplify the discussion, we combine the control and data token together as a
new kind of token which contains both control and data information. Such token can
flow through activity edges. In other words, we do not distinguish control flow edges
and object flow edges.
Figure 2.10 shows an example which uses most of the elements shown in
Fig. 2.9. It describes the functionality of withdrawing money from an automated
teller machine ( ATM) [28]. A user needs to enter the access code first. In case of
failure, the user can input the access code again. The operation will abort if access
code is wrong in both cases. If the input access code is right, the user can enter the
amount of money he wants to withdraw. At the same time, the printer will be ready
to print a receipt. Once the ATM decides whether there is enough money the user
can withdraw, it provides the cash and generates the information for this transaction.
Finally, the printer prints the receipt and the transaction is complete.
The token for this example contains the ATM transaction information such as
the input access code and input cash amount, the context information such as the
available cash amount and correct access code. In general, a token reflects all the data
information required for this activity. Table 2.1 shows the composition of a token of
the ATM activity diagram. It consists of five variables which will be used to make
the decisions illustrated in Table 2.2.
32 2 Modeling and Specification of SoC Designs
start
t1
t7 [amount available]
f Prepare to
Dispense cash d print receipt
t9
Generate receipt
content e
syn_2 t10
g Finish transaction
and print receipt
t11
end
Without formalism, it is hard to describe and model the activity diagrams accurately.
UML activity diagram itself is a semi-formal specification that cannot be directly
mapped to a model checker input (e.g., SMV models). In practice, Petri-net is used as
an intermediate formal model between activity diagrams and SMV model, because
2.4 Specification Using UML Activity Diagrams 33
the Petri-net formalism can capture the major functional scenarios as well as guide
the translation.
Definition 2.4 describes the relation between the activity nodes and flow edges
with a Petri-net semantics. Although it does not model the full features of activity
diagrams, it formally depicts the static abstracted structure of activity diagrams which
can be used to describe the scenarios that need to be tested.
Definition 2.4 An activity diagram is a directed graph described using an eight-tuple
(A, T, F, C, V, A, a I , a F ) where
A = {a1 , a2 , . . . , am } is a set of action nodes.
T = {t1 , t2 , . . . , tn } is a set of completion transitions.
F {AT }{T A} is a set of flow edges between activity nodes and completion
transitions.
C = {c1 , c2 , . . . , cn } is a finite set of guard conditions. Here, ci (1 i n) is
a predicate (expression) based on the input variables. There is a mapping from
f i F to ci , referred as Cond( f i ) = ci .
Let V be the set of all possible assignments for input variables V1 , V2 , . . . , Vk
where k is a positive integer.
M : AV V is a mapping that describes the value change of the input variables
inside an activity node.
a I A is the initial node, and a F A is the final node. There is only one
completion transition t T and c C such that (a I , t) F, and for any t T ,
(t , a I )
/ F and (a F , t )
/ F.
34 2 Modeling and Specification of SoC Designs
A node can be an action node, an initial node or a final node. The completion
transition and flow edge are used to model the behavior of the control nodes. In
the graph, the nodes are connected by flow edges associated with a completion
transition. Because activity diagrams allow tokens to exist in the flows concurrently,
the completion transition can be used to synchronize the token flows. If a completion
transition has multiple incoming flow edges, it will do the join operation. If there
are multiple outgoing flow edges, then it will do the fork operation. For each flow,
e.g., there may be a condition which can guide the token traverse. The graph has one
initial node that indicates the start of control and data flows. Activity diagrams have
two kinds of final nodes: flow final nodes and activity final nodes. We can combine
them together and use a join operation to get a new activity final node. So in the
definition there is only one final node.
When analyzing dynamic behaviors of an activity diagram, we need to use the
states (a set of actions executing concurrently) to model the status of a system.
Current state (denoted by C S) of an activity diagram indicates the actions which are
being activated.
Definition 2.5 Let D be an activity diagram. The current state C S of D is a subset
of A. For any transition t T ,
t denotes the preset of t, then t = { a | (a, t) F}.
t denotes the postset of t, then t = {a | (t, a) F}.
enabled(C S) denotes the set of completion transitions that are associated with
the outgoing flow edges of C S, then enabled(C S) = { t | t C S }.
firable(CS) denotes the set of transitions that can be fired from C S, then
firable(CS)={ t | t enabled(CS) t are all completed n A. Cond((t, n))
is satisfied (C S t) t = }. After some t is fired, the new current state
C S = f ir e(C S, t) = (C S t) t .
The current state of an activity diagram indicates which activity nodes are holding
the tokens. For example, when {d, f } is the current state of the activity diagram in
Fig. 2.10, two tokens are in the activity nodes d and f individually. At this time, only
the transition associated with t9 is firable. If it is fired, then the next state is {e, f }.
Because of the inherent concurrency, several transitions can be fired at the
same time. For an activity diagram, all the firable transitions in a state form a
concurr ent transition.
Definition 2.6 Let D be an activity diagram. For a state C S of D, a concurrent
transition is a set of completion transitions t1 , t2 , ..., tn f irable(C S) where
1. i, j (1 i < j n), ti t j = ;
2. t (enabled(C S) {t1 , t2 , . . . , tn }), there exists an i (1 i n) such that
t t = .
i
n
After firing from nstate C S, the current state C S = f ir e(C S, ) =
i=1
( f ir e(C S, ti )) =
i=1 ((C S ti ) ti ).
2.4 Specification Using UML Activity Diagrams 35
The dummy node is inserted here because it assumes that outgoing edges of the
fork node must connect to an activity rather than a selection node. For a key path,
when firing transitions, we need to consider guard conditions. For clarity, in Fig.
2.10, we did not label the condition guards for each transition.
Definition 2.8 Let D be an activity diagram. An interaction of the activity diagram is
a set of activity nodes (actions) that can be activated simultaneously. A k-interaction
is a set that contains k activity nodes.
In order to detect whether a concurrent state of an activity diagram is reachable
or can be activated, we use the term interaction1 to describe the scenario that a set
of actions can be activated simultaneously. For example, in Fig. 2.10, {d, f } is an
example of 2-interaction in the ATM.
1 Unlike the interaction in UML Interaction overview diagram, the interaction here means that
several actions are activated at the same time.
36 2 Modeling and Specification of SoC Designs
By parsing a UML activity diagram, both the control and data flows can be extracted.
The translation consists of two parts: static information extraction and dynamic
information extraction. Static information extraction analyzes the structure of an
activity diagram and then generates a skeleton of the SMV input. The dynamic
information extraction analyzes the dynamic behavior of the system by focusing on
control and data flow analysis (i.e., the state change of activities, data manipulation
in activities and the condition of the transitions).
This step collects both the input data manipulated by the activities and the pred-
icates used as guard conditions of the transitions. For example in Fig. 2.10,
there are five input data variables that determine the data and control flows:
access_code, access_code_input, access_code_r esolve, amount_input, and
amount_available. Since there may be a large number of possible values for a vari-
able, during model checking it will cause the state space explosion. SMV does not
support complex data types (e.g., float, double, etc.). For each variable, it is required
that the value range should be specified explicitly. To avoid state space explosion,
the following methods can be used to reduce the complexity of data types:
Scaling. Scaling is to proportionally reduce the value range of a variable.
Reduction. Reduction is to reduce the cardinality of possible values for a variable.
Since it is hard to implement the above techniques automatically, before the SMV
translation, the variable type information is tuned manually for activity diagrams.
During translation, each activity is assigned with a state variable which has three
possible state values: unvisited (0), unvisited (1) and visited (2). visited indicates that
no token has passed through this activity node. Visiting indicates currently the activity
is holding one or more tokens. visited indicates that some token has passed through
this activity node and currently there is no token in this activity node. The extraction
procedure instantiates the activity state variables and assigns suitable values to them.
During initialization, the initial activity node is assigned unvisited that means there is
a token ready at the initial state. Other nodes are initialized to unvisited. Also, each
flow edge is assigned with a state variable which has two possible values: f ir ed (1)
and un f ir ed (0). Fir ed means some tokens have flowed from the incoming activity
nodes to its outgoing activity nodes. U n f ir ed means no token has passed through
this activity edge. Initially, they are set with value 0.
Figure 2.11 shows the generated skeleton of Fig. 2.10 in SMV format [18, 23].
There are three modules in this skeleton. The module state defines the token infor-
mation (described in Table 2.1) as well as the state variable for activity nodes and
flow edges. For example, veri f y_access_code is a state variable for an action with
three states. Initially it is assigned the state unvisited (0). Module AT M shows a
2.4 Specification Using UML Activity Diagrams 37
static skeleton without dynamic behavior information. In this phase, variables are col-
lected without any processing. The missing state transition details will be described
in Sect. 2.4.3.2. The module main creates the module instances and elaborates them
together. For example, st is an instance of state module and atm is an instance of
ATM module. Both the st and atm are bound together, because atm will handle the
state changes of variables in st.
After static information extraction, it needs to extract both data manipulations and
transitions of state variables, because they will determine the data and control flows.
Figure 2.12 defines a set of rules that specify the state transition for each activity node
and the value changes of each data. In these rules, the preset and postset notations
are used. In these rules, the assignment and constraint to a set means the assignment
and constraint to each element in the set. For example, if t = {a1 , a2 , . . . ak },
38 2 Modeling and Specification of SoC Designs
StockBroker
t0 t1
VerigyOrderForm addOrderFormList
t2 t3
getNewOrder
DisplayOrderErrorInfo
t7
t4
checkLimitOrderPrice
t5 t6
tradeMarkderOrderSale tradeMarketOrderBuy
t8 t9
t11 t12
tradeLimitOrderSale tradeLimitOrderBuy
t13 t14
t16
t17
t15
getOrderResult
t18
trade_FAILURE
t23 t19
updateOrderDB_FAILURE
t28
trade_SUCESS
t20
updateStockDB_SUCESS
trade_NOMATCH updateOrderDB
updateOrderDB_SUCESS
t29
trade_PARTEXE
updateStrockDB_PARTEXE t27
t26 t21
updateOrderHashMap
updateStockHolderDB_PARTEXE
updateOrderDB_PARTEXE
to the join node can be fired. In this rule, if we want to fire the transition, it needs
to wait until all the activity nodes in the preset of the transition are visited. Rule 6
shows how to manipulate the state change of the transition when it is fired. Rule
7 presents the translation for value change of the variables. If an activity performs
some operation on the variable, the value of the variable can be modified only when
the activity state is unvisited.
References
1. Rose A, Swan S, Pierce J, Fernandez J (2005) Transaction level modeling in SystemC. Open
SystemC Initiative. http://www.systemc.org
2. Object Management Group (2006) UML profile for system on a chip (SoC), v 1.0.1. http://
www.omg.org/technology/documents/formal/profile_soc.htm
References 41
3. Riccobene E, Scandurra P, Rosti A, Bocchio S (2005) A UML 2.0 profile for systemc: toward
high-level soc design. In: Proceedings of ACM international conference on embedded software,
pp 38141
4. Chureau A, Savaria Y, Aboulhamid EM (2005) The role of model-level transactors and UML
in functional prototyping of systems-on-chip: a software-radio application. In: Proceedings of
design automation and test in Europe (DATE), pp 698703
5. Mueller W, Rosti A, Bocchio S, Riccobene E, Scandurra P, Dehaene W, Vanderperren Y (2006)
UML for ESL design: basic principles, tools, and applications. In: Proceedings of international
conference on computer-aided design (ICCAD), pp 7380
6. Ammann P, Black P, Majurski W (1998) Using model checking to generate tests from specifi-
cations. In: Proceedings of international conference on formal engineering methods (ICFEM),
pp 4654
7. Mishra P, Dutt N (2008) Processor description languages. Morgan Kaufmann Publishers, San
Francisco
8. Hennessy J, Patterson D (2003) Computer architecture: a quantitative approach. Morgan Kauf-
mann Publishers, San Francisco
9. Hopcroft JE, Motwani R, Ullman FD (2006) Introduction to automata theory, language, and
computation 3rd edn. Addison-Wesley
10. Open SystemC Initiative (OSCI) (2006) Systemc. http://www.systemc.org
11. Cai L, Gajski D (2003) Transaction level modeling: an overview. In: Proceedings of inter-
national conference on hardware/software codesign and system, synthesis (CODES+ISSS),
pp 1924
12. Ghenassia F (2005) Transaction level modeling with systemC. Springer, Dordrecht
13. Abdi S, Gajski D (2005) A formalism for functionality preserving system level transforma-
tions. In: Proceedings of Asia and South Pacific design automation conference (ASPDAC),
pp 139144
14. Kroening D, Sharygina N (2005) Formal verification of systemc by automatic hard-
ware/software partitioning. In: Proceedings of international conference on formal methods
and models for co-design (MEMOCODE), pp 101110
15. Moy M, Maraninchi F, Maillet-Contoz L (2005) Lussy: A toolbox for the analysis of systems-
on-a-chip at the transactional level. In: Proceedings of the international conference on appli-
cation of concurrency to system design, pp 2635
16. Karlsson D, Eles P, Peng Z (2006) Formal verification of systemc designs using a petri-net
based representation. In: Proceedings of design, automation, and test in Europe (DATE),
pp 12281233
17. Habibi A, Tahar S (2006) Design and verification of systemC transaction-level models. IEEE
Trans Very Large Scale Integr Syst (TVLSI) 14(1):5768
18. McMillan KL (OSCI) (2006) SMV model checker. http://www.kenmcmil.com/
19. Unhelkar B (2005) Verification and Validation for Quality of UML 2.0 Models. Wiley, New
York
20. Chen M, Qiu X, Li X (2006) Automatic test case generation for uml activity diagrams. In:
Proceedings of international workshop on automation on software test, pp 28
21. Chen M, Qiu X, Xu W, Wang L, Zhao J, Li X (2009) UML activity diagram based automatic
test case generation for java programs. Comput J 52(5):545556
22. Eshuis R (2006) Symbolic model checking of UML activity diagrams. ACM Trans on Softw
Eng Methodol 15(1):138
23. Cimatti A, Clarke EM, Giunchiglia F, Roveri M (1999) NUSMV: A new symbolic model
verifier. In: Proceedings of international conference on computer aided verification (CAV), pp
495499
24. Guelfi N, Mammar A (2005) NUSMV: A formal semantics of timed activity diagrams and
its Promela translation. In: Proceedings of Asia-Pacific software engineering conference
(APSEC), pp 283290
25. Das D, Kumar R, Chakrabarti PP (2006) Timing verification of UML activity diagram based
code block level models for real time multiprocessor system-on-chip applications. In: Proceed-
ings of Asia-Pacific software engineering conference (APSEC), pp 199208
42 2 Modeling and Specification of SoC Designs