We refined channels to be point to point between two behaviors, and will have double handshake semantics. These behaviors must be either hierarchical behaviors or identity behaviors. The channel will also no longer hold addresses, and any data to be transferred will be read by the identity behavior on one side and written out by the identity behavior on the other side. It is best illustrated in Figure 9.

3.2 Principle of Duplication

When designing embedded systems, the designers may encounter modules that slow down the execution flow because of their slow hardware response. In Figure 10 a), let’s say that module B is the one with a big delay. One of the common solutions would be to simply duplicate the module in question (hardware IP for instance) and do a parallel execution to speed the execution, as shown in b). Module A will forward half of its computation to module B’ and half to B”, assuming that both modules perform identical computation tasks. Finally, our system is shown in c), with 2 modules B’ and B” in an endless loop, performing calculations for A and forwarding the result to C.

3.3 Behavior Type

The principle of duplication shown in the previous section is sound if and only if the two behaviors running in parallel are identical. In order to include this property into Model Algebra, we introduce Behavior Type: each behavior will have a type, and may be shown explicitly after the behavior name, separated by a colon. Figure 11 updates the figures in c) (from Figure 10) with the behavior type and with the proper Model Algebra objects.

For two behaviors to be of the same type, there is one underlying condition: both behaviors have to have the same ports and these ports have to have the same bindings to other ports or variables. If this is not met, the two behaviors shall be considered of different type.

3.4 Behavior Merging

This transformation merges two behaviors if the following conditions are met:

• Both behaviors are of the same type. This implies that both behaviors have the same bindings to the same ports and/or variables.
• Their sets of successor behaviors are equal. In other words, the execution of any of the two behaviors is followed immediately by the execution of one specific behavior.

3.5 Control Node Merging

This transformation rule allows to reduce the number of control nodes by merging two or more nodes if:

• Their sets of predecessor behaviors are equal.
• They have the same successor behavior.

4. Model Algebra Data Structure

In order to be able to properly manipulate and transform a model described in Model Algebra, we need a suitable data structure to describe any posible model. We now describe the Model Algebra Data Structure used in our tool. Our Model Algebra Data Structure is saved in the XML format [4] and have the extension .MAG. The set of rules that all MAG files conform to is expressed in a XML Schema Definition (XSD) [5]. MAG files are composed of the following elements: BEHAVIOR, VARIABLE, CONDITION, CHANNEL, LINK, PORT, CD, DD_VAR_NB_READ, DD_VAR_NB_WRITE, DD_PORT_NB_READ, DD_PORT_NB_WRITE, DD_PORT_B_READ, and DD_PORT_B_WRITE.

The root of every MAG file is a BEHAVIOR object which contains any other objects listed above. The BEHAVIOR object is hierarchical, meaning that any object can only be contained inside a BEHAVIOR object and no other.

The graphical representation of the MAG object tree is shown in Figure 14. In this figure, we can see that the only other object that can be hierarchical is CHANNEL, which contains LINK. It describes the ports that connect both behaviors to the channel. CD refers to Control Dependency, and has an attribute pointing to CONDITION. This object marks if the CD depends on a variable, port or a boolean value. All the data dependency objects are represented in the figure as DD: these include data dependencies on variables and ports, blockingand nonblocking reads and write operations.

5. TLM Verifier

We developed a tool to create, transform and verify TLMs, named TLMVer. It is composed of:

• Input API: it is the interface for the MA converter which creates a Model Algebra data structure. It creates all the MA objects and dependencies between them.
• Frontend GUI: shows the graphical representation of the MAG file. It has an interface to allow the user to apply any transformation in any order to the model. It also checks for isomorphism between two models.
• Backend: it responds to the GUI and applies all the transformation rules, and performs the equivalency checks.

In Figure 15, we show the verification flow using TLMVer. We would start with an application and goes through several refinement steps. Both applications’ TLMs are fed into the MA Converter, which interfaces with our TLMVer API. This creates the MA representation (MAG file) that is the input for the TLMVer. Finally, the transformations are performed in this step by the tool and a isomorphism is checked at the end. If both models are isomorphic, we can say that both models are equivalent.

The MA Converter’s task is to parse the TLM and make the appropiate calls to the Input API. This module has not yet been developed, and the models we use are created by a script calling the API.

5.1 Isomorphism Checker

Our tool can take two models’ MA representation and check if both graphs are isomorphic. Isomorphism indicates syntactic equality of 2 models and it is the strongest possible equivalence. MA representations have a root node which will be the Virtual Starting Point (VSP). They may or may not have a connected Virtual Terminating Point (VTP), and commonly has cyclic edges.

One assumption that makes the checker very simple is the case in which a model M1 and a model M2, both share the same set of subbehaviors with the same name. In this case, the checker algorithm is shown in Algorithm 1. The checker’s task is to mainly verify the data dependencies between each behavior and the variables, and to verify the dominance of each behavior to all other behaviors (line 10). If all dominance checks are true, and the data dependencies are equal, both models are isomorphic.

For each variable/behavior pair, a check operation is done to see if there exists a data dependency in which the behavior reads or writes to that variable (line 22). The function checkOperation is shown in Algorithm 2.

6. System Level Refinement and Verification Experimental setup

The design methodology for our system is shown in Figure 16. It starts with an executable functional specification model of the design and is gradually refined into a cycle accurate model which is then forwarded into the traditional manufacturing phase. The refinement process is composed of several steps in which objects in our models are modified, replaced or eliminated. After each step, the designer ends up with a new executable model which serves as the base for the next refinement step. As shown in Figure 16, cycle accurate design is not part of our domain and will not be discussed here.

The refinement depicted in Figure 16 are:

• Behavior Partitioning: the behaviors are rearranged to reflect the mapping of leaf behaviors to component behaviors.
• Serializing: Behaviors that must be executed with a single controller are serialized, it converts parallel composition into sequential compositions.
• Communication Scheduling: by modifying the scheduling of bus transactions, the performance of the design can be improved.
• Transaction Routing: Splits transaction links into two links putting a router in between.
• These key refinements were described in detail in [3]. In this article, we will focus on the design optimizations depicted in Figure 17. These optimizations can be proven for correctness using the new transformation rules of Model Algebra.

The optimization depicted are:

• Pipelining: sequential behaviors are separated into different processing units which run concurrently. Each behavior will forward data to the next one and immediately begin processing the next data packet. Between each pair of behaviors a FIFO structure may be modeled.
• Duplication: slow behaviors may be duplicated in order to compute two or more data packets simultaneously and speed up the pipeline.

6.1 FIFO modeling

To model communication between behaviors, we can use communication channels, described above. But for several types of applications, the model of computation used is Kahn Process Networks, were the behaviors execute concurrently and communicate through unbounded FIFOs. Our model of a FIFO can have one or more storage variables. Shown in Figure 18 is a 1-place FIFO. The structure is based on two identity behaviors: e1 and e2. The first one performs the double handshake channel communication with the preceding behavior and writes out the data into the variable. The second identity behavior reads the variable and pass it through the channel to the next behavior.

Results of FIFO Transformation

We can use the transformation rules described in this article to prove that a n-place FIFO can be reduced to a 1-place FIFO. This is illustrated in Figure 20. The initial model is a subsection of a n-place FIFO depicting a 2-place FIFO, shown in the upper left corner of the figure. There is a incoming channel ch1 and an outgoing channel ch3. The outgoing channel links with the rest of the FIFO. The first transformation rule applied is the Channel Resolution Rule, so channel ch2 is resolved into two new control dependencies: identity behavior e3 goes to e1 and e2 goes to e4. The Identity behavior e2 now writes directly to variable v2. The result is shown in the upper right model in Figure 20. The next rule applied is Identity Elimination: e2 is eliminated and the variables v1 and v2 are merged, keeping the name v1. The other rule that was applied is the Redundant Control Dependency Elimination: the control dependency between vsp and e1 is eliminated. The result is shown in the lower right model in Figure 20. The last step is to apply again the Identity Elimination Rule to behavior e3. The resulting model is shown in the lower left part of the figure and it is the same as a 1-place FIFO, proving that any FIFO can be reduced into a 1-place FIFO applying the basic transformation rules of MA.

Taking several FIFOs with different sizes, we utilized our verification tool to measure the transformation times. We built FIFOs with sizes 1,2,3,4,5 and 10 places and applied the transformation rules. The results are shown in Figure 21. We can see that, as expected, the total transformation time increases with the size of the FIFO, but still in the order of seconds.

6.2 Pipeline Modeling

Pipelined architectures are a common optimization for systems with certain types of applications. In a pipeline, data is transferred from one processing module to the next, while all modules run in parallel. This increases dramatically the throughput of the data packets, but the overall time to process one individual packet remains the same. It has been commonly used in microprocessor architecture.

Design decisions

To create an optimum pipeline, the designer must adequately partition the behaviors into different stages. The pipeline throughput depends directly on the slowest module, so the optimum balance in terms of behavior speed must be achieved while partitioning. The pipeline optimization is illustrated in Figure 22. In this figure, we start with 4 sequential behaviors labeled ’B1’, ’B2’, ’B3’ and ’B4’. Their estimated delay times are 5, 10, 20 and 20. The overall delay for each packet would be 55 time units. The optimum way to create the pipeline would be to use 3 pipeline stages, with behaviors ’B1’ and ’B2’ together in the first stage. This way, data packets would be processed every 20 time units.

A simple 3 stage pipeline model is shown in Figure 23. We use channels to communicate the data between behaviors A, B and C.

Verification results

In Figure 24 we can see the transformation steps to this 3 stage pipelined architecture. Starting in the upper left corner, we can see the model after applying the Flattening rule to the behaviors shown in Figure 23. The next step is to apply the Channel Resolution rule, converting channels ch1 and ch2 into control dependencies. The resulting model is shown in the upper right part of the figure. We can see now that behaviors e2 and e4 write directly to variables v2 and v3, and both now execute behaviors e1 and e3 afterwards. Next, the Redundant Control Dependency Elimination rule is applied and the control dependencies between vsp and e1 and e3 are deleted. This is shown in the lower right part of the figure. The last step is to apply the Identity Elimination rule to behaviors e1, e2, e3 and e4. We can see that the model shown in the lower left part of the figure is the representation of a serialized model with behaviors A, B and C executing one after another, using the data written by the previous stage.

In order to test our transformation rules, we modeled a JPEG Encoder using Model Algebra’s representation. The JPEG encoder is composed of 5 main functions, as shown in Figure 25. They are named: ReadBmp, DCT, Quantize, Zigzag and Huff. They run sequentially in a loop for 180 times, taking a .bmp file as the input and writing out a .jpeg file. Each function can be mapped into a single core or with another function. We created 4 different models, all pipelined, with different number of stages. All were synthesized and implemented into a Xilinx Virtex 4 FPGA board. The mappings for each of the platforms is shown in Figure 26. Each platform is composed of 2 or more MicroBlaze softcore embedded processors, one shared bus (OPB protocol) and one transducer serving as a shared memory. The MicroBlazes will exchange data by storing it in the transducer internal FIFO and reading it out from there.

As shown in Figure 27, the execution time decreases as we increase the number of pipeline stages.

In order to check for equivalence of these different models, we created Model Algebra representations of all 4 and applied the transformations, and checked for isomorphism with the non-pipelined model. The transformation time for these 4 models is shown in Figure 28, and the number and type of transformation rules applied is shown in Figure 29.

As we can see in Figure 28, the transformation time for each of the platforms is in the order of seconds, and scales linearly. In Figure 29, we can observe that the number of transformations also increases linearly with the number of stages, and all transformation rules applied increase with it.

7. Conclusions

In this article we presented a summary of the system level verification challenges and the Model Algebra formalism. We described new transformation rules for Model Algebra: channel resolution, control node merging and behavior merging. Building upon these new transformation rules, we presented useful system level optimizations, namely pipelining, use of FIFO channels and behavior duplication.

We showed how we could model a N-place FIFO and a pipeline, and used Model Algebra’s transformation rules to prove their correctness.

We defined a data structure to describe models written in Model Algebra, named MAG files. This data structure allowed the description, graphical representation and storage of intermediate and final structures of these models in MA.

Using Model Algebra’s composition and transformation rules, we developed a software tool that can take models written in MA (as MAG files), represent them graphically and see transformation rules applied to them. By modeling a multimedia application such as a JPEG encoder into a pipelined architecture, we could prove that Model Algebra’s representation of these optimizations on these platforms could be successfully transformed and compared with the non pipelined model. The transformation time was fast (in the order of seconds) and the number of transformation rules increased linearly with the number of pipeline stages.

The implementation of the software tool gives us more confidence in refinement results, more ability to explore different sequences of transformations and the means to develop correct refinement and optimization tools.

8. Recommendations and future work

There is need to develop more transformation rules in order to check for isomorphism in more dissimilar models. As the number of transformation rule increases, the verifier tool will be more versatile and more complex designs will be formally verifiable. This will reduce the design and verification time, improving time-to-market parameters and increasing productivity.

References

Samar Abdi and Daniel Gajski. Verification of system level model transformations. Internation Journal of Parallel Programming, 34(1):29-59, February 2006

Samar Abdi and Daniel Gajski. A formalism for functionality system level transformations. In Proceedings of the Asia Pacific Design Automation Conference, pages 139-144, 2005

Samar Abdi. Functional Verification of System Level Model Refinements. PhD Thesis, University of California, Irvine, 2005.