Karsten Albers

Frank Slomka

Efficient Feasibility Analysis for Real-Time Systems with EDF scheduling*

This paper presents new fast exact feasibility tests for uniprocessor real-time systems using preemptive EDF scheduling. Task sets which are accepted by previously described sufficient tests will be evaluated in nearly the same time as with the old tests by the new algorithms. Many task sets are not accepted by the earlier tests despite them beeing feasible. These task sets will be evaluated by the new algorithms a lot faster than with known exact feasibility tests. Therefore it is possible to use them for many applications for which only sufficient test are suitable. Additionally this paper shows that the best previous known sufficient test, the best known feasibility bound and the best known approximation algorithm can be derived from these new tests. In result this leads to an integrated schedulability theory for EDF.

Introduction

The analysis of the time behavior of embedded real-time systems is essential for the automation of the design process. A formal verification which guarantees all deadlines in a real-time system would be the best. This verification is called feasibility test. Three different kinds of tests are available: • Exact tests with long execution times or simple models [START_REF] Baruah | Generalized Multiframe Tasks[END_REF], [START_REF] Baruah | Preemptive Scheduling Hard-Real-Time Sporadic Tasks on One Processor[END_REF], [START_REF] Gresser | Echtzeitnachweis Ereignisgesteuerter Realzeitsysteme[END_REF]. • Fast sufficient tests which fails to accept feasible task sets, especially those with high utilizations [START_REF] Devi | An Improved Schedulability Test for Uniprocessor Periodic Task Systems[END_REF], [START_REF] Liu | Scheduling Algorithms for Multiprogramming in Hard Real-Time Environments[END_REF]. • Approximations, which are allowing an adjustment of performance and acceptance rate [START_REF] Albers | An Event Stream Driven Approximation for the Analysis of Real-Time Systems[END_REF], [START_REF] Chakraborty | Approximate Schedulability Analysis[END_REF]. For many applications an exact test or an approximation with a high acceptance rate must be used. For many task sets a fast sufficient test is adequate. This paper proposes two new tests for preemptive EDF scheduling, which have a performance comparable with the sufficient tests for those tasks sets which can be recognized by these sufficient tests and outperforms the existing exact tests by orders of magnitude. These algorithms are tested and compared using a large amount of randomly generated task sets and some examples from literature. In Section 2 the analysis model is introduced, Section 3 gives an introduction to the existing feasibility tests and the concepts needed further in this paper. It contains the first contribution of this work: the proof of equivalence between the sufficient test given by Devi [START_REF] Devi | An Improved Schedulability Test for Uniprocessor Periodic Task Systems[END_REF] and the superposition approximation described in [START_REF] Albers | An Event Stream Driven Approximation for the Analysis of Real-Time Systems[END_REF]. It is shown that the test by Devi is a special case of the superposition approach. Section 4 presents as the main contribution of the work the new fast sufficient and necessary feasibility tests and also the proof for deriving the feasibility bound out of these tests. In Section 5 the new test algorithms are evaluated followed by a conclusion in Section 6.

Model

We consider the sporadic task system consisting of a set of tasks Γ={τ 1 ,..., τ n }. Each task τ i is described by • an initial release time (or phase) φ i , • a relative deadline D i (measured from the release time), • a worst-case execution time C i and • a minimal distance (or period) T i between two instances of a task. An invocation of a task is called a job, and the k th invocation of each job is denoted τ i,k . In the following only the synchronous case is considered, so the first jobs of all tasks are released simultaneously. This is a common assumption which also leads to a sufficient test for the asynchronous case [START_REF] Stankovic | Deadline Scheduling for Real-Time Systems EDF and Related Algorithms[END_REF]. A good sufficient condition for the asynchronous case is proposed in [START_REF] Pellizzoni | A New Sufficient Feasibility Test for Asynchronous Real-Time Periodic Task Sets[END_REF]. It is based on the tests improved in this paper. The specific utilization of a task is the part of the capacity which is needed for executing this task (

). The utilization U of the system is the sum of the specific utilizations of all tasks. We consider the uniprocessor feasibility test. The scheduling is done using earliest deadline first (EDF) which is known to be optimal [START_REF] Liu | Scheduling Algorithms for Multiprogramming in Hard Real-Time Environments[END_REF]. To keep the explanations in this paper simple the sporadic task model is used. The new tests can be extended to more advanced task models. Especially the extension for the event stream model [START_REF] Gresser | Echtzeitnachweis Ereignisgesteuerter Realzeitsysteme[END_REF] is easy by following the definitions proposed in [START_REF] Albers | An Event Stream Driven Approximation for the Analysis of Real-Time Systems[END_REF].

Background and related work

The feasibility test for uniprocessor systems using EDF with deadlines smaller then the periods of the tasks is

U τ ( ) C τ T ⁄ τ =
known to be Co-NP-hard [START_REF] Baruah | Preemptive Scheduling Hard-Real-Time Sporadic Tasks on One Processor[END_REF]. There are only feasibility tests with pseudo-polynomial complexity available so far. It is unknown whether the problem has polynomial complexity. In the following an introduction to the relevant feasibility tests of the literature is given. An overview is given in [START_REF] Stankovic | Deadline Scheduling for Real-Time Systems EDF and Related Algorithms[END_REF].

Sufficient tests

For a restricted version of the given model with the condition T i = D i for each task τ i , Liu and Layland [START_REF] Liu | Scheduling Algorithms for Multiprogramming in Hard Real-Time Environments[END_REF] proved that the task system is feasible if the utilization .

Test by Devi

Recently Devi [START_REF] Devi | An Improved Schedulability Test for Uniprocessor Periodic Task Systems[END_REF] proposed a test which allows task systems with deadlines smaller than periods with a reduced complexity:

Def. 1: Test Devi [START_REF] Devi | An Improved Schedulability Test for Uniprocessor Periodic Task Systems[END_REF]: A task system Γ, arranged in order of non-decreasing relative deadlines is feasible using EDF scheduling if and Unfortunately this test is only sufficient. It allows a fast evaluation and acceptance of task sets in many cases.

Processor demand test

In [START_REF] Baruah | Preemptive Scheduling Hard-Real-Time Sporadic Tasks on One Processor[END_REF] The test has a pseudo-polynomial complexity if the considered utilization is bound by a constant. The problem is that the runtime of the algorithm depends not only on the utilization but also on the ratio of the different periods and deadlines in the task set [START_REF] Albers | An Event Stream Driven Approximation for the Analysis of Real-Time Systems[END_REF]. If the task set contains tasks with small periods and tasks with large periods, the runtime can become quite large. See the experiments given in Section 5 for more details.

Approximation by superposition

Recently, several approximations have been proposed to solve the complexity problem of the demand bound approach: One by Chakraborty et al. [START_REF] Chakraborty | Approximate Schedulability Analysis[END_REF] and the superposition approach [START_REF] Albers | An Event Stream Driven Approximation for the Analysis of Real-Time Systems[END_REF]. They bridge the gap between the fast but only sufficient test of Devi and the necessary but slow processor demand test. The algorithms are only sufficient, but the degree of sufficiency can be adjusted. The main idea of the superposition approach is to test only a selectable limited amount of test intervals for each task and use an approximation to compensate the remaining test intervals.

Def. 4: Approximated task demand bound function dbf'(I,τ τ τ τ) ) ) ) [1]: An upper bound for the task demand bound function considering only the jobs up to the selectable maximum test interval Im(τ) exactly.

The approximation is using the specific utilization of the task. In the special case of considering only the first job of each task, the maximum test interval is equal to the deadline of the task. The approximated demand bound function is a superposition of the approximated task demand bound functions.

Def. 5: Approximated demand bound function [1] dbf'(I,Γ Γ Γ Γ):

One advantage of this approximation is that it is not necessary to calculate dbf'(I,Γ) for each job separatly. Lemma 1: Super position test: A task system Γ is feasible if dbf'(I,Γ) ≤ I for all Def. 6: SuperPos(x) : The super position test which calculates at the maximum the first x jobs of each task exactly (test level x) is called SuperPos(x) A higher level of the superpostion test leads to a higher acceptance rate but also to a longer execution time of the test. Figure 1 shows measured acceptance rates using different SuperPos(x). The superposition test is a sufficient test with a selectable error. It can be regarded as a series of ------------------------------------ 3) SuperPos(4) SuperPos( 5) SuperPos( 6) SuperPos( 7) SuperPos( 8) SuperPos( 9) SuperPos [START_REF] George | Preemptive and Non-Preemptive Real-Time Uni-Processor Scheduling[END_REF] Processor Demand Utilization (%) percentage task sets feasible

U 1 ≤ n Γ = 1 k n ≤ ≤ ( ) ∀ C i T i ----- i 1 = k ∑ 1 D k ------ T i min T i D i , ( ) - T i -
-     C i ⋅ i 1 = k ∑ ⋅ + 1 ≤       dbf I Γ , ( ) I D i - T i -------------1 + C i ⋅ τ ∀ i Γ I D i ≥ ∧ ∈ ∑ = I max U 1 U - ( ) ⁄ ( ) max T i D i - ( ) { } = 0 0.2
dbf' I τ , ( ) dbf Im τ ( ) τ , ( ) C τ T τ ------I Im τ ( ) - ( ) ⋅ + I Im τ ( ) > dbf I τ , ( ) I Im τ ( ) ≤      = dbf' I Γ , ( ) dbf' I τ , ( ) τ ∀ Γ ∈ ∑ = I I max ≤
sufficient tests, which gets better with declining error.

Superposition vs. Devi

An interesting point is the relationship of the superposition test to the best previously known sufficient test given by Devi [START_REF] Devi | An Improved Schedulability Test for Uniprocessor Periodic Task Systems[END_REF]. This test also has to be performed for the deadline of each task. Setting I = D k in the above equation results in SuperPos( 1). This proves Lemma 2. The relationship between the test by Devi and the superposition approach allows to include the extensions of the test by Devi described in [START_REF] Devi | An Improved Schedulability Test for Uniprocessor Periodic Task Systems[END_REF] into the super position approach. The extensions concern practical relevant issues like switching time, priority ceiling protocol, self-suspension and limits for the number of priorities.

Superposition vs. real-time calculus

In the concept of real-time calculus [START_REF] Chakraborty | Performace Evaluation of Network Processor Architectures: Combining Simulation with Analytical Estimation[END_REF] based on the network calculus [START_REF] Le Boudec | Network Calculus -A Theory of deterministic Queuing Systems for the Internet[END_REF] the demand and the capacity of a system are described by arrival and service curves. The idea of these functions is the same as in the processor demand test, apart from that the capacity is not regarded as bisecting line but also as a function. The idea behind the real-time calculus is to define mathematical operations on the arrival and service curves to solve the feasibility test problem. By definition the curves are unlimited. Therfore the equations behind this concept are unfortunatly expensive to compute in the case of general arrival and service curves [START_REF] Chakraborty | Performace Evaluation of Network Processor Architectures: Combining Simulation with Analytical Estimation[END_REF]. To make the concept practicable a piecewise linear approximation with up to three staight line segments is proposed. The error of this approximation is unkown. By using the results of Section 3.5 it is possible to calculate a lower bound on the approximation error of the approximated real-time calculus. Figure 4 shows the realtime calculus approximation of one task. First the approximation of a simple periodic task with two lines is shown (a), second the approximation of a bursty task is outlined (b). In this case three lines are needed for a good approximation.

Comparing Figure 3 with Figure 4 a) shows a close relationship between the approximation of the real-time calculus and the test given by Devi. The real-time calculus approximation is a bit worse than the test given by Devi because of the limited number of curves in the approximation of the real-time calculus. As shown in the last section the test by Devi is equal to SuperPos(1) of the superposition approach. The main difference between the test by Devi and the real-time calculus is the specification of bursts which can be only expressed by the real-time calculus. By using event streams it is easy to analyse burst by the superposition test [START_REF] Albers | An Event Stream Driven Approximation for the Analysis of Real-Time Systems[END_REF]. However, this leads to a higher complexity then the test by Devi because of each element of the burst has to be handled as a seperate element of the event stream. ------------------------------------

τ i Γ ∈ D τ D i ≤ ( ) { } = I C i i D i I ≤ ( ) ∀ ∑ C i T i -----I D i - ( ) ⋅ i D i I ≤ ( ) ∀ ∑ + ≥ C i i D i I ≤ ( ) ∀ ∑ = I C i T i ----- D i T i -----C i ⋅ i D i I ≤ ( ) ∀ ∑ - i D i I ≤ ( ) ∀ ∑ ⋅ + 1 k Γ ≤ ≤ ( ) ∀ D k D k C i T i ----- i 1 = k ∑ ⋅ T i min T i D i , ( ) - T i -
-     C i ⋅ i 1 = k ∑ + ≥ D k k C i T i ----- i 1 = k ∑ ⋅ T i D i - T i ----------------     C i ⋅ i 1 = k ∑ + ≥ C i i 1 = k ∑ ≥ D k C i T i ----- D i T i -----C i ⋅ i 1 = k ∑ - i 1 = k ∑ ⋅ +

Improved feasibility tests

Approximated feasibility tests are only sufficient. This is a problem because not all scheduable task sets are accepted by this tests. Even if the degree of sufficiency is selectable the tests fails to recognize feasible task sets (Figure 1). Even worse, choosing a high degree of sufficiency leads to a test with long execution time, while choosing a low degree leads to a bad acceptance rate for the feasible task sets. The idea is to use different levels of approximation, starting with a fast approximation (SuperPos(1)) and switch to a slow one just as necessary.

Dynamic error test

This idea leads to a fast test for all those task sets which the sufficient tests could recognize. The algorithm for the new test is shown in Figure 5. The test starts at the level SuperPos( 1). This level allows all tasks to be approximated after their first job. The test runs at this level until either the test succeeds or the approximated demand (dbf´) exceeds the actual test interval (I act ) and the task set is not feasible by this approximation. In this case it is necessary to rise the level and withdraw the approximations for those tasks which would not be approximated using the new level (Γ rev ). It is not necessary to recalculate the whole test because the values calculated by the first approximation can be reused.

Lemma 3: If dbf'(I,G) ≤ I for an interval I than dbf(I',G) ≤ I' for all intervals I' between I and I next . I next is the next test interval after I which is not approximated.

The prove of this lemma is visualized in Figure 6 and can also be followed using Lemma 4. Therefore if the test fails at I next , the previous test guarantees all intervals which are smaller than I next , even if they are approximated.

Lemma 4: Let be two consecutive test intervals for . If we assume it exists a

for which and applies then the approximated demand bound function holds [START_REF] Albers | An Event Stream Driven Approximation for the Analysis of Real-Time Systems[END_REF]. Proof: See Section 3.2 in [START_REF] Albers | An Event Stream Driven Approximation for the Analysis of Real-Time Systems[END_REF]. For all tasks for which the approximation is revised due to the switch of the level the next test interval following I act has to be investigated: Lemma 5: Following test interval This interval is added to the list of test intervals. It is further necessary to reduce the approximated demand by the overestimated approximation costs for these revised tasks. These costs are given by app. Let Γ rev be the set of all tasks for which the approximation is revised: Lemma 6: Overestimated approximation costs If dbf'≤ I act the new level is sufficient, otherwise it has to be increased. If no task is approximated before increasing the level the demand bound function exceeds the capacity and the test fails. We propose to double the level at each step which limits the amount of steps to . This is small compared to the total amount of test intervals. Only task sets which cannot be evaluated using a fast level will need a long evaluation time. These task sets would not be accepted by existing sufficient tests like the test by Devi. Task sets accepted by the test by Devi are accepted by this test running completly on the level SuperPos(1). This condition holds for all levels of the superpositon test. It is not necessary for a good average case performance of the analysis to combine sufficient and necessary tests. The maximum level for the dynamic test can be limited. The result is a test with a strictly limited worst-case run-time and a good average case run-time.

All approximated test

Despite that the proposed test outperform the existing approaches by orders of magnitude, it can be improved even further. Especially for task sets containing very small and very large tasks, the dynamic test could switch soon into higher levels. Considering many test intervals may result in an unnecessary effort. It could be the case that only a few test intervals are critical and that it is possible to approximate the others. This leads to a new test. The algorithm for this test can be found in Figure 7. The goal of the new algorithm is to reduce the number of considered test intervals further. Figure 7 shows the algorithm. Instead of using fixed test bounds for each task, approximation is done as much as possible. The first test intervall resulting out of the first job of each task is inserted into testlist. Testlist is processed in ascending order. All the following test intervalls are approximated first. Only if a test fails for an test interval I test , the approximation of the demand bound function of each task is step by step revised until the test either succeds or no task is approximated any more. The revision is done by replacing the approximated costs of the task by their real cost. Because of quitting the approximation in this interval it is necessary to add one

I I next , dbf′ I ( ) I ∆ I I I ∆ + I next < < dbf I I ∆ + ( ) I I ∆ + > dbf′ I ( ) I > NextInt I τ , ( ) I D τ - T τ -------------- 1 +     T τ D τ + = app I Γ rev , (
)

I D i - T i ------------- I D i - T i ------------- -       τ i ∀ Γ rev ∈ ∑ C i = n max
additional test interval for each revised task into testlist. These additional test intervals can be calculated using Lemma . Note that it is only necessary to calcultate the interval following I test because the approximation has already verified all test intervals smaller than I test . The algorithm terminates if it is possible to approximate all tasks successfull in one test interval or if the test fails. If the initial test interval is accepted for each task without generating new test intervals, the behaviour and the performance of the test is equal to the test given by Devi [START_REF] Devi | An Improved Schedulability Test for Uniprocessor Periodic Task Systems[END_REF].

Feasibility bound

A feasibility bound describes the upper limit for all intervals which are necessary to be tested. It is important to find a short one because this limits the effort for the feasibility test. A good overview of the different feasibility bounds can be found in [START_REF] Stankovic | Deadline Scheduling for Real-Time Systems EDF and Related Algorithms[END_REF]. Baruah et al. [START_REF] Baruah | Preemptive Scheduling Hard-Real-Time Sporadic Tasks on One Processor[END_REF] defined such a bound for the processor demand test, which is part of Definition 3. Another one can be derived from the busy period condition [START_REF] Stankovic | Deadline Scheduling for Real-Time Systems EDF and Related Algorithms[END_REF]. George et al. [START_REF] George | Preemptive and Non-Preemptive Real-Time Uni-Processor Scheduling[END_REF] define a bound which is smaller than the bound given by Baruah et al:

The new all approximated superpositon approach delivers a new feasibility bound. It is reached (and no further test interval is needed) if for a test interval the difference between the demand bound function and the capacity allows the approximation of all tasks. A task system with a utilization lower 100% can never exceed the capacity beyond this interval. Using Lemma 6 the sum of the demand bound function and the approximation errors can be calculated: This gives the new feasibility bound:

If the condition I sup ≥ D max is used, it can be followed:

Using leads to the following bound:

For the case that all C τ ≤ D τ this bound is the same as the bound given by George et al., for the other cases this new bound is lower than this bound. This relationship allows a better understanding of the bound and leads to a integrated feasibility theory for EDF. The main contribution of this result is that it is not necessary for the new test to calculate and check the feasibility bound by George et al. The superposition bound is tighter and is checked in an implicit way. It might be interesting to calculate the busy period of the system as outlined in [START_REF] Stankovic | Deadline Scheduling for Real-Time Systems EDF and Related Algorithms[END_REF], because this bound might be tighter than the superposition bound under some conditions. Calculating this bound however has exponential complexity and may need more effort than the test without this bound.

Experiments

We have generated a large number of random task sets to evaluate the performance gain due to the new tests. As a metric we counted the test intervals checked by each of the algorithms. This metric is common to evaluate feasibility tests [START_REF] Bini | The Space of Rate Monotonic Schedulability[END_REF], [START_REF] Pellizzoni | A New Sufficient Feasibility Test for Asynchronous Real-Time Periodic Task Sets[END_REF] and shows exactly the behavior of the different algorithms.

The generation of the random task sets follows the uniform distribution proposed by Bini [START_REF] Bini | Biasing Effects in Schedulability Measures[END_REF]. In Figure 8 a test was performed using 18,000 task sets with a utilization between 90% and 99% (high utilizations are hard to test). It shows the average and the maximum iterations needed for the tests. The size of the task sets varied between 5 and 100 tasks using a uniformed random distribution. They had an average gap of 20%, 30% and 40%. The gap describes the difference between deadline and period. The sizes of periods are also equally distributed, the ratio between the maximum and the minimum period was of no concern for this experiment. The result of the experiment is that the all approximation test needs 10 to 20 times less iterations than the processor demand test, which goes up to 200 times less effort considering the maximum amount of iterations.

Figure 9 shows the result of another experiment which investigates the effect of the ratio T max /T min . Therefore the test was performed with a ratio varying from 100 to 1,000,000. The results are presented using an exponential scale. Such high ratios could for example be possible if system interrupts and the schedulability overhead are defininded as tasks. For each value 4,000 tasks set where generated randomly with a size between 5 and 100 tasks and an average gap between 10% and 50% and an utilization varying between 90% and 100%. The first graph shows the maximum measured effort needed for the processor demand test which increases up to more than 50 million iterations. The effort of the other values is visualized in the second graph. Also there are some variations due to the random values especially for the dynamic test. The measured effort of both new tests are far below the effort needed for the old test. The maximum effort measured for the dynamic test was about 9,000. For the all approximation test it is about 3,000 iterations. Another interesting point is that the effort doesn't depend on the ratio of the periods. This becomes even more obvious when investigating the average effort needed. For ------------------------------------------------------------ -----------------------------------------------------, ( ) = the all approximation test it varies between 102 and 116 iterations, as opposed to 465 to 955,053 for the processor demand test. Tab. 1 contains some results for task sets coming from real examples. The task set of Burns and of the modified set of Ma & Shin can be found in [START_REF] Albers | An Event Stream Driven Approximation for the Analysis of Real-Time Systems[END_REF], the Generic Avionics Platform example (GAP) in [START_REF] Stankovic | Deadline Scheduling for Real-Time Systems EDF and Related Algorithms[END_REF] and the other two task sets in [START_REF] Gresser | Echtzeitnachweis Ereignisgesteuerter Realzeitsysteme[END_REF]. The amount of tasks are small (7 to 21 tasks) but even for such small examples the new tests need between 5 and 100 times less iterations than the processor demand test. The run-time overhead of one iteration ot the new tests is small compared to both alternative algorithms, the processor demand test and the test by Devi. Only the approximation leads to a some more effort. Compared to the algorithm of Devi the overhead can be completely eliminated.

i ∀ Γ ∈ I george 1 D i T i ----- -     C i ⋅ τ i Γ ∈ D i T i ≤ ∧ ∑ 1 U - -
= I app I τ , ( ) dbf I τ , ( ) + τ Γ ∈ ∑ ≥ I sup I sup D τ - T τ ---------------------- I D τ - T τ -------------- -       C τ I D τ - T τ --------------1 + C τ ⋅ τ ∀ i Γ ∈ I D τ ≥ ∑ + τ Γ ∈ ∑ = I sup I sup C τ T τ ------ τ Γ ∈ ∑ ⋅ C τ D τ ⋅ T τ ----------------- τ Γ ∈ ∑ - C τ τ Γ ∈ ∑ + = U C T ⁄ ∑ = I sup min D max 1 D i T i ⁄ - ( ) C i ⋅ τ i ∀ Γ ∈ ∑ 1 U - -

Conclusion

We proposed two new feasibility test for EDF. They are exact and outperform the existing tests by orders of magnitude. Task sets which are recognized by the existing sufficient test or approximations can be evaluated by the new test with a comparable effort. We proved that the new concept integrates the processor demand test, the feasibility bound by George et

Figure 1 :

 1 Figure 1: Results for different values for SuperPos(x)

Figure 2 :

 2 Figure 2: Approximation by Devi for two tasks

Figure 3 :Figure 4 :

 34 Figure 3: Approximation by Devi for a single task

Figure 5 :Figure 6 :

 56 Figure 5: Dynamic Test ALGORITHM DynamicError IF U >1 ⇒ not feasible Imax = minimum feasibility interval; :testlist.add(τ ι ,T i + D i ) WHILE (testlist ≠ {} AND I act < Imax) τ i , I act = testlist.getNext() dbf' = dbf'+ C τ + (I act -I old ) * Uready WHILE (dbf' > I act ) IF (ApproxList = {}) ⇒ NOT FEASIBLE increase level; : Uready = Uready -C j , / T j , dbf' = dbf' -app(I act ,τ j ) testlist.add( τ j , NextInt(I act ,τ j )) END WHILE IF (I act < Testboarder(τ) testlist.add(τ, I act + T i ) ELSE Uready = Uready + C i / T i ApproxList.add(τ); I old =I act END WHILE ⇒ FEASIBLE τ i ∀ Γ ∈

Figure 7 :

 7 Figure 7: All approximated test

Figure 8 :

 8 Figure 8: Results with different utilizations

Figure 9 :

 9 Figure 9: Results with different values for T min / T max

2: Demand bound function Dbf(I) [2]: The max- imum cumulated execution requirement of jobs having both request time and deadline within interval I It is possible to split the demand bound function into demand bound functions for each single task. dbf(I,τ) is the

  cumulated execution requirement of only one task. The available capacity of execution time in an interval I is exactly the length of the interval. Testing the demand bound function for all intervals against the capacity leads to an exact test. To make the test tractable it is possible to calculate a maximum test interval (I max ) which is an upper bound (feasibility bound) and it is only necessary to test the demand bound function for intervals lower than I max .

	The maximum demand
	for an interval I can be found if all tasks are released
	synchronous at the beginning of I and only those jobs are
	considered which have both their release time and their
	absolute deadline within I.
	Def.

Baruah et al.

proposed an exact test for task systems with deadlines shorter than their periods. The main idea was to calculate the maximum demand of all tasks within a time interval and compare it with the available capacity of the processor. The demand is the cumulated worst-case execution time of the relevant jobs.

Def. 3: Processor demand test [2]: A task

  system Γ is feasible if and only if dbf(I,Γ) ≤ I for all . It is only necessary to check those intervals where the value of dbf(I,Γ) is changed. The absolute deadlines of all jobs determine these intervals. Other values for I max are discussed in Section 4.3.

  al. and the sufficient feasibility test by Devi.

				Maximum effort for different utilizations
								Dynamic Processor Demand All approximated
	Iterations
		90	91	92	93	94	95	96	97	98	99
						Utilization (%)
				Average effort for different utilizations
		6000 7000						Dynamic Processor Demand All Approximated
		5000
	Iterations	3000 4000
		2000
		1000
		0 90	91	92	93	94	95	96	97	98	99
						Utilization (%)

Table 1 :

 1 Iterations for example task graphs

	Test	Devi	Dyn.	All Appr. Proc. Dem.
	Burns	14	14	14	1,112
	Ma & Shin FAILED	16	11	61
	GAP	18	18	18	1,228
	Gresser 1	FAILED	24	20	307
	Gresser 2	FAILED	34	25	205

Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05) 1530-1591/05 $ 20.00 IEEE

The research described is supported by the Deutsche Forschungsgemeinschaft under grant SL 47/1-1


C Freissinet
email: caroline.freissinet@nasa.gov

D P Glavin

K Miller

A Buch

A E Brunner

M Cabane

J L Eigenbrode

A G Fairen

S Kashyap

M Martin

R Navarro-Gonzalez

A Steele

R E Summons

C Szopa

P R Mahaffy

FROM SAM INSTRUMENT BACKGROUND TO MARTIAN SIGNAL: CHALLENGES OF SOLID SAMPLE ANALYSES ON MARS

Introduction: Amongst the Sample Analysis at Mars (SAM) experiment capabilities, the GCMS mode (coupling of the Gas Chromatograph and the Quadrupole Mass Spectrometer instruments) was designed for the separation and identification of the chemical components of gases evolved from a solid sample, either processed using heat in pyrolysis or adding a chemical reactants in the wet chemistry experiments [1]. However, SAM empty cup blank runs revealed a suite of internally derived volatile compounds, which can interfere with a martian signal detection. Thus, understanding the SAM instrument background is an essential step before resolving the origin of the signal as a possible martian hydrocarbon signature.

Here we report on various chlorohydrocarbons (chloromethanes, chlorobenzene and dichloroalkanes) detected above instrument background levels at the Cumberland (CB) drill site, and discuss how they might be or not be related to SAM internal sources.

SAM solid sample analyses:

The analyses of gases released from the Rocknest (RN), John Klein (JK), and CB solid samples were conducted by heating the sample portions in a pyrolysis oven to >800ºC, at a rate of 35ºC/min under 1 standard cubic centimeters per min He flow and 1) monitoring the evolved gases with a quadrupole mass spectrometer (Evolved Gas Analysis, EGA mode), and 2) trapping a specific temperature range of evolved gases using hydrocarbon traps containing Tenax TA and GR and then heating the traps to send the gases through one of the six gas chromatographic columns before analysis in GCMS. Prior to EGA and GCMS analyses of the first 3 solid samples (RN, JK and CB) collected by MSL and delivered to SAM, a procedural blank run was carried out with an empty quartz cup to characterize the volatile sources/background internal to the SAM instrument.

Discussion:

SAM internal sources: The hydrocarbon trap(s) Tenax products are a major part of the SAM internal background measured by GCMS. Other major contributors to the background signal are the reaction products of one of the chemicals used for SAM wet chemistry experiment: N-methyl-N-tertbutyldimethylsilyl-trifluoroacetamide (MTBSTFA) [2]. This molecule was sealed inside each of the seven derivatization cups present in the SMS. Any MTBSTFA released from the cups will readily react with the residual water present inside the instrument to form byproducts, identified in the GCMS blanks by their mass spectra and used to estimate the initial amount of MTBSTFA present in the sample.! The presence of reactive species in the background can create newly formed products by interaction with inorganic species in the martian regolith, such as oxychlorine compounds. Before confirming detection of martian molecules, the possibility that these compounds could be derived from reactions between martian volatiles and terrestrial components internal to SAM has to be eliminated. For this reason, the empty cup blank runs on Mars are required, as are the laboratory experiments performed under SAM-like conditions to understand the reaction products of molecules in the background with known inorganic species in the martian regolith [3,4,5].

The case for chlorinated hydrocarbons: Numerous chlorohydrocarbons have been identified in some CB samples, including chloromethane, dichloromethane, trichloromethane, carbon tetrachloride [6,7,8], chlorobenzene, 1,2-dichloropropane, 1,1-and 1,2dichlorobutane and possibly 1,2-dichlorethane (Fig. 1). Although the chlorine in these compounds is believed to come from a martian oxychlorine phase [6,7], the origin of the primary carbon source requires additional investigation. 2796.pdf 45th Lunar and Planetary Science Conference (2014) [6]. It is notably the case for the RN samples, where the primary source of carbon for the chloromethanes has been argued to be terrestrial in origin [6,8]. Strategies have been successfully developed to reduce the MTBSTFA source in the CB-5, CB-6 triple portion and CB-6-residue runs (i.e. the CB-6 sample reheated under the same conditions as CB-6) and the MTBSTFA reduction offered additional insights to the origin of the chloromethane carbon. Indeed, the estimated initial amount of MTBSTFA carbon displayed a decreasing trend from CB-3 (0.032 ± 0.006 nmol of MTBSTFA C; no cup preheating) to CB-5 (0.018 ± 0.004 nmol of MTBSTFA C; cup preheated to ~335ºC) to CB-6 (0.009 ± 0.002 nmol of MTBSTFA C; cup preheated to ~390ºC). This decreasing trend is also observed for chloromethane and dichloromethane abundances measured by GCMS (Fig. 2), thus confirming MTBSTFA as a major carbon source for these compounds. However, distinctly larger amounts of chloromethane and dichloromethane were released from the Sheepbed mudstone (JK and CB) than from RN, suggesting a possible additional martian source of carbon [7]. It is interesting to recall here that chloroand dichloromethane were the only two chlorinated compounds detected by Viking in 1976 after thermal volatilization of surface soils by the GCMS instruments at the Viking landing sites 1 and 2, respectively [9]. The authors concluded that the trace amounts detected were likely derived from terrestrial sources, although this hypothesis has been revisited [10] and challenged [11] and a martian carbon contribution to the chloromethanes measured by Viking still cannot be ruled out. Although the amount of carbon available from MTBSTFA alone is sufficient to form all of the chloromethanes detected in the SAM experiments at CB, trichloromethane and carbon tetrachloride do not decrease with MTBSTFA reduction (Fig. 2), and are not observed in the CB-6residue. These combined observations may indicate a non-terrestrial source of CHCl 3 and CCl 4 . Given the significant reduction of volatiles present in the instrument background in the CB-5 run compared to CB-3 and the lack of these chlorinated alkanes in any of the RN runs, in the blank run or in the reheated CB-6-residue, a martian carbon source for 1,2-DCP in CB is possible. The fact that no 1,2-DCP and none of the dichlorobutane isomers are detected in the laboratory pyrolysis GCMS experiments with MTBSTFA and perchlorates, and that no C3-or C4alkanes have been detected in similar experiments, suggests that neither MTBSTFA nor the hydrocarbon trap components are a major carbon contributor to these chlorohydrocarbons detected in CB. The tentative identification of propane in the CB-5 GCMS analysis, made difficult by its low retention time and weak mass spectrum, indicates that aliphatic hydrocarbons may be available as precursors for the 1,2-DCP detected at CB. This propane could be a fragment of a larger hydrocarbon in the CB sample itself. Laboratory experiments using SAM-like conditions show that 1,2-DCP can be formed from C3hydrocarbons or C3-alcohols when heated in the presence of perchlorates. In addition, 1,2-DCP is a product of the pyrolysis of the Murchison meteorite organic material in the presence of perchlorates [4].

Chlorobenzene: Another paper at this conference [3] discusses the origin(s) of chlorobenzene detected by SAM and a possible martian origin for the elevated levels of chlorobenzene detected at CB.

Conclusion:

Taken together, these results indicate that the internal SAM sources create a background that challenges the analysis of solid samples in search for organics, creating interferences between terrestrial and possible indigenous carbon sources. We have been exploring the possibility of SAM-derived C contributions to chlorohydrocarbon generation. Current observations provide no direct link between SAM internal sources and the chlorohydrocarbons detected on Mars, thus a martian organic contribution to the chloromethanes, dichloroalkanes and chlorobenzene detected at CB is possible.

Fig. 1 :

 1 Fig. 1: Gas chromatogram of the CB-3 sample. 1: chloromethane, 2: dichloromethane, 3: trichloromethane, 4: carbon tetrachloride, 5: dichloroethane, 6: dichloropropane, 7: dichlorobutane, 8: chlorobenzene It is known from laboratory experiments that the pyrolysis of MTBSTFA in the presence of Ca-and Mg-perchlorates generate all the four types of chloromethanes, and that at least part of these compounds detected in SAM derives from this reaction

Fig. 2 :

 2 Fig. 2: Comparative abundances of chlorine-bearing hydrocarbons in RN, JK and CB. Abundance trend between the CB-3 sample (no MTBSTFA-reduction) and CB-5 sample (MTBSTFA-reduction).

1, 2 -

 2 Dichloropropane (1,2-DCP), as well as 1,1-and 1,2-dichlorobutane and possibly 1,2-dichloroethane have all been identified in the CB-3 and CB-5 runs.

Lunar and Planetary Science Conference (2014)

	45th				2796.pdf
		Rocknest (RN)	John Klein (JK)	Cumberland (CB)
			Sheepbed mudstone
				CB-3	CB-5
	CH 3 Cl%	+"	+"	+"
	CH 2 Cl 2%	+"	+"	+"
	CHCl 3%	+"	+"	+"
	CCl 4%	+"	+"	+"
	C 3 H 6 Cl 2%	#"	#"	+"
	C 6 H 5 Cl%	+"	+"	++"


Caroline Freissinet
email: caroline.freissinet@nasa.gov

Daniel P Glavin

A Buch

Cyril Szopa

S Kashyap

H B Franz

Jennifer L Eigenbrode

W B Brinckerhoff

R Navarro-González

A MARTIAN MUDSTONE C Freissinet

S Teinturier

C A Malespin

B D Prats

P R Mahaffy

First In Situ Wet Chemistry Experiment on Mars Using the SAM Instrument: MTBSTFA Derivatization on a Martian Mudstone

établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction:

The wet chemistry experiments on the Sample Analysis at Mars (SAM) instrument were designed for the extraction and identification of refractory organic chemical components in solid samples using gas chromatography-mass spectrometry (GCMS) [1]. The chemical derivatization agent used, N-methyl-N-tert-butyldimethylsilyl-trifluoroacetamide (MTBSTFA), was sealed inside seven Inconel metal cups present in the SAM Sample Manipulation System (SMS). Although none of these foil-capped derivatization cups have been punctured on Mars for a wet chemistry experiment, data from SAM has shown that some MTBSTFA vapor leaked into the SMS and is detected mostly as its reaction product with water in both empty cup blank runs and solid sample experiments [2]. Despite the MTBSTFA background in SAM, several dichlorinated alkanes and chlorobenzene of martian origin have been identified by GCMS above background levels in a drilled mudstone sample called Cumberland (CB) collected at Yellowknife Bay [3]. Here we report preliminary results from an MTBSTFA derivatization (MD) GCMS experiment that was optimized for the detection of MTBSTFA residual vapor reaction products with refractory organic compounds and other molecules present in the CB mudstone sample.

MTBSTFA Derivatization:

The CB sample used in the MD experiment was drilled in the Sheepbed mudstone on Sol 279, and a fresh triple portion of the mudstone sample (~ 135 ± 31 mg) was added on top of a previously pyrolyzed CB single portion sample. This "doggy bag" sample was left inside SAM for about 400 sols and accumulated and reacted with MTBSTFA vapor present in the SMS during the traverse to the base of Mt. Sharp. The MD experiment was conducted as a multi-sol experiment as follows: 1) The first step (MD1) consists of a low temperature heating of the sample from ambient to ~125 ºC at a rate of 35 ºC/min under 1 standard cubic centimeters per min He flow during which time volatiles released from the sample were sent to the SAM hydrocarbon trap (silica beads, Tenax TA, and Carbosieve G) set at a temperature of 5°C. The sample was then heated from 125ºC to ~ 250 ºC to decompose perchlorates and other oxychlorine compounds in the sample to release O 2 , in order to limit the combustion of possible organic molecules and their MTBSTFA derivatives in the second MD step. Volatiles released from the sample during heating to 250°C were analyzed directly using the quadrupole mass spectrometer (QMS) only. MTBSTFA reaction products and other volatiles collected on the hydrocarbon trap during the ~125 °C heating step were then analyzed by GC separation (MXT-CLPesticide, 30 m length, 0.25 mm ID, 0.25 µm film thickness) and QMS analysis (scans from m/z 2 to 407) after heating the trap to 310 °C. The cup was then removed from the pyrolysis oven and placed back into the SMS where the sample could re-adsorb and react with MTBSTFA vapor present in the SMS for 48 hours. 2) The second MD step (MD2) utilized a higher temperature heating from ambient to ~900 ºC to perform derivatization of molecules in the sample that evolve at elevated temperatures, with much less O 2 available in the sample for combustion of organics. In the MD2 step, the entire volatile fraction released from the sample during the heating was sent to the hydrocarbon trap for GCMS analysis as previously described.

After the MD1 and MD2 GCMS analyses, a procedural control experiment was carried out using the identical SAM analytical conditions on a quartz cup containing a triple portion of CB sample that was heated previously to ~900 °C twice on Sol 382 and Sol 394.

Discussion: MTBSTFA was selected as one of the chemical reagents used in the SAM derivatization experiments since MTBSTFA can react with a broad range of molecules containing a labile hydrogen such as alcohols, primary and secondary amines, carboxylic acids and amino acids in the free form (Figure 1). The silyl ester products of these molecules are typically much more volatile than the original non-derivatized molecule, which enables the transfer of the MTBSTFA derivatives through the SAM gas processing system for GCMS analysis [4].

2934.pdf 46th Lunar and Planetary Science Conference (2015)

The initial abundance of MTBSTFA adsorbed on a cup and a sample was estimated from the abundances of the primary MTBSTFA byproducts formed from its reaction with water molecules including tertbutyldimethylsilanol, N-methyl-2,2,2-trifluoroacetamide, and1,3-bis(1,1-dimethylethyl)-1,1,3,3tetramethyldisiloxane [2], and was expected to be at least 116 nmol or 0.03 mL, as estimated from the CB-Blank-1 EGA experiment [3]. In the MD2 experiment, the abundances of MTBSTFA reaction products detected by GCMS and corresponding MTBSTFA abundances released from the Cumberland "doggy bag" triple portion were found to be much higher, in the µmol range. This result is not surprising since the MD experiments were optimized for the concentration and detection of MTBSTFA reaction products.

In Figure 2, several key masses detected by GCMS that correspond to potential high molecular weight MTBSTFA reaction products are plotted. Several masses up to m/z 358 (the highest yet detected after pyrolysis of a sample by SAM on Mars) are observed in the MD2 GCMS analysis of the CB triple portion mudstone sample, but were not identified above background level in the twice-heated CB residue analysis that served as a blank (e.g. m/z 281 at retention time 13.1 min, Fig. 2). Numerous peaks were detected by GCMS above background and we are continuing to work to identify the derivatized compounds by comparison to mass spectral libraries of known MTBSTFA derivatives and by analysis of the fragmentation patterns. Our preliminary results from MD2 compared to the control experiment indicate that several MTBSTFA derivatized aromatic hydrocarbons may be present in the sample. Chlorobenzene, a chlorohydrocarbon that is not derived from MTBSTFA-perchlorate reactions was also detected by GCMS in the MD experiments. This chlorobenzene may originate from reactions between oxychlorine species and metastable oxidized aromatic hydrocarbons in the Cumberland sample [5]. MTBSTFA derivatization products such as reaction products with water from the sample and from the SAM background, with HCl from perchlorate decomposition and with phenol from the hydrocarbon trap degradation were also detected in this GCMS experiment. The presence of those compounds indicates that enough MTBSTFA was present to perform derivatization in the sample, as well as downstream in the gas processing system.

Conclusion:

These experiments represent the first successful MTBSTFA derivatization experiment on Mars. Several MTBSTFA reaction products were generated during reactions with the Cumberland mudstone sample at elevated temperatures, with some products containing mass fragments up to m/z 358. We are continuing anthe alysis of this interesting data set to identify these derivatization products that should shed additional light on the chemical nature of the organic matter present in the Cumberland mudstone.

References:

Figure 1 :

 1 Figure 1: Example MTBSTFA reaction with an amino acid to form the volatile silyl ester derivative and a trifluoro-N-methylacetamide (TFMA) byproduct that are both detectable by the SAM GCMS.

Figure 2 :

 2 Figure 2: Comparison of some specific high masses for (a) the CB sample and (b) the CB blank for MD2 experiments, after the sample has been cleaned out of part of its O2 in MD1.

pdf 46th Lunar and Planetary Science Conference (2015)

  [1] Mahaffy, P. et al. (2012) Space Sci Rev, 170, 401-478. [2] Glavin, D. et al. (2013) JGR Planets, Vol. 118, 1-19. [3] Freissinet et al. (2015) JGR Planets, submitted. [4] Buch, A. et al. (2006) PSS, 54, 1592-1599. [5] Glavin et al. (2015), this conference.

			m/z 90						180
		5 10	m/z 92 m/z 112 m/z 207					160
			m/z 221
	MS response (counts/s)	10 3 10 4	m/z 225 m/z 263 m/z 281 m/z 289 m/z 305 m/z 356					GC_IT_FLASH2	140 120 100 80	GC Column Temperature (°C)
									60
		2 10							40
		11.6	8		11.8 10	12.0 14 Retention Time (minutes) s x10 3 12		16	12.2	18
									180
			m/z 90
		5 10	m/z 92 m/z 112 m/z 207					160
	MS response (counts/s)	10 3 10 4	m/z 221 m/z 225 m/z 263 m/z 281 m/z 289 m/z 305 m/z 356					140 120 100 80	GC Column Temperature (°C)
									60
		2 10							40
			8	11.6	10	11.8 12 Retention Time (minutes) 14 s x10 3	12.0	16	18	12.2

GC_IT_FLASH2

2934.


Samar Abdi
email: sabdi@cecs.uci.edu

Daniel Gajski
email: gajski@cecs.uci.edu

Functional Validation of System Level Static Scheduling

Increase in system level modeling has given rise to a need for efficient functional validation of models above cycle accurate level. This paper presents a technique for comparing system level models, before and after the static scheduling of tasks on processing elements of the architecture. We derive a graph representation from models written in system level design languages (SLDLs) and define their execution semantics. Notion of functional equivalence of system level models is established using these graphs. We then present well defined rules for reduction of such graphs to a normal form. Finally, we show how to check for functional equivalence of two system level models by isomorphism of their normal graph representations. A checker built on the above concept is used to automatically validate the functional correctness of the static scheduling step. As a result, the models generated for various scheduling decisions do not have to be reverified using costly simulations.

Introduction

System level (SL) design has received much attention lately due to the rising complexity of modern HW-SW designs. Design methodologies now involve several modeling stages to take an executable specification of the design to a cycle accurate implementation in a gradual, step wise fashion. At each step, the system model is transformed to reflect the design decision made at that step. However, it is imperative that the functionality of the original specification is preserved as the design progresses through these incremental model transformations. In other words, we need to validate if two models, before and after the implementation of a design decision, are functionally equivalent. In this paper, we look at functional validation of model transformations resulting from system level static scheduling.

A possible system level design methodology is as follows. We start by distributing the specification tasks (re-ferred to as behaviors) onto different HW and SW processing elements (PEs) to derive an architecture model. However, the behaviors in this architecture model are not yet scheduled. The static scheduling step allows for serializing the concurrent behaviors on the HW PEs, since they will be implemented with a single controller. Also, at this stage, the communication between PEs may be statically scheduled to optimize timing. Communication synthesis adds bus architecture and arbitration policy, resulting in a completely scheduled bus transaction model. Finally, the SW tasks are compiled for the target processor and the HW behaviors are synthesized.

Research on task level static scheduling has mostly been done for embedded systems targeting real time applications [START_REF] Wong | Static task scheduling of embedded systems[END_REF]. For distributed systems, static communication scheduling [START_REF] Surma | Collision graph based communication scheduling for parallel systems[END_REF] has been proposed for improving timing. SLDLs like SystemC 2.0 [START_REF] Gajski | SystemC[END_REF] and SpecC [START_REF] Gajski | SpecC: Specification Language and Methodology[END_REF] help in incorporating task level static scheduling in system level design methodologies by allowing the exploration of different schedules for both computation and communication in a much speedier manner than cycle accurate co-simulation. This has led to research being directed towards modeling and verification at system level in order to verify the correctness of design steps. Traditional software model checking [START_REF] Holzmann | The model checker spin[END_REF] and bounded model checking [START_REF] Clarke | A tool for checking ANSI-C programs[END_REF] allow property verification of high level models written in C-like languages. However, to the best of our knowledge, there has been little work in equivalence verification of system level models. The closest work [START_REF] Saito | An equivalence checking methodology for hardware oriented c-based specifications[END_REF] relies on textual comparison of models and requires them to be syntactically very similar.

The rest of the paper is organized as follows. In Section 2, we look at how and why is static scheduling performed in SL models. Section 3 presents a graph based abstraction of SL models using key language concepts. We also look at the execution semantics of such graphs and their extraction from SLDL code. In Section 4, we propose a method for checking functional equivalence of SLDL models by reducing their abstracted graphs to a normal form. The rules for performing this graph normalization are also explained. Finally, we present experimental results for a functional equivalence checker based on the above concept and wind up with conclusions.

Static scheduling in SL models

Static scheduling is performed in system level models either due to resource constraints or timing optimization. Behaviors mapped to HW are implemented using controller(s) and data path(s). As a result, behaviors that are grouped for implementation with the same controller must be serialized. Reordering of behaviors can also take place as a result of communication scheduling. Such a scenario is shown in Figure 1, where data d is sent from PE1 to PE2 over channel c. The channel implements rendezvous communication semantics, i.e. both sender and receiver must synchronize for the transaction to take place. Consequently, for the case shown in Figure 1

Graph abstractions of SL models

Computation in SLDLs is encapsulated inside behaviors that read data from variables via in-ports, perform local computation, and then write data to variables via outports. Most SLDLs, also support the concept of hierarchy, where a complex behavior can be described in terms of subbehaviors and their compositions. A behavior without any sub-behaviors is called a leaf behavior. We will assume that model transformations will treat the leaf behaviors as atomic. We also define a class of leaf behaviors, B I , consisting of identity behaviors that output the same data as their input. They do not perform any computation, and are typically used as place holders or for data routing. We assume channel transactions only between identity behaviors.

In this section we will define two graphs, namely the behavior control graph (BCG) and the port connection network (PCN). The former is used to capture the control dependencies between leaf behaviors, while the latter captures data dependencies between various objects in the model.

q1 qm q1' qn' b1_queue b 1 _ q 1 '_ q u e u e b 1 _ q n '_ q u e u e b 1 b k b k _q n _ q u e u e

Control and data dependency graphs

The BCG is a directed graph (N,E) with two types of nodes, namely behavior nodes(N B ) and control nodes(N Q ). The behavior nodes, as the name suggests, indicate behavior execution, while the control nodes evaluate control conditions that lead to further behavior executions. Directed edges are allowed from behavior nodes to control nodes and vice versa. Also, a control node can have one, and only one, out going edge. Thus,

E(BCG) ⊂ N B (BCG) × N Q (BCG) ∪ N Q (BCG) × N B (BCG)
The execution of a behavior node, and similarly, evaluation in a control node, will be referred to as a firing. Node firings are facilitated by tokens that circulate in the queues of the BCG as shown in Figure 2. Each behavior node (shown by rounded edged box) in the BCG has one queue, for instance b1 queue for behavior node b 1 . All incoming edges to a behavior node represent the various writers to the queue. A behavior node blocks on an empty queue and fires if there is at least one token in its queue. Upon firing, one token is dequeued from the node's queue. The control node (shown by circular node), on the other hand, has as many queues as the number of incoming edges. For instance q n has k queues, one each for edges from b 1 through b k . A control node checks all its queues and blocks on empty queues.

If the queue is not empty, it dequeues a token from the queue and proceeds to check the next queue. The node fires after it has dequeued one token from each of its queues.

After firing, a behavior node generates as many tokens as its out-degree, and each token is written to the corresponding queue of the destination control node in a non-blocking fashion. Upon firing, the control node evaluates its condition. If the condition evaluates to TRUE, then a token is enqueued to the queue of the destination behavior node. The PCN is a directed graph which has three types of nodes, namely behavior nodes (N B ), condition nodes (N Q ) and variable nodes (N V ). The edges represent data dependencies in the model and are labeled using the port names involved in the dependency as shown in Figure 3. For instance, a directed edge from a behavior node b to a variable node v (shown by rectangular box), labeled p (written (b, v, p)) would mean that b writes to the storage indicated by v via its out-port p. Similarly, an edge from a variable node v to a behavior node b , labeled p (written (v , b , p )) would indicate that b reads variable v using its in port p . Note that for each variable v, there can be only one writer behavior (written as wr(v)). Control conditions also create data dependencies in the model. Thus, if a control condition q is a boolean function call q = f b (v 1 , v 2 , ..., v n ), then the node representing q has a directed edge from all the n variable nodes v 1 thorough v n .

Deriving BCG and PCN from SLDL models

BCG and PCN are powerful enough to represent a model's execution trace at the granularity level of leaf behaviors. However, they lack the concept of hierarchy that most SLDLs have. Also, BCG does not have different constructs for sequential and concurrent execution. Concurrency is realized simply by orthogonality of the behavior nodes. We will now show how a model written in a SLDL can be abstracted into a BCG, PCN pair.

The control flow between behaviors is typically expressed using switch-case or goto constructs in SLDL. A simple pseudo code example for a hierarchical behavior b is as follows Due to their rendezvous semantics, channels in SLDLs imply control flow dependencies between communicating behaviors. Figure 5 demonstrates this control dependency extraction from channels. Recall our assumption that the SLDL model has channel transactions only between identity behaviors. The synchronization properties of the SLDL channel would ensure that any behavior following the sender identity behavior would not execute until the receiver identity behavior has executed, and vice versa. If we were to optimize away the channel to reveal the control dependencies, the result will be as shown in figure 5. Note that the channel also results in the edge (e, e ) in the PCN.

Equivalence checking of SL models

In this section we present methods for automatically checking if two models, each represented by a BCG, PCN pair, are functionally equivalent. We define a notion of equivalence and rules for reducing the graphs to an equivalent normal form. If the normal forms for two models are identical, then they are functionally equivalent.

Notion of Functional Equivalence

Our notion of functional equivalence is based on the trace of values that the variables hold during model execution. In particular, we are interested in the variables that are written to by non-identity behaviors. We will refer to such variables as observed variables. The reasoning is that variables that are connected to the output ports of identity behaviors are simply a copy of another variable. Informally speaking, we consider two models to be functionally equivalent, if they have identical observed variables and the trace of values assumed by those variables during model execution is identical, given the same initial assignment. The formal notion of equivalence is as follows.

Given a model M, let I(M) be the initial assignment of observed variables in M. Let

Graph reduction

Our goal is to eliminate identity behavior nodes and redundant dependencies from the BCG and PCN, as the model is reduced to its normal form. Redundant dependencies include control dependencies that do not influence the value trace of the observed variables or set of dependencies that may be replaced by a smaller set.

Identity Elimination

The identity behavior, by definition, does not perform any computation. Hence, we may remove the identity behaviors from BCG and PCN, while making appropriate changes to the variable dependencies. The simple example illustrated in figure 6(b) shows parts of the BCG and PCN involving an identity behavior e. In the BCG, e is part of the control path from b 1 to b 2 . It must be noted that there are no other edges to either e or the control nodes q 1 and q 2 . As per the semantics of BCG, we can eliminate e by merging the control nodes q 1 and q 2 as shown for the BCG in figure 6(b). Note that in both the models, b 2 will execute after b 1 if both control conditions q 1 and q 2 evaluate to TRUE. Hence, the elimination of e leads to the merging of nodes q 1 and q 2 to form the new control node labeled as q 1 ∧ q 2 (ANDing of the boolean variables q 1 and q 2 ). However, it must be noted that as a result of elimination of e, the variable that e was writing to, also becomes invalid. This variable v 2 is shown in the PCN in figure 6(a). Now, variable v 2 is simply a copy of v 1 , by definition of the identity behavior. Therefore, all dependencies on v 2 , including in-port connections for behaviors and parameters for control conditions, must be replaced by dependencies on v 1 . The elimination of e from the original model results in the PCN shown in figure 6(b). This simple example of identity elimination shows how the reduction rule works in principle. We now present the general definition of the rule.

Identity Elimination Rule: Given a model M, let e ∈ N B (M) be an identity behavior. Let M' be the model resulting from elimination of e. Let there be m edges to e from control nodes q 1 through q m in BCG(M). Also, let there be n edges from e to control nodes labeled q 1 through q n in BCG. Now, ∀i, j, s.t.1 ≤ i ≤ m, 1 ≤ j ≤ n In BCG(M), q i has in-degree l(i) and q j has in-degree k( j) + 1. Let, (x i 1 , q i ), (x i 2 , q i ), ..., (x i l(i) , q i ) ∈ E(BCG(M)), and (e, q j ), (y j 1 , q j ), ..., (y j k( j) , q j ) ∈ E(BCG) Also, let (q j , z j ) ∈ E(BCG). After, elimination of e, the merger of control nodes would result in m × n new control nodes. Therefore, ∀i, j, s.t.

1 ≤ i ≤ m, 1 ≤ j ≤ n q i ∧ q j : x i 1 &...&x i l(i) &y j 1 &...&y j k( j) ; z j ∈ BCG(M )
In the PCN, if (e , e), (e, v, out) ∈ PCN(M), e ∈ B I , then

PCN(M ) = (PCN(M) -(e , e)) ∪ (e , v, out). If (v, e, in), (e, v , out) ∈ PCN(M), then ∀x, s.t.(v , x, p) ∈ PCN(M) PCN(M ) = (PCN(M) -(v , x, p)) ∪ (v, x, p).

Redundant control dependency elimination

In order to eliminate spurious edges in a BCG, we first need a control dependence analysis. Given model M, let y ∈ N B (BCG(M)), x ∈ N(BCG(M)). If during any execution of M, y always fires at least once before and at least once between every firing of x, then we define y to be a dominator of x. The set of dominator nodes for x will be represented by dom(x, M). The set dom(x, M) can be defined inductively as follows

1. If x ∈ N B (BCG), then dom(x, M) = dom(x, M) ∪ T (q,x)∈E(BCG(M)) {y : y ∈ dom(q, M)} 2. If x ∈ N Q (BCG), then dom(x, M) = dom(x, M) ∪ S (b,x)∈E(BCG(M)) {b ∪ {y : y ∈ dom(b, M)}} Given q ∈ N Q (BCG(M)). Let b 1 , b 2 ∈ N B (BCG) and (b 1 , q), (b 2 , q) ∈ E(BCG)
Thus b 1 and b 2 must fire for q to fire.If we can show that b 1 ∈ dom(b 2 , M) then the edge (b 1 , q) can be eliminated from the BCG. This is because, upon execution of b 1 , a token will be enqueued in the queue corresponding to (b 1 , q). Now, if b 2 executes, we know that b 1 has already executed and enqueued the relevant token. The node q will dequeue this token from b 1 and will wait for a token from b 2 . Hence, a token from b 2 means that b 1 must already have a token sent to q. If we remove edge (b 1 , q), while keeping edge (b 2 , q), the order of firings in BCG would not change.

Control Dependency Elimination Rule

: Given model M, let q ∈ N Q (BCG(M)). If ∃b 1 , b 2 ∈ N B (BCG(M)), s.t. b 1 ∈ dom(b 2 , M) and (b 1 , q), (b 2 , q) ∈ E(BCG(M)), then E(BCG(M)) = E(BCG(M)) -(b 1 , q).

Control Relaxation

Given model M, let (b 2 , q 2 ), (q 2 , b 3 ) ∈ BCG(M). If there is no data dependency between b 2 and b 3 and between b 2 and q 2 , then changing the order of firing between b 2 and q 2 , or b 2 and b 3 would not change the value trace for any variable in M. Therefore, the artificial control dependency from b 2 to q 2 may be removed, as illustrated in figure 7. However, the rule applies only if the nodes q 1 and b 2 must have an in-degree of 1, while the node b 3 has an out-degree of 1. With these restrictions, dom(b

2 , M) = b 1 ∪ dom(b 1 , M).
Thus, firing of b 1 will enqueue a token on the queue for b 3 if q 2 is TRUE. Also, the token released by firing of b 2 must be enqueued to q 3 if the edge (b 2 , q 2 ) is to be removed. Hence, the transformation illustrated in figure 7 is functionally correct under the given restrictions.

Testing functional equivalence

In order to validate functional equivalence of M and M', we convert their BCG and PCN to the normal form. The normal form of M is derived by iteratively applying the reduction rules to the BCG(M), PCN(M) pair until none of the rules is applicable anymore. The resulting normal form graphs are represented by NBCG(M) and NPCN(M). Similarly, we derive the normal form graphs for M'. If NBCG(M) is identical to NBCG(M') and NPCN(M) is identical to NPCN(M'), then M is equivalent to M'. This follows from transitivity of the equivalence relation and the functionality preserving nature of the reduction rules. Since, the static scheduling process (Section 2) changes only the control dependencies, the leaf level behaviors in both models should match. For lack of space, we could not present a walk through example of the normalization process. We refer the reader to [START_REF] Abdi | System Level Verification with Model Algebra[END_REF] for the same.

Experimental Results

A tool, consisting of two modules, was written in C++ for checking equivalence of scheduled and unscheduled SpecC models. The graph extractor module derives the BCG and PCN from a SpecC Model, while the Graph Reducer module used the rules in Section 4.2 to generate the normalized form BCG and PCN. An automatic static scheduler was used to create models for different serializations on HW PEs. Experiments for communication scheduling were performed by manual transformation of models.

The model used is a GSM voice codec application [START_REF] Gerstlauer | Design of a GSM Vocoder using SpecC Methodology[END_REF] for cellular phones. The unscheduled model consisted of 1273 lines of SpecC code, with 43 non-identity leaf level behaviors that were distributed on 3 PEs. The BCG and PCN extraction and reduction times were in the order of a few seconds on a 2 GHz PC running RedHat Linux OS as shown in Table 1. The type column indicates the type of scheduling performed; either computation serialization (serial) or communication scheduling (comm.). Communication scheduling was done on the serialized model. The extraction time also includes the time for dominator analysis of all the nodes in the BCG. As expected, extraction and reduction of models after communication scheduling took slightly longer due to extra control dependencies and extra control relaxation cycles needed for normalization. Comparison of normalized graphs took negligible time.

Conclusion and Future Work

We presented a technique to check the functional equivalence of system level models before and after the scheduling of behaviors in the architecture PEs. The main advantage of this technique is that the scheduled model does not require any functional simulation. On the flip side, the equivalence checker cannot handle run-time scheduling that adds an RTOS model, which cannot be resolved by the checker. However, this is only to be expected since dynamic scheduling requires analysis at a smaller granularity level than the leaf level behaviors, for instance interleaving of concurrent behaviors. In the future, we would like to extend our equivalence checker to validate more design steps like communication synthesis.

  Consider an unscheduled HW PE with two threads of execution. The first thread executes behavior b 1 followed by b 2 , while the second thread executes b 3 followed by b 4 . A possible serialization of the PE would sequentially execute the behaviors in the order {b 1 , b 3 , b 2 , b 4 }. Other schedules, that do not violate data dependencies, are also possible.

Figure 1 .

 1 Figure 1. Different communication schedules for transaction over channel c.

  (a), b 2 must wait until b 3 has completed and the transaction is performed. If b 3 takes a long time to execute, execution inside PE1 will stall, as it waits for the data transaction. Behavior b 2 may be scheduled before the transaction, if it has no data dependency on b 3 . The resulting schedule,shown in 1(b), optimizes timing.

Figure 2 .

 2 Figure 2. The firing semantics of BCG nodes

Figure 3 .

 3 Figure 3. Port connection network showing data dependencies

Figure 4 .

 4 Figure 4. BCGs for different hierarchical behavior compositions

Figure 5 .

 5 Figure 5. Effect of rendezvous channel on BCG and PCN

  ∀v ∈ N V (PCN(M)), ∃wr(v) ∈ N B (PCN(M)) Let d i , i > 0 be the value written to v after the i th execution of wr(v). Let d 0 be the initial assignment value of v. We define the ordered set τ(v, M, I(M)) = {d 0 , d 1 , d 2 , ...} We claim that two models M and M are equivalent iff ∀v, I(M) = I(M ) ⇒ τ(v, M, I(M)) = τ(v, M , I(M ))

Figure 6 .

 6 Figure 6. Parts of BCG and PCN before and after identity elimination

Figure 7 .

 7 Figure 7. Control relaxation for edge (b 2 , q 2 )

Figure 8 .

 8 Figure 8. Control relaxation for edge (b 2 , q 2 ) without in and out-degree restrictions

Table 1 . Performance of equivalence checker for different scheduling decisions

 1

	Sched. Type Extraction Time Reduction Time
	serial	2.12s	5.66s
	serial	2.11s	5.18s
	comm.	2.42s	7.11s
	comm.	2.83s	7.03s
	comm.	3.06s	9.02s

Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05) 1530-1591/05 $ 20.00 IEEE

Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05)


Shuqing Zhao
email: szhao@uci.edu

Daniel D Gajski
email: gajski@uci.edu

Defining an enhanced RTL Semantics

In this paper we formally define an enhanced RTL semantics. This is intended to elevate the RTL design abstraction level and help bridge the HDL semantic gap among synthesis, simulation and formal verification tools. We define the enhanced semantics based on a new RTL++ language that supports pipelined operations using a new pipelined register variable concept. The execution semantics of RTL++ is specified in a structural operational semantics style aimed to form the basis for related simulation and formal verification algorithm development. A RFSM model is defined to support natively the synthesis semantics of RTL++. We also present an example of extending Sys-temC to support the notion of pipelined register variable.

Introduction

In today's SoC era most of the new hardware block designs are still conducted at the register transfer level. Engineers first use hardware design language like Verilog or VHDL to model the RTL hardware components: control logic and datapath units such as multiplexers, registers, arithmetic units etc. Synthesis, simulation, and optionally formal verification tools are then used on this model to generate the hardware logic and verify its functional correctness. Often times this is a long and error-prone process that has been and continues to be the major bottleneck of SoC design productivity. One of the main source of the problem is always attributed to Verilog or VHDL. They were designed and well suited to support gate-level simulation details e.g. their delta cycle semantics guarantee that they can simulate the combinational logic behavior even if there are combinational feedback loop within the circuit. They do not support conveniently the true RTL semantics for synthesis, simulation and formal verification. Furthermore their semantics are not formally defined and even the IEEE stan-dard documents have ambiguities which led to incompatible simulation results among different vendors. In practice whatever coding style the dominant EDA tool accepts became the de facto standard for RTL semantics.

To alleviate this problem, many languages [START_REF]Accellera[END_REF][START_REF]Open SystemC Initiative[END_REF][START_REF] Gajski | SpecC: Specification Language and Methodology[END_REF], 3] and associated tools have been proposed and implemented in the industry and academia. However in our opinion some of these languages are not suited for RTL, some inherited the exact problems that exists in today's HDLs, and some are headed in a wrong direction [START_REF] Edwards | The challenges of hardware synthesis from c-like languages[END_REF]. We believe a study on the appropriate RTL semantics is necessary and could shed light on the design of the next generation HDLs by allowing precise specifications of intended program behavior and permitting proofs that a program does (or perhaps does not) meet its specification.

In Section 2 we review some of the related works that have been accomplished. We propose a new RTL++ language as our basis to discuss and describe the enhanced RTL semantics in Section 3. In Section 4 we present the formal execution semantics for RTL++ using structural operational semantics(SOS) [START_REF] Plotkin | A Structural Approach to Operational Semantics[END_REF] as the framework. In Section 5 we give the definition of a new model of computation called Register-transfer Finite State Machine (RFSM) as a platform to describe the synthesis semantics for RTL++. Section 6 shows an example to extend SystemC to support the key semantic enhancement. Section 7 concludes the paper and suggests the future research direction.

Related Work

There has been some effort attempted to define formal semantics for existing HDLs. The most relevant one is [START_REF] Gordon | Language independent rtl semantics[END_REF] in which Gordon defined a trace semantics model for Verilog synthesizable subset. Accellera made an effort in 2001 to standardize on RTL semantics [START_REF]Accellera[END_REF]. [START_REF] Zhao | Modeling a new rtl semantics in C++[END_REF] provides an implementation using a C++ library to model this proposed semantics. Zhu in [START_REF] Zhu | MetaRTL: Raising the abstraction level of RTL design[END_REF] defined a meta RTL language to enrich RTL data types. Another inspiration source has been from synchronous programming community who pioneered the synchrony concept which is also the assumption used in this paper. Esterel [START_REF] Berry | A hardware implementation of Pure Esterel[END_REF] is ideal for control-dominant application and has been adopted in control software domain while Lustre [START_REF] Halbwachs | Synchronous Programming of Reactive Systems[END_REF] has been largely applicable to digital signal processing software development. We believe a good RTL language should be simpler and more attuned for both control and data oriented application. Our goal is to provide a formal semantic framework to guide the related simulation, synthesis and formal verification tool. It is not our intention to invent yet another new HDL though we have not found an suitable language allowing us to define the RTL semantics we would like to propose. We also would like to stay language neutral to avoid inheriting something without knowing the consequence. Therefore we start by defining an new RTL language called RTL++ that will serve the purpose as an experimental ground for studying the new semantics we proposed. The new features in the RTL++ language could help inspire designs of future HDLs or extensions of existing languages. In Section 6 we showed an example of extending SystemC to support a feature in our RTL++.

The RTL++ language

A good way to introduce a new language is by example. Listing 1 presents an RTL++ program example which we adapted from [START_REF] Paulin | Force-directed scheduling in automated data path synthesis[END_REF]. This example demonstrates most of the language constructs needed for specifying a RTL block. Similar to HDLs like Verilog module is the basic compositional unit for building structural hierarchy. A system modeled in RTL++ is composed of a list of modules that runs in parallel while communicating through their ports connected by wires. Each module is synchronous to a clock. The whole system can be seen as a globally asynchronous but locally synchronous one which suffice to represent most of the hardware systems. The detailed communication mechanism is outside the scope of this paper where we focus on the behavior of each individual module. The module behavior is specified with a while true loop statement. You can see that the language is mainly an imperative language which is familiar to most engineers. In contrast to the current practice of describing a FSM in a HDL case statement that explicitly branches to executing different actions block based on specific state values, RTL++ promotes the usage of so-called implicit state-machine style. A sequential block of program is divided into cycle block using a cycle delimiterwait statement in RTL++. Each cycle block implies a distinct program control flow state.

We presents in the following sections the main ingredients in RTL++ that distinguishes it from other HDLs. Many topics of importance are omitted. These include data structures, data types, functions and procedures etc. For instance RTL++ only uses integer and bool as the only data types accepted for boolean and arithmetic operations. In this paper we focus on the execution flow control aspect of a RTL program.

Variables

To avoid the shortcomings in other HDLs such as register inferencing ambiguities, a clear semantics for synthesis is the number one objective for the design of RTL++. We define respectively three types of variables: wire, register, and pipelined register intended to be mapped exactly to the same type of objects in the synthesized hardware logic. They all associate with the module clock. We present their informal semantics as follows.

Q Q' D Q Q' D Q Q' D Q Q' D Figure 1.
Using back-to-back shift registers to represent pipelined operation

Wire

Wire variable is used to store intermediate computation results within the cycle block boundary. Once assigned a new value it is immediately available to all readers. This is in a sense similar to VHDL variable from which it nevertheless differs in an aspect that the storage of a wire variable is volatile. The variable lives only in its definition cycle block, where there is an assignment with the variable being on the left hand side. The variable dies immediately once it passes the cycle block boundary delimited by wait statement. The wire variable can be mapped to the combinational output of a function in hardware logic.

Register

Register variable is used to store computation results across cycle block boundaries. It uses essentially two buffers to hold its current value and its new value. When a value is assigned to the register variable, the value is stored in the new value buffer first. Only in the beginning of next clock cycle, its current value will be updated to the saved new value buffer. Unlike VHDL signal or Verilog reg which could be synthesized to registers or wires depending on how they are inferred, a register variable in RTL++ language corresponds to a specific physical register (flip-flop) in hardware.

Pipelined Register

It is very awkward to capture in RTL HDL the design intent of pipelined operations which are very common in RTL design. We introduce a pipelined register variable in RTL++ to facilitate this purpose. As illustrated in Figure 1 a backto-back shift register array is used to represent the effect of an pipelined operation. The depth of the array is equal to the number of stages of the pipeline. With respect to the pipeline output, it is an equivalent abstraction -the same input sequences produce the same output sequence. (This is under the normal assumption that the intermediate pipeline stage registers are not used directly for com-putation.) The introduction of this new type of variable in RTL++ (as the name suggests) help raise the RTL abstraction level which usually deals only with computations happening in one clock cycle. This abstraction works for modeling and simulation obviously. To be synthesizable it relies on the availability of pipeline retiming tools such as Synopsys Design Compiler [13] which has a behavioral retiming feature that can essentially find an optimal boundary in the combinational logic to insert pipeline stage registers. Also as exemplified in Listing 1 pipelined register variable can be used on module ports to account for interconnect delay that has become dominant for deep submicron chip design.

Abstract Syntax

We define the RTL++ language with an abstract syntax which lets us focus on the structures of the program with semantic significance rather than worrying about parsing correctly the lexical token. The syntax can be captured in a BNF-like notation as follows:

a ::= n | v | a 1 aop a 2 (Arith. Expression) b ::= true | false | a 1 bop a a 2 (Boolean Expression) | bop b1 b | b 1 bop b2 b 2 S ::= v = a (Assignments) | wait (Cycling) | wait until b (Conditional Cycling) | nop (No Operation) | S 1 ; S 2 (Sequencing) | if b then S 1 else S 2 (Branching) | while b do S (Loop)
Where the various syntactic categories and meta-variables that are used to range over constructs of each category: [ass]

v = a, s s[v → v.write(A[a]s)] [nop] nop, s s [wait] wait, s (V → V.update()) [seq partial ] S1, s S1 , s S1; S2, s S1 ; S2, s [seq complete ] S1, s s S1; S2, s S2, s [i f t ] if b then S1 else S2, s S1, s if B[b]s = true [i f f ] if b then S1 else S2, s S1, s if B[b]s = false [while] while b do S,

Formal Execution Semantics of RTL++

We define execution semantics of RTL++ using Plotkinstyle structural operational semantics (SOS) as our framework. The idea is to explicitly describe how RTL++ programs compute in stepwise fashion and the possible statetransformation they perform. SOS uses a transition system which is a structure Γ, where Γ is a set of configurations and ⊆ Γ × Γ is the transition relation.

In the context of RTL++, the configuration is a pair S, s where S is the RTL++ syntactic constructs defined in Section 3.2, s is the value(state) of all RTL++ variables including wires, registers, and pipelined registers. The transition relation has two forms: S, s S , s where S execution is not completed and results in an intermediate configuration S or S, s v in which S has terminated and the terminal state is s . The specific configuration transitions for a specific RTL++ program are obtained inductively from a collection of so-called transition rules of the form premises conclusion . If premise of a rule is empty it is called an axiom. The complete definition of transition relation for RTL++ is given in Table 1.

In the assignment axiom [ass] we use A[a]s and B[b]

s to denote the semantic functions for arithmetic expression and boolean expression respectively. Semantic function takes a syntactic entity as argument and returns its meaning. We will only define semantics of the variables and omit the rest of the detail of the expression semantics of RTL++. We uniformly define any of the three types of variables as a vector υ = {υ 0 , ..., υ n } where for wire, n = 0; for regular registers, n = 1; for pipelined registers n is the total number of pipeline stages. We can define three variable functions as

I R O d fo fs PC fr Q Q' D Q Q' D Q Q' D Q Q' D Q Q' D Q Q' D Q Q' D Figure 2. Register-transfer Finite State Ma- chine follows: read() = υ n write(x) = {x, υ 1 , ..., υ n } update() = {unde f , υ 0 , ..., υ n-1 }

With these three functions defined, we have semantic function A[v]s = A[v.read()]s which forms the basis of A[a]s. Axiom [ass]

indicates that an assignment to a variable is equal to a calling to its write() function.

Axiom [nop] obviously does not have any effect on the state s at all. Axiom [wait] essentially expresses the update of all variables. The sequential composition rules [seq partial ] and [seq complete ] express that to execute S 1 ; S 2 in state s we first execute S 1 one step from s. Only when all the statements contained in S 1 has been completed S 2 can be executed. Axioms [i f t ] and [i f f ] shows that the first step in executing a branch statement is to perform the test and to select the appropriate branch. The [while] rule shows that the first step in the execution of the while-construct is to unfold it one level, that is to rewrite it as a branch statement. The test will therefore be performed in the second step of the execution (where one of the axioms

[i f t ] or [i f f ] is applied).
The last rule [wait until ] shows that a wait until statement can actually be translated into an equivalent while statement.

Synthesis Semantics: Register-transfer Finite State Machine

RTL++ has very clear synthesis semantics. All constructs of the program can be easily translated onto a hard-ware model of computation while preserving its execution semantics. A commonly used model of computation for RTL design is FSMD [START_REF] Gajski | High-Level Synthesis: Introduction to Chip and System Design[END_REF]. However it does not support the pipelined operation semantics directly. Here we define a new model called Register-transfer Finite State Machine (RFSM) that natively supports the proposed RTL++ semantics. Figure 2 • R is the set of register (memory elements) that store the datapath states. Its initial set R 0 = {unde f }.

R = {R i |i > 0 and i ≤ n}
where n is the total number of registers (pipelined registers are grouped as one), and

∀R i ∈ R, R i = (r i [1], r i [2], ..., r i [m i ])
where m is the number of pipeline stages of R i , and we define the first stage register set

R[1] = {r i [1]|i > 0 and i ≤ n}
and the last stage register set

R[m] = {r i [m i ]|i > 0 and i ≤ n}
• I is a finite set of input symbols.

• O is a finite set of output symbols.

• f s : PC × R × I → PC is the state transition function.

• f r : PC × R[m] × I → R[1] ∀R i , ∀ k > 1 and k ≤ m i , r i [k] = r i [k -1] is the register update function. • f o : PC × R → O is the output function.
Each cycle block of a RTL++ program can be labeled with a unique natural number starting with the first cycle block being 0. These cycle block labels corresponds directly into PC state register of RFSM. Synthesis tool has the freedom to re-encode the state value assignment using such as one-hot or one-cold encoding. The register and pipelined register variables also have a one-to-one mapping from their declarations in the program to the datapath register set R of RFSM. These hardware physical registers definitely can be shared among register variables having non-overlap life time [START_REF] Kurdahi | Real: A program for register allocation[END_REF]. This topic is out of the scope of this paper. The rest of the RTL++ assignment statements can be handled by synthesis tool using allocation and binding algorithm [START_REF] Gajski | High-Level Synthesis: Introduction to Chip and System Design[END_REF] to generate the combinational logic and the connections.

Adding RTL++ Semantics in SystemC

Because formal semantics can help to clarify the ambiguities in the language design by allowing us to make rigorous statements about properties of programs and the interactions between program constructs, it provides a firm foundation for many applications related to programming languages. In this section we show an example of extending SystemC language [START_REF]Open SystemC Initiative[END_REF] under the guidance of the new RTL++ semantics described above. More specifically we implement the key construct pipelined register variable of RTL++ as shown in Listing 2. It has the form of a new C++ class template reg T, num stages .

Listing 3 provides an simple design example using this newly defined pipelined register variable type reg T, num stages . This is an example adapted from the pipe example bundled in OSCI SystemC software package. The original example describes a 3-stage pipeline RTL design using a coding style that captures computation for each stage in a separate module and connects those modules back-to-back. We show that using the new semantics the same design intention can be kept faithfully with the output equivalence maintained on a per-cycle basis. The new code yields the cycle-to-cycle equivalent simulation result as the original OSCI example while clearly having several advantages. It has 60% less lines of code (˜110 comparing to

Listing 3. Pipelined Register Variable Usage Example

the original ˜330) and is more adaptable to design changes which happens all the time in practice. For example changing the number of stages from 3 to 4 for this example just need one change of the macro NUM STAGES in our code.

Conclusions and Future directions

In this paper we have proposed an enhanced semantics that supports pipelined operation. Due to the lack of suitable HDL to use to define our proposed semantics, we have also defined the abstract syntax for RTL++ language intended to capture the minimal but necessary set of ingredients for RTL design modeling rather than designing a perfect language. For example, wait statement in RTL++ only supports one clock cycle advancement. In a real world language, to help user avoid repeating wait for multiple times one will certainly add another wait[n] statement for coding convenience and readability improvement purpose. The execution semantics of RTL++ is documented in the intuitive and simple structural operational semantics notations. We also define a formal RFSM model for us to discuss the synthesis semantics of RTL++. These contributions form the unambiguous basis for future algorithm and tool developments in the area of RTL synthesis, formal verification and simulation. We have shown one example of extending Sys-temC to support the pipelined register variable concept in RTL++ semantics. Our immediate future research direction is to study the communication semantics between modules to investigate whether a higher level abstraction is needed for RTL.

n

  will range over numerals, w will range over wires, r will range over registers, p will range over pipelined registers, v will range over all three types of variables, v = w ∪ r ∪ p a will range over arithmetic expressions, b will range over boolean expressions, S will range over statements, and aop ∈ {+, -, * , ...} a finite set of integer binary operators, bop a ∈ {=,<,>,...} a finite set of binary integer boolean operators, bop b1 ∈ {not, ...} a finite set of unary boolean operators, bop b2 ∈ {and, or, ...} a finite set of binary boolean operators.

  illustrates the model from a structural hardware logic point of view. Formally a RFSM is a 7-tuple PC, R, I, O, f s , f r , f o where • PC ⊂ Z * is a finite set of non-negative integers which essentially represent the control states (program counter) of the program. Its initial set PC 0 = {0}.

t e m p

  l a t e < c l a s s T , c o n s t i n t n u m s t a g e s > c l a s s r e g : s c m o d u l e { p u b l i c : 25 s c i n < bool > c l k ; / / c l o c k SC HAS PROCESS ( r e g ) ; r e g ( sc module name name ) 30 : sc m o d u l e ( name ) { SC METHOD ( p i p e ) ; s e n s i t i v e p o s << c l k ; d o n t i n i t i a l i z e ( ) ; } ; 35 void w r i t e ( T c ) { n e x t = c ; } T r e a d ( ) { r e t u r n d a t a [ n u m s t a g e s -1 ] ; } 40 p r i v a t e : T d a t

# d e f

  i n e NUM STAGES 3 s t r u c t a l g s t a g e s : sc m o d u l e { double q u o t ; w h i l e ( t r u e ) { a = i n 1 . r e a d ( ) ; b = i n 2 . r e a d ( ) ; sum = a + b ; d i f f = ab ; i f ( diff == 0 ) d i f f = 5 . 0 ; 75 prod = sum * d i f f ; q u o t = sum / d i f f ; c = ( prod>0 && quot >0)? pow ( prod , q u o t ) : 0 . ; 80 ( * p o w r r e g ) . w r i t e ( c ) ; powr . w r i t e ( ( * p o w r reg ) . r e a d ( ) ) ; w a i t ( ) ; } ; }

u t wire i n t e g e r Uinp , i n p u t wire i n t e g e r Ap , i n p u t wire i n t e g e r DXp , output r e g i s t e r i n t e g e r Xoutp , output r e g i s t e r i n t e g e r Youtp , output r e g i s t e r i n t e g e r Uoutp , c l o c k c l k ) ; r e g i s t e r i n t e g e r

	module d i f f e q (
	i n p u t wire bool s t a r t ,
	output p r e g i s t e r <2> bool ready ,
	i n p u t wire bool r e s e t ,
	i n p u t wire i n t e g e r Xinp ,
	i n p u t wire i n t e g e r Yinp ,
	i n p x , y , u , a , dx ;
	r e g i s t e r i n t e g e r t1 , t3 , t4 , t 5 ;
	p r e g i s t e r <2> i n t e g e r t 2 ; / / p a t h t o t 2 i s p i p e l i n e d
	w h i l e t r u e {
	wait u n t i l ( s t a r t == 1 ) ;
	r e a d y = 0 ;
	x = Xinp ; y = Yinp ; u = Uinp ;
	a = Ap ; dx = DXp ;
	wait ;
	w h i l e ( x < a ) {
	t 1 = u * dx ;
	t 2 = 3 * x ;	/ / s t a r t 1 s t p i p e l i n e d op
	wait ;
	t 2 = 3 * y ;	/ / s t a r t 2nd p i p e l i n e d op
	x = x + dx ;
	wait ;
	t 4 = t 1 * t 2 ;	/ / t 2 from 1 s t p i p e l i n e d op
	y = y + t1 ;
	wait ;
	t 5 = dx * t 2 ;	/ / t 2 from 2 nd p i p e l i n e d op
	wait ;
	u = u -t 4 ;
	wait ;
	u = u -t 5 ;
	wait ;
	}
	Xoutp = x ; Youtp = y ; Uoutp = u ; r e a d y = 1 ;
	}

endmodule Listing 1. RTL++ code example for differential equation y + 3xy + 3y = 0 solver

Table 1 . Operational Semantics of RTL++

 1

		s
		if b then (S; while b do S) else nop, s
	[wait until ]	wait until b, s
		while not b do wait, s

SystemC Implementation of Pipelined Register Variable

		a [ n u m s t a g e s ] ;
		T next ;
	45	void p i p e ( ) {
		/ / s h i f t i n g t h e p i p e
		f o r ( i n t i = n u m s t a g e s -1 ; i > 0 ; i --) {
		d a t a [ i ] = d a t a [ i -1 ] ;
		} ;
	50	d a t a [ 0 ] = n e x t ;
		}
	} ;
		Listing 2.

Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05) 1530-1591/05 $ 20.00 IEEE

Proceedings of the Design, Automation and Test in Europe Conference and Exhibition (DATE'05)