Theorem Proving Guided Development of Formal Assertions in a Resource-Constrained Scheduler for High-Level Synthesis.
This paper presents a formal specification and a proof of correctness for the widely-used Force-Directed List Scheduling (FDLS) algorithm for resource-constrained scheduling of data flow graphs in high-level synthesis systems. The proof effort is conducted using a higher-order logic theorem prover. During the proof effort many interesting properties of the FDLS algorithm are discovered. These properties are formally stated and proved in a higher-order logic theorem proving environment. These properties constitute a detailed set of formal assertions and invariants that should hold at various steps in the FDLS algorithm. They are then inserted as programming assertions in the implementation of the FDLS algorithm in a production-strength high-level synthesis system. When turned on, the programming assertions (1) certify whether a specific run of the FDLS algorithm produced correct schedules and, (2) in the event of failure, help discover and isolate programming errors in the FDLS implementation.We present a detailed example and several experiments to demonstrate the effectiveness of these assertions in discovering and isolating errors. Based on this experience, we discuss the role of the formal theorem proving exercise in developing a useful set of assertions for embedding in the scheduler code and argue that in the absence of such a formal proof checking effort, discovering such a useful set of assertions would have been an arduous if not impossible task.
and often expensive ramifications since as they could lead to the synthesis and finally fabrication of incorrect designs.
Therefore, reliability and correctness of these tools have become important issues which need to be addressed.
Simulation has traditionally been used to check for correct operations of digital systems. However, with increase
in system functionality and complexity, this is proving to be inadequate due to the computational demands on the
task involved. In formal verification, correctness is determined independent of the input values to the design. Thus,
exhaustive validation is implicit. Formal verification approaches like theorem proving and model checking techniques
are powerful techniques employed to formally verify RTL designs. Both support use of formal specification languages
with rigorous semantics and formal proof methods that support mechanization. An RTL design synthesized from a
real-world specification often comprises a large state space. This makes formal verification of the RTL design as a
post-design activity rather tedious, often resulting in a tremendous strain on the verification tool and the verification
engineer. In a model checking environment, increase in RTL design size results in a combinatorial explosion in the
number of global states. Theorem proving is not limited by design size but tends to be extremely tedious requiring a lot
of time and user interaction. Moreover in the synthesis of an RTL design from high-level synthesis, the information on
how the specification was refined into an implementation is no longer available at the end of synthesis. This compounds
the problems faced by formal verification techniques further.
Several researchers have proposed alternatives to the post-synthesis verification effort. The idea of formal hardware
synthesis was originally proposed by Johnson [19]. He presented a technique [19] for deriving synchronous-system
descriptions from recursive function definitions, using correctness preserving functional algebraic transformations.
Since then several techniques have been proposed that attempt to guarantee "correct by construction" synthesized
designs, eliminating the need for a separate verification stage [4, 7, 11, 20]. These techniques employ formal logic
and require the user to closely interact with the synthesis tool as the specification is refined into an implementation.
Eisenbiegler et al. [1] introduced a general scheme for formally embedding high level synthesis algorithms in HOL [6].
High Level Synthesis is performed by a sequence of logical transformations. The input specification (data flow graph)
is fed both to the synthesis system and to the theorem prover. After each stage in synthesis, the control information
is passed on to the HOL environment, where the corresponding transformation is executed within the logic. If the
control information generated by the external system is faulty, the corresponding transformation cannot be performed
within the logic and an exception is raised. This approach is probably the only reported attempt at formalizing a
conventional synthesis process. However, the methodology requires a tight integration between the synthesis system
and a formal verification environment.
Formal Verification of RTL designs generated in a conventional high-level synthesis environment has long been a
challenge. In HLS [3, 8, 14], a behavioral specification goes through a series of transformations leading finally to an
design that meets a set of performance goals. A HLS synthesis flow is usually comprised of the following four
main stages:
ffl The Scheduling Stage: This stage specifies the partial order between the operations in the input specification.
Each data and control operation is bound to a time step. The operations may also be mapped to functional
units in a component library during this stage.
ffl The Register Allocation Stage: Carriers in the specification, and those additionally identified during the scheduling
phase are mapped to physical registers.
ffl The Binding Stage: Interconnection among the different components in the design is established.
ffl The Control Generation Stage: A controller is generated to sequence the operations in the RTL design.
We propose a Formal Assertions approach to building a formal high-level synthesis System. The approach works under
the premise that, if each stage in a synthesis system, like scheduling, register optimization, interconnect optimization
etc. can be verified to perform correct transformations on its input, then by compositionality, we can assert that
the resulting RTL design is equivalent to its input specification. This divide and conquer approach to verification
is a powerful technique and has been well researched in the area of transformation-based synthesis systems but the
algorithmic complexities involved in conventional HLS renders the verification process in a formal proof system rather
complex. Our approach attempts to bypass this problem. The formal assertions approach is not limited by the state
space of the design since we never attempt to verify the RTL design directly, only the changes made to it during the
process of synthesis.
In this paper, we look closely at an important stage in high-level synthesis, namely the Scheduling stage. We will
illustrate our approach by verifying an implementation of this stage in a conventional HLS system. The formalism
achieved in the context of a theorem proving exercise is embedded within the synthesis domain. An appealing aspect
of our approach is that the verification exercise is conducted within the framework of a conventional synthesis system
thus avoiding the complexities involved in integrating the synthesis system with a verification tool. By seamlessly
integrating with conventional automatic synthesis, the formal assertions approach introduces a formalism into the
synthesis sub-tasks which is transparent to the designer.
Section 2 gives an outline of our verification approach. In Section 3, we will introduce the verification problem
and present the core set of correctness conditions. In Section 4, we will present a well known scheduling algorithm
and formulate the conditions for our verification approach and discuss the proof strategy. Section 5 discusses the
applicability of the proof exercise within the context of a high level synthesis environment. Results are presented in
Section 7, scope of our verification approach is discussed in Section 8 and we will make some conclusions in Section 9.
Assertions based Verification - An Outline
Our verification approach is based on higher-order logic theorem proving leading to formal assertions in program code.
Each stage in high-level synthesis is well understood and its scope well-defined. The input specification as it passes
through each stage in synthesis, undergoes very specific modifications that bring it closer to the final RTL design. It
is therefore possible to capture the specification of each stage in synthesis in a precise manner.
2.1 Verification Outline
ffl Characterization: Identify a base specification model for each synthesis task. This model should cover all aspects
of correctness for the particular synthesis task. With each task in synthesis being so well-defined, the base
specification model is usually a tight set of correctness properties that completely characterizes the synthesis
task.
ffl Formalization: The specification model is now formalized as a collection of theorems in a higher-order logic
theorem proving environment: these form the base formal assertions. An algorithm is chosen to realize the
corresponding synthesis task and is described in the same formal environment.
ffl Verification: The formal description of the algorithm is verified against the theorems that characterize the base
specification model. Inconsistencies in the base model are identified during the verification exercise. Further,
the model is enhanced with several additional formal assertions derived during verification The formal assertions
now represent the invariants in the algorithm.
ffl Formal Assertions Embedding:. Develop a software implementation of the algorithm that was formally verified
in the previous stage. Embed the much enhanced and formally verified set of formal assertions within this
software implementation as program assertions. During synthesis, the implementation of each task is continually
evaluated against the specification model specified by these assertions and any design error during synthesis can
be detected. A high-level synthesis system wherein each task is embedded with its formal specification model
constitutes a Formal Synthesis System that strives to generate error-free RTL designs.
In the rest of the paper, we will explain our verification approach in the context of the scheduling task in high-level
synthesis.
Scheduling Task and Base Specification Model
The Scheduling task is one of the most crucial steps in high-level synthesis since it directly impacts the tradeoff
between design cost and performance. It maps each operation in the specification to a time step given constraints
imposed by the input specification and the user. These time steps correspond to clock cycles in the RTL design.
Scheduling can be done either under resource constraints (design area and component library) or under time constraints
(design speed). In this paper we illustrate our verification technique on a resource-constrained scheduling algorithm.
The scheduling stage views the input specification as a dependency graph. A dependency graph is a directed acyclic
graph (DAG) where each vertex is associated with an operation in the specification and the presence of an edge between
any two vertices in the graph denotes a data dependency or control dependency between the operations associated
with the vertices. Data dependencies capture the operation of the assignment statements in the input specifications
and hence their order of execution. Control dependencies make up the semantics of conditional and loop constructs.
Consider a simple dependency graph as shown in Figure 1. OP1;OP2;OP3 and OP4 denote the four vertices in the
graph. The operation type is specified inside each vertex. The primary inputs feed OP1; OP2 and OP 3. The edges
denote data dependencies and specify the order in which the operations should be executed in the final RTL design.
In addition to a dependency graph, the scheduling stage expects a valid module bag of library components that have
enough functionality to fully implement all operations in the specification. This module bag is typically generated in
the module generation stage that usually precedes scheduling in the synthesis flow.
3.1 Base Specification Model for Scheduling Task
Let N be the set of operation nodes and E be the set of dependency edges in the dependency graph. Let R bag denote
the bag of resources available and sched func be the schedule function that maps every operation in the graph to a
positive time step. Given this, the following three correctness conditions capture the base specification model:
1. Existence: The schedule function maps each and every operation in the input specification to a positive time
step.
OP2
OP3
OP4

Figure

1: A Simple Dependency Graph
2. Dependency Preserved: If a directed edge exists between any two operations in the graph, the operation at
the source of the edge will be scheduled at an earlier time step than the operation at its destination.
sched sched
Thus, in Figure 1, OP2 should always be scheduled before OP 4.
3. Resource Sufficiency: Operations mapped to the same time step must satisfy resource constraints 1 . Let T
be the set of all time steps to which operations in the graph are scheduled. Let OTS be the set of all operator
types in the graph and op map be the function that maps an operator type to a set of operations at time step
n. Let Rmap map an operator type to all the modules in R bag that can implement the operator type.
The two "+" operations, OP1 and OP2 in the dependency graph shown in Figure 1 can be scheduled in the
same time step provided R bag has at least two adders.
Every correct schedule should satisfy the above three correctness conditions 2 . These properties are far removed from
any algorithmic details and so hold for the entire class of resource-constrained scheduling algorithms.
In our treatment of the scheduling stage in this paper, we have concentrated on the primary function of the scheduler:
time-stamping the operations in the input specification. In most high-level synthesis systems, in addition to this
primary function, the scheduling stage also performs functional unit allocation, either concurrently or in a stepwise
refinement manner. Our methodology can be quite easily extended to reflect any additional tasks performed by the
scheduling stage. For the sake of this paper, we will assume that the scheduling stage does not support multi-cycling
or chaining of operations. Therefore, an operation in the input specification consumes exactly one time step. We will
further assume that the high-level synthesis system generates non-pipelined RTL designs and therefore the scheduling
task does not have to consider structural pipelining or functional pipelining issues. Additional correctness conditions
can be easily included in the base specification model in order to reflect any or all of these extensions to the primary
scheduling task.
We assume that there is at least one resource in R bag that can implement an operation in the graph.
2 We can conceivablyadd a 4th condition that captures a desirable property in a scheduler: a tightness property that states that every time
step between 1 and the maximum time step for the scheduled graph must have at least one operation scheduled. Let Tmax be the maximum
time step to which nodes in the input graph are scheduled. We can state this property as
In the following sections, we will discuss our verification strategy by closely looking at a scheduling algorithm used
widely in high-level synthesis: the Force Directed List Scheduling algorithm proposed by Paulin and Knight [13].
Theory - Formal Verification of a Scheduling Algorithm
Force Directed List Scheduling (FDLS) [13] is a resource-constrained scheduling algorithm. It is a popular scheduling
technique, widely used in many synthesis tools that exist in the current literature. The FDLS algorithm shown in

Figure

2, is based on the classic list scheduling algorithm [16]. It uses a global measure of concurrency throughout the
scheduling process [13].
4.1 Overview of Force Directed List Scheduling Algorithm
All operations in the dependency graph are sorted in a topological order based on the control and data dependencies.
In each time step, T step a list of operations that are ready to be scheduled, called the ready list, L ready is formed.
This includes all operations whose predecessor operations have been scheduled. As long as the resource bag, R bag is
insufficient to schedule the operations in L ready , the inner while loop (See Figure 2) keeps deferring an operation in
each iteration. In order to select an operation to defer, a deferral force is calculated for each of the ready list operations
and the least force operation is picked. When the resources are sufficient the remaining operations in the ready list
are scheduled in the current time step.
The first step in computing deferral forces is to determine the time frames for every operation by evaluating their ASAP
and ALAP (as late as possible) schedules. The next step is to determine the distribution graphs which is a measure of
the concurrency of similar operations [12]. Finally, the forces for each operation are computed given their time frames
and the distribution graphs. After the calculation of forces for all operations have been performed, the deferral that
produces the lowest force is chosen. This is repeated until resources are sufficient to implement the operations in the
ready list. All operations in the pruned ready list are now assigned to a time step.
4.2 Formalization of Base Specification Model
The base specification model for the scheduling task described earlier in Section 3 is now formalized as theorems in
higher-order logic. The formulation is done in the PVS (Prototype Verification System) [17] specification language
environment. In order to understand the formal specification model better we will first introduce basic type information
about the formal model of the FDLS algorithm. Based on this, we will describe the formalization of the correctness
properties as theorems in higher-order logic.
4.2.1 FDLS Type Specification
The input to the scheduling algorithm is a dependency graph. The operations in this input specification form the
nodes in the graph and the dependencies between operations are represented by directed edges. The type specification
shown in Figure 3 describes the type structure of the input specification. Operations can be arithmetic, logical,
conditional etc. We therefore model the operation node, op node, for any desired set of data values by declaring it
as an uninterpreted type. It thus behaves as a placeholder for an arbitrary set of data values. The + in the type
declaration denotes that op node is a nonempty type and that there has to exist at least one variable of this type to
avoid certain typecheck conditions. dep edge is declared as an interpreted type. It is actually a type name for a tuple
type and defines an ordered pair of op node thus capturing the semantics of a directed edge in the input dependency
Force Directed List Scheduling(DFG; R bag )
Begin
Length in the DFG
while (T step - Tmax )   Each iteration corresponds to a T step
Evaluate Time F rames
ready / f All operations whose time frames intersect with T step g
while (R bag not sufficient)   Need to defer an operation
Compute
Op / Operation in L ready with the least force
ready / L ready \Gamma fOpg   Defer the operation
if (Op in critical path) then
Evaluate Time F rames
while
for each (operation Op 2 L ready )
Schedule Op at T step
end for
while
End

Figure

2: Force Directed List Scheduling Algorithm
graph. The tuple type op graph captures the semantics of the input dependency graph. It is defined to be an ordered
pair of sets. The first projection is of type op node set while the second projection is of type dep edge set and is
actually a dependent type defined in terms of its first projection. This ensures that a input dependency graph g is
well-formed in terms of its edges being defined only in terms of the nodes in the graph.
In addition to the input dependency graph, the scheduling task expects a bag of resources and an initial schedule
function. In the type declaration shown in Figure 3, module is an uninterpreted nonempty type. A bag of modules is
derived from it to represent the input resource bag. The scheduling function is of type schedule and maps the domain
of op node to the naturals.

Figure

4 shows some of the relevant variables used in the description of the correctness theorems. The input graph is
defined in terms of a finite set of nodes N, and a set of edges E. Three function variables of type schedule are declared
and a module bag variable, Rbag is declared. The scheduling algorithm is represented by the fdls function. It is a
recursive function that takes an input graph, (N, E), a bag of resources Rbag, and an initial schedule (just a placeholder
function to initiate recursion). final sched func is the output function of the scheduling algorithm.
4.2.2 Existence Theorem:
The existence theorem is shown in Figure 5. This theorem states that, final sched func, the schedule function
obtained after the execution of the fdls function maps every operation in the input graph to a positive natural:
The fdls function expects three arguments: the dependency graph, a bag of resources and an initial scheduling
function. The output of the fdls function is the final schedule. The above theorem asserts that this final schedule
maps every node in the graph to a positive time step. The existence function accepts a set of nodes and a schedule
function and returns a true if all nodes in the node set have been scheduled.
op-node: TYPE+;
dep-edge: e: edge - proj-1(e) /= proj-2(e);
pred[e:dep-edge - node-set(proj-1(e)) AND
proj-1(e1)=proj-1(e) AND proj-2(e1)=proj-2(e) =?
module: TYPE+;
modules
schedule:

Figure

3: Types for Formal Model of FDLS Algorithm
N: VAR finite-set[op-node];
E: VAR pred[dep-edge];
Rbag: VAR modules;
sched-func: VAR schedule;
init-sched-func: VAR schedule;
final-sched-func: VAR schedule;

Figure

4: Variables in PVS Model for Scheduling
4.2.3 Dependencies Preserved Theorem:
This theorem is shown in Figure 6. It ensures that the final schedule does not violate the dependencies specified in
the input dependency
The dependencies preserved function takes a graph and the final schedule and ensures that the dependencies in the
graph are preserved by the final schedule. This function visits every edge in the input graph and checks if the partial
order is maintained by the schedule.
existence: THEOREM
FORALL (N, E, Rbag, init-sched-func, final-sched-func):
=? existence(N, final-sched-func)
existence(N,

Figure

5: Existence Theorem for Scheduling
dependencies-preserved: THEOREM
FORALL (N, E, Rbag, init-sched-func, final-sched-func):
=? dependencies-preserved((N, E), final-sched-func)
dependencies-preserved(og,

Figure

Dependencies Preserved Theorem for Scheduling
FORALL (N, E, Rbag, init-sched-func,
fdls((N, E), Rbag, init-sched-func))
constraints-satisfied((N, E), Rbag,
final-sched-func)
constraints-satisfied(og, Rbag, sched-func):
FORALL (tstep: posnat):
proj-1(og)(n) and
IN
resource-suff?(ros: finite-set[op-node],
Rbag:
IF (EXISTS opnode-resource-map:
member(opnode-resource-map(n1), mbag) AND
member(opnode-reource-map(n2), mbag)
THEN true
ELSE false

Figure

7: Resources Sufficient Theorem for Scheduling
4.2.4 Resources Sufficient Theorem:
This theorem shown in Figure 7, asserts that a correct scheduling function obeys the resource constraints as specified
by the input resource bag. This is specific to a resource constrained scheduler algorithm which attempts to optimize
on the time steps given a limited set of resources.
The schedule satisfies constraints is a function that performs the resource suff? test at each time step. The
resource suff? function returns a true if all operations in the given time step denoted by S can be executed by the
resources in Rbag. The resource suff? function is specified in the PVS model of the fdls theory and is shown in

Figure

7.
The resource suff? function accepts a set of selected nodes known as the ready set and a bag of resources. We declare
a function, opnode resource map that maps the set of op node to the resource bag Rbag. The resource suff? function
returns true if this mapping is injective and all nodes in ros are mapped to resources in Rbag.
The three base theorems specify the functional correctness of a resource constrained scheduling algorithm. They make
no assumptions about the implementation details of the scheduling algorithm and assert properties that should be
satisfied by any correct scheduling task that attempts to time-stamp the input dependency graph.
We had two choices in modeling the FDLS algorithm in PVS: constructively by explicitly defining how the result
of the algorithm is to be constructed, or descriptively, i.e. by stating a set of properties (axioms) the algorithm is
to satisfy. We chose the former style since it was most conducive to our top-down approach to verifying the FDLS
algorithm. Each function in the algorithm is constructively defined and we use the PVS language mechanisms to
ensure that all functions and hence the algorithm is well defined and total. A purely descriptive style could introduce
inconsistent axioms and lemmas although it would be very useful for under-specification. In fact, a judicious mix of
both styles of specification would best suit our verification strategy. Since our verification exercise concentrates on
developing the correctness properties of the scheduling task, we can axiomatize portions of the formal model of the
FDLS algorithm that pertain purely to optimization issues. For example, in the FDLS algorithm shown in Figure 2,
the Compute deferral forces function decides which operations from the ready set are selected to be scheduled at
the current time step. A set of axioms can quite easily be stated to capture the requirements of this function. The
exact construction of this function is not necessary to conduct our verification exercise.
4.3 Formal Verification of FDLS Algorithm
Given the formal model of the FDLS algorithm and the three theorems as formal assertions that capture the general
correctness criteria for the FDLS algorithm, we next verify that the formal model of this algorithm indeed satisfies
these theorems in the PVS proof checking environment. The PVS verifier employs a sequent calculus [18]. In a sequent,
the conjunction of the antecedents should imply the disjunction of the consequents. A sequent calculus proof can be
viewed as a tree of sequents whose root is a sequent of the form ' A, where A is the property to be proved and the
antecedent is empty. A proof in PVS ends when every path from the root of the tree terminates in a leaf node, where
the implication is indeed true.
The fdls theory in PVS is shown in Figure 8. The fdls function is defined recursively and captures the semantics of
the FDLS algorithm shown in Figure 2. In the pseudo-code shown in Figure 2, the outer most while loop terminates
when But inside the loop Tmax is conditionally stretched. Modeling the loop structure as a recursive
function with the same terminating condition would lead to an ill-defined function. In a recursive function in PVS we
are required to specify a MEASURE function to ensure that the recursive function is well-defined. The measure is applied
to the arguments of the recursive call and compared to the measure applied to the original arguments. In the above
case, the MEASURE function specifies that the cardinality of the set of unscheduled op node in the input graph should
reduce with each recursive call. Due to lack of space, the formalization of force and its update using time frames,
distribution graphs, calculation of ASAP and ALAP schedules are not shown in the PVS model in Figure 8. We will
present some insight into our verification approach by partially walking through a portion of the proof exercise for one
of the theorems, namely the existence theorem.
The existence theorem states a truth about all nodes in the input graph. The proof for this theorem proceeds by
induction on the variable N, the set of op node using an induction scheme for card(N). This results in a base case
that is easily discharged by grind-a built-in strategy and an induction case that is displayed below as a sequent in

Figure

9.
The proof goal is specified by formula [1] in the consequent. In the antecedent, formula f-1g reiterates the induction
step. By carefully studying the sequent, one can observe that the proof goal is actually embedded within formula [-3].
With appropriate proof steps to isolate the right side of the implication in formula f-3g, we can, with proper instan-
tiations, extract a formula that matches the proof goal shown in formula [1]. In order to isolate the proof goal and
thus prove the theorem we have to carefully introduce four additional lemmas into the specification. These lemmas
form the first hierarchy of lemmas for the Existence theorem and are categorized as Level 1 lemmas as shown in Figure
10. They assert a set of correctness properties that are very specific to the FDLS algorithm. For example, lemma
delete ros card lemma states that the function new unsched nodes always returns a set whose cardinality is always
smaller than the original node set N. In other words, it formalizes the assertion that a nonempty set of operators is
scheduler: THEORY
BEGIN
IMPORTING fdls-types
get-max-parent-tstep((R: finite-set[op-node]),
(og: op-graph), (sched-func: schedule)):
IN IF empty?(P) THEN 0 ELSE maxrec(P) ENDIF
get-max-sched((sched-func:
updated-sched((ros: non-empty-finite-set[op-node]),
(sched-func: schedule), (max-sched: nat)):
(LAMBDA (n: op-node):
IF ros(n) THEN max-sched
updated-ros((ros: non-empty-finite-set[op-node]), (mbag: modules)):
get-ros((og:
n: op-node -
final-ros((og: op-graph), (mbag: modules)):
new-sched-func((og: op-graph), (mbag: modules), (sched-func: schedule)):
updated-sched(final-ros(og, mbag), sched-func, get-max-sched(sched-func))
new-edges((og: op-graph), (N: finite-set[op-node])):
e: dep-edge - PROJ-2(og)(e) AND N(PROJ-1(e)) AND N(PROJ-2(e))
new-unsched-nodes((og: op-graph), (mbag: modules)):
fdls((og: op-graph), (mbag: modules), (sched-func: schedule)):
fdls((new-unsched-nodes(og, mbag),
restrict(new-edges(og, new-unsched-nodes(og, mbag)))),
mbag, new-sched-func(og, mbag, sched-func))
END scheduler

Figure

8: Overview of PVS Theory for FDLS Algorithm
AND
fdls((new-unsched-nodes((S!1, restrict(E!1)), Rbag!1),
restrict(new-edges((S!1, restrict(E!1)),
new-unsched-nodes((S!1,
restrict(E!1)),
Rbag!1,
new-sched-func((S!1, restrict(E!1)), Rbag!1, init-sched-func!1)))
[-3]
IMPLIES FORALL (E, Rbag, init-sched-func, final-sched-func):
=? existence(S2, final-sched-func))

Figure

9: Induction Step Proof Sequent in FDLS Algorithm Verification
scheduled in each recursive call of the fdls function. The new unsched nodes function in this lemma takes the given
graph and returns a smaller node set by removing from the graph the operators that were scheduled in the current
iteration. The proof steps for the delete ros card lemma lemma are shown in Table 11. The proof for this lemma is
easily discharged with the introduction of three additional lemmas as shown in the table. These lemmas introduced
to prove the delete ros card lemma form the second hierarchy or Level 2 lemmas.
We adopted a top-down approach to simplify the proof exercise. Theorems are proved using lemmas (Level 1 lemmas)
and other appropriate inference rules provided by the proof system. The proofs of the the Level 1 lemmas sometimes
require the introduction of additional lemmas (Level 2 lemmas) and sufficient care is taken to ensure that the lemmas
that are introduced are consistent and relevant to the verification exercise. These lemmas are next proved and in the
course of their proofs, additional lemmas are introduced. This process continues until no more additional lemmas need
to be introduced. A theorem is thus considered proved only after it has been proved and the lemmas in all hierarchies
below it are successfully proved. The top-down approach results in a well-structured proof exercise. In addition to
making the overall proof effort manageable, it has the added advantage of systematically deriving a large set of formal
correctness properties (lemmas).
In a large and complex task such as Scheduling, it is rather difficult to identify the task invariants. This makes the
verification of such algorithms a hard problem. Our approach presents a systematic way to identify these invariants
and generate them in a formal environment. For the Existence theorem alone, a total of 26 invariants were formulated
as a part of the proof exercise. This large set of formally derived invariants provide considerable more insight into the
correctness issues concerning the existence theorem for the FDLS algorithm. A similar proof approach was adopted to
verify the other two theorems concerning dependency preservation and resource sufficiency. Thus, starting with three
base theorems, we were able to formulate a set of 43 lemmas or formal assertions as a consequence of the formal proof
system. These formal assertions were organized into four levels of hierarchy and assert several invariant properties of
the FDLS algorithm. Without introducing this formalism in our specification model, it would be very hard to identify
the task invariants or formal assertions, express them with precision and be assured of their correctness. In the next
section, we will show how we used the set of formal assertions that make up the enhanced specification model for the
delete-ros-card-lemma: LEMMA
nonempty?(N) =?
card(new-unsched-nodes((N, E),
delete-existence-lemma: LEMMA
final-sched-func: schedule,
init-sched-func: schedule, Rbag: modules):
existence(new-unsched-nodes((N, E), Rbag), final-sched-func)
AND
existence(difference(N, new-unsched-nodes((N, E), Rbag)),
new-sched-func((N, E), Rbag, init-sched-func))
=? existence(N, final-sched-func))
ros-construction-lemma: LEMMA
FORALL (E: pred[dep-edge],
N: finite-set[op-node], Rbag: modules, n: op-node):
member(n, N)
AND
NOT member(n, new-unsched-nodes((N, E), Rbag))
=? member(n, final-ros((N, E), Rbag))
ros-existence-lemma: LEMMA
init-sched-func: schedule, Rbag: modules, n: op-node):
member(n, final-ros((N, E), mbag))
=? new-sched-func((N, E), mbag, init-sched-func)(n) ? 0

Figure

10: Level 1 Lemmas for Existence Theorem in FDLS Algorithm
FDLS algorithm to formalize a C++ implementation of the FDLS algorithm.
Implementation - Formal Assertions Embedding in Program Code
In this section, we will discuss how we used the set of formal assertions that make up the specification model of the
FDLS algorithm to verify the scheduler implementation in an existing high-level synthesis system, DSS [5]. DSS accepts
algorithmic behavioral specifications written in a subset of VHDL and generates an RTL design also expressed in VHDL,
subject to the constraints on clock period, area, schedule length, and power dissipation. The scheduling phase in DSS
is implemented as a variation of the FDLS algorithm, extended to handle VHDL specifications with multiple processes,
signal assignments and wait statements. The FDLS algorithm is further enhanced to perform global process scheduling
such that operations across processes share the same data path resources. In addition to assigning timesteps, this
stage also binds operations to functional units in the target library. The scheduling stage currently does not support
pipelining, chaining or multicycling. The overall structure of the implemented scheduler in DSS is modeled closely on
the FDLS algorithm described in Section 4.
The theorems and lemmas formulated during the theorem proving exercise constitute a set of formal assertions and
invariants that represent the functional specification of the FDLS algorithm. If, during an execution run, the scheduler
is faithful to this formal specification model, we can assert that a correct schedule will be generated.
(ASSERT)
(ASSERT)
(ASSERT)

Figure

11: Proof Steps for delete ros card lemma
Since the formal specification model is formulated in higher-order logic and the implementation (the scheduler in DSS)
is in the C++ software domain, establishing the equivalence ' Imp ) Spec is not a straightforward procedure. The
formalized specification model is a set of formal assertions that specifies the invariants for different portions of the FDLS
algorithm. The formal assertions are translated into C++ program assert statements and embedded in portions of the
scheduler implementation that correspond to the spatial locality of the invariants in the formal model of the algorithm.
The scheduler is thus embedded with its formal specification model giving rise to an auto-verifying scheduler. For
the sake of illustration, Figure 12 shows the FDLS algorithm with a small sample of the formally derived program
assertions embedded within it. The three base program assertions correspond to the three base formal assertions stated
originally. We carefully translate these theorems to C++ assert statements and place them outside the body of the
FDLS implementation. Since they verify the truths for any scheduling technique, they can be used as a checkpoint in
order to ensure that the final state of the scheduler is not in violation of the three universal correctness properties.
Once the scheduler has completed execution and generated a schedule, the base program assertions are executed on
the schedule. If an incorrect schedule is generated, one of these assertions raises an exception. Thus, any schedule
that is generated by the formally embedded scheduler is guaranteed to be error-free. A correct scheduler is completely
specified by the three base assertions and they are capable of detecting any error in the scheduler implementation that
might result in an incorrect schedule.
The base formal assertions, due to their spatial location in the code and their high-level notion of correctness usually
do not provide any more useful information about an incorrect schedule apart from detecting its presence. The lemmas
and axioms that were systematically formulated as formal assertions and verified as a result of the PVS proof exercise
play an important role in error diagnostics. We will illustrate this by referring to the embedded FDLS algorithm
shown in Figure 12. The formal assertions, introduced at different levels of hierarchy during the proof exercise are
carefully translated into program assertions. The hierarchy is preserved in the organization of the program assertions.
Thus level 1 program assertions are narrower in scope but at the same time focus on detecting errors in local areas
of the scheduler implementation. These assertions are embedded in the code as shown just after the inner while
loop and after the for loop and they assert the invariant properties of the loop statement. The delete ros card
assertion states an invariant property that is true at the end of every iteration of the outer while loop. By placing
it in that portion of the code, we ensure the identification of any violations to this assertion in every iteration of the
scheduler. Contrast this with the error showing up in the base assertions after all iterations of the scheduler have
been completed. Level 1 assertions thus, offer better diagnostics and the user is promptly made aware of any error
in the implementation. As we proceed down the hierarchy of formal assertions, finer details of the implementation
are subjected to verification. The formal assertions that correspond to these levels are specific to verifying smaller
portions of the scheduler code and thus they can expose errors in the code are pinpoint them accurately. Going back
Force Directed List Scheduling(DFG; R bag )
Begin
Length in the DFG
Level 3 Assertions
schedule invariant; ordered schedule
strict subset nonempty
oe
while (T step - Tmax )
Evaluate Time F rames
ready / f All operations whose time frames intersect with T step g
while (R bag not sufficient)
Compute Assertions
ros invariant; ros construction
ros nondependence; card strict sub
oe
Op / Operation in L ready with the least force
ready / L ready \Gamma fOpg
if (Op in critical path) then
Evaluate Time F rames
end while Level 1 Assertions
final ros sufficiency; edge dependence
final ros wellformed; ros sufficiency
oe
for each (operation Op 2 L ready )
Schedule Op at T step
end for Level 1 Assertions
delete ros card; delete existence
graph wellformed; edge wellformed
oe
while
Base Assertions
existence; dep preserved; res sufficiency
oe
End

Figure

12: FDLS Algorithm with a Sample of Formal Assertions
to our previous example, although the program assertion delete ros card, by virtue of its position in the code is
able to detect errors within one iteration of the outside while loop in the the scheduler, it might still not be good
enough to locate the source of a problem. card strict subset was one of the lemmas used to complete the proof
of the delete ros card property in the theorem proving environment. The corresponding Level 2 formal assertion
verifies the invariance during each iteration of the inner while loop in the algorithm. The assertion concentrates on a
smaller portion of the implementation and can promptly detect any violations to the base assertions.The verification
approach can thus be extended to as many levels of hierarchy as there are in the formal assertion tree until the source
of an error is isolated.
Detection and Localization - An Example
DSS, since its inception has been used to synthesize over benchmarks and other large-scale specifications.
These design examples were carefully chosen to test a wide range of synthesis issues and ranged from single process
arithmetic-dominated specifications to multiple process specifications with complicated synchronization protocols and
various combinations of control constructs like conditionals and loops. In fact, this effort was part of a concerted
#endif
assert(dependencies preserved(fdls map));
#endif
#endif

Figure

13: Base Program Assertions in Scheduler
attempt to systematically validate DSS using simulation and formal techniques [9, 10, 15]. During the course of this
exercise, sometimes incorrect RTL designs were synthesized. Analysis of these faulty designs eventually lead to the
discovery of implementation errors in the HLS system. Notably, some of the errors in the RTL designs, were attributed
to conceptual flaws in the scheduler implementation. These errors were identified using systematic simulation methods
and traditional software debugging aids. Although this exercise led to an increased confidence in the reliability of the
synthesis system, given the limited number of test cases involved, one could never be sure of isolating all bugs in the
system. Also, the complexity of the synthesis system itself rendered the error trace back often quite laborious and time
consuming. With the formal assertions approach, we hope to address both problems in validating synthesized RTL
designs. In particular, since the formal specification model of the scheduler is embedded within its implementation (as
C++ assertions), an incorrect schedule is almost always guaranteed to violate this specification model. This violation
is immediately flagged as an exception and the user is notified. By properly enabling the formal derived program
assertions, the trace back to the source of the bug can be performed almost effortlessly.
To illustrate our approach, we will walk through an error detection exercise in the scheduling stage of the synthesis
system using the formal assertions technique. The formally embedded scheduler was seeded with an error that would
result in the synthesis of an RTL design with an incorrect schedule. We begin by enabling only the base program
assertions during the first run of the scheduler. Since these assertions are checked only once during an execution
run the overhead introduced by them is minimal. If necessary, we could then systematically enable the levels of
hierarchy in the formal assertions tree to build an error trace that would guide us to the problem area in the scheduler
implementation. The bug in the scheduler code fires the dependencies preserved base program assertion during
the synthesis of an RTL design. As shown in Figure 13, this assertion is situated at the end of the scheduling task
along with the other two base assertions. In the figure, the function fdls graph implements the FDLS algorithm and
returns a final schedule fdls map. The base assertions are placed outside the actual implementation of the scheduler.
The assertion that checks to see if the schedule preserves the dependencies (boldfaced and italicized in the figure) in
the input graph fails due to the error introduced in the code. This tells us that the final schedule somehow violates
the partial order specified by the input graph. In order to get more information about the source of the error, the
Level 1 program assertions are enabled. The scheduler is executed again for the same set of test cases and this time the
assertion failure occurs within the body of the fdls graph function. The portion of the scheduler function that has
the embedded assertion is shown in Figure 14. The assertion edge dependency lemma is placed just at the termination
of the inner while loop. This assertion is a C++ translation of the following PVS lemma.
if (unsched-nodes(p) == ready-list(n)) f
break;
// end inner while loop
assert(edge dependency lemma(ready list,
unsched nodes, original unsched nodes));
#endif
assert(delete-ros-card-existence-lemma(unsched-nodes.length(),
#endif

Figure

14: Level 1 Program Assertions in Scheduler
FORALL (og; op-graph, e: dep-edge):
member(e,
NOT member(e, new-edges(og, new-unsched-nodes(og, mbag)))
AND member(PROJ-2(e), new-unsched-nodes(og, mbag))
The above lemma states that, if an edge is present in the present graph but is not present in the next update of the
graph, one of its nodes must be in the ready set ROS, and the other node must be in the updated graph. Thus the
failure of this formal assertion (shown boldfaced in Figure 14) gives the user some insight into the nature of the error.
The portion of the scheduler code around this formal assertion was examined closely for errors but no immediate
cause for error was discovered. The Level 2 assertions were now enabled in the hope that they would provide more
information on the cause of the error. The scheduler is executed again and this time one of the assertions in the Level 2
class of program assertions fails. A snapshot of the code is shown in In Figure 15. This time the program assertion
ros nondependence assertion (shown boldfaced in Figure 15) fails. It is placed just before the inner while loop that
checks for resource sufficiency in Figure 12. This assertion is translated from the following PVS lemma.
ros-nondependence: LEMMA
FORALL (og: op-graph, n: op-node, m: op-node):
member(n, ros) AND member(m, ros)
=? NOT member((n, m), proj-2(og)) AND
NOT member((m, n), proj-2(og))
This lemma states a property that all nodes in the ready set, ros, must satisfy. This property asserts that no two
nodes in the ready set can have an edge between them. This means that, the ready set is comprised of nodes that
have no dependency relations among them. Clearly, this assertion failure indicates that the current ready set somehow
violates this property. So we only need to look at the routine that builds the ready set in order to find the error.
// Build the ready list
while (n !=
Check if there is any unscheduled parent
all-parents-are-scheduled
error   if (p !=
if
all-parents-are-scheduled
break;
if (all-parents-are-scheduled) f
assert(ros nondependence(ready list, unsched nodes));
#endif
// Defer operations until resource constraints are met
while

Figure

15: Level 2 Program Assertions in Scheduler
Upon examining this portion of the code which is located just above the failed assertion, it can be easily noticed that
the selection process is the culprit. The selection process erroneously admits a node into the ready set even when one
of its parents have not been scheduled yet. This is caused by the if statement in the code shown in Figure 12. The
selection process should admit a node in the ready set only after all of its parents have been scheduled. This can be
achieved by replacing the erroneous if construct by a while construct.
By constraining the scheduler implementation to abide by its formal specification at every step of the execution run,
we can ensure a very efficient and reliable error detection and trace mechanism. Errors can be traced back to their
source using a technique of systematically enabling higher levels of formal assertions.
7 Errors Discovered by Formal Assertions
In order to test the effectiveness of the formal assertions approach, the synthesis system was seeded with 6 programming
errors in the formally embedded scheduling stage. These errors represent actual implementation errors that were earlier
discovered over a period of time through traditional validation techniques like simulation and code walk throughs. It
was hoped that our approach would serve two purposes: discover at least all 6 seeded errors and with little or no user
intervention and provide an error trace to the source of the program errors in the scheduler. We executed the synthesis
system for a number of design examples.

Table

1 shows the details of the experiment. The seven examples range in size from as little as 12 operation nodes up
to as many as 300 operation nodes.
Test Assertion Levels that detect the Errors
(op nodes)
26 fbase,1,2g pass fbaseg fbase,1g f1g pass pass
Test3 50 fbase,1,2g fbase,1g fbaseg pass f1g pass pass
Test6 200 fbase,1,2g fbase,1g fbaseg pass f1g fbase,1g fbaseg

Table

1: Verification Results for a Formally Embedded Scheduler
Columns 3-7 tabulate the error detection results for each of the five program errors detected during the execution of
the scheduler code. The entries in these columns indicate the levels of formal assertions that were needed to pinpoint
the source of the error. All the pass entries in Table 1 indicate successful execution. For these test cases, the program
errors had no adverse effects and a correct schedule was generated by the implementation. So none of the formal
assertions were triggered. If base formal assertions were sufficient to ascertain the source of an error, then base alone
appears in the corresponding entry of the table. Thus, Error 3 was detected by one of the base formal assertions for
all test cases. Next observe the results for Error 1. This error involved an incorrect way of building the ready set and
was earlier illustrated in the previous section when we walked through an error detection exercise. For Test
error went undetected since none of the nodes in this test case had more than one parent, and as a result the error
in the code did not result in an incorrect schedule. For the rest of the test cases, the formal assertions, base through
level 2 detected this error. In all these cases, although the error was detected by all three levels, formal assertions up
to level 2 had to be enabled in order to pinpoint the source of the error.
discovered with the formal assertions approach. The error hitherto, had escaped detection even during
simulation and code inspection. The defer operation routine was the culprit. The available resources were incorrectly
analyzed while building the ready list. As a result, there was a discontinuity in the schedule numbers assigned to the
operators in the input specification. This conceptual error was detected by enabling the Level 1 program assertions.
introduced an error in the ASAP and ALAP routines. It manifests itself in the last three test cases and in fact
needed formal assertions up to level 1 hierarchy to be enabled in order to locate the source of the error. Error 6 had
no effect over the schedule for the first four test cases since they had enough resources to schedule their operations
and hence the bug goes undetected. Error 7 represents a program error in the force calculation routine. The scheduler
generated correct schedules for test cases 1, 2, and 3 since there was enough resources to schedule the operations and
hence the defer operation routine was never executed while scheduling these test cases. In the rest of the four test
cases, the error was discovered and its source pinpointed by the base assertions.
The overhead of the formal assertions approach is not significant. Table 2 shows timing information for the test cases
presented above. This experiment was conducted on a Sparc 5 workstation with 60Mb resident memory. The second
column represents FDLS algorithm run time with none of the assertions enabled. The entries in the third column
denote the run times for the algorithm with the three base assertions enabled. The increase in run times is hardly
noticeable and this is to be expected since the base assertions are evaluated just once after the scheduling algorithm
assigns the time steps. The fourth column represents run times when all levels of program assertions are enabled in
the algorithm. There is an appreciable increase in run times since the assertions embedded within the algorithm are
now evaluated several times during the execution of the algorithm. It can be quite clearly seen that the overhead
introduced by the formal assertions approach does not pose any serious problems to the performance of the FDLS
algorithm. Typically, base assertions can be switched on during the normal synthesis process. An assertion failure
signals that the synthesis process is at fault somewhere in the implementation. The design can then be re-synthesized
Test No. FDLS Algorithm run time in seconds
assertions Base assertions All assertions

Table

2: Run-time Overhead due to Formal Assertions in Scheduler
by enabling lower levels of program assertions in order to trace back to the source of a program error in the synthesis
system.
8 Scope of the Verification Effort
The formal assertions technique ensures the detection of any incorrect schedule: a schedule that directly or
indirectly violates the base formal assertions. Therefore, the validity of the verification approach hinges on the
completeness of the set of theorems that make up our base specification model. The lemmas derived formulated
during the thorem proving exercise are usually limited to identifying errors that result in violations of any of the base
theorems. In the above experiment, it was observed that except for Error 5, all errors that led to an incorrect schedule
were identified by the base assertions. This reinforced our confidence in the completeness of the set of base theorems.
exploited the absence of a base correctness condition that ensured the tightness property discussed earlier in
the second footnote at the end of Section3.1. There we discussed the possibility of adding a fourth base theorem that
captured the so-called tightness property, which states that there cannot be a discontinuity in the schedule of the input
graph. Since this was not strictly a correctness issue we did not include it in our base theorems. But it so happened
that one of the level 1 lemmas (engendered by the induction strategy in our deductive analysis) used to prove the
base theorems explicitly specified this property. This explains why Error 5 was discovered by level 1 assertions but
slipped past the base assertions. Typically the lower level assertions and axioms enable the error detection at a finer
granularity than possible with the base assertions and the error detecting capabilities are limited to but more specific
as compared to the base formal assertions.
After verification, the formal assertions are translated into program assertions in the synthesis system. Given the
expressive differences between the logic and software domain, the translation process often could get quite complicated.
Ultimately, the correctness of the formal assertions approach hinges on this translation process. Convenient data
structures exist that allow us to conveniently conduct the translation process. Sometimes the theorems cannot be
translated directly in the software domain. In such cases, we develop equivalent formal assertions amenable to the
software domain and then formally establish the equivalence relationships to ensure that the translation process is
indeed correct.
Portability issues of the formal assertions approach need to be addressed. Base assertions, typically, can be quite easily
ported across different algorithms that perform the same task in synthesis. Lower level assertions formulated during
the course of the formal proof exercise present limited portability. These formal assertions with some modifications can
be fairly easily ported across implementations that belong to the same class of algorithms. Portability across classes
of algorithms could be restricted and would require additional proof exercises in order to formulate appropriate formal
assertions.
The formal assertions approach verifies a single execution run of the synthesis process and guarantees a correct design
if the specification is not violated in the process of synthesis. It is therefore entirely feasible that the bugs in the
synthesis system go undetected until they manifest themselves during an execution as shown in Table 1. The bugs are
exposed as soon as they introduce errors in the RTL designs being synthesized.
9 Conclusions and Future Work
Insertion of assertions and invariants [2] in programs has been known to be an effective technique for establishing the
correctness of the outcome of executing the program and for discovering and isolating errors. However, determination
of an appropriate set of assertions is often a tedious and error-prone task in itself. In this paper, we made use of
mechanical theorem proving to systematically discover a set of sufficiently capable assertions.
We presented a formal approach to verifying RTL designs generated during high-level synthesis. The verification
is conducted through program assertions discovered in a theorem proving environment. In this paper, we focused
on the resource-constrained scheduling task in synthesis. Correctness conditions for resource-constrained scheduling
have been formally specified in higher-order logic and a formal specification of the FDLS algorithm is verified using
deductive techniques. A large set of additional properties is systematically discovered during the verification exercise.
All of these properties are then embedded as program assertions in the implementation of the scheduling algorithm
in a high-level synthesis tool. These assertions act as watchpoints that collectively ensure the detection of any errors
during the synthesis process.
An appealing aspect of this approach is the systematic incorporation of design verification within a traditional high-level
synthesis flow. We conduct the formal verification exercise of the synthesized RTL design in the synthesis
environment as the design is being synthesized, avoiding the need for functional verification of the synthesized design
later using a formal verification tool or a simulator. The time taken for our "on-the-fly" verification approach scales
tolerably with the size of the design being synthesized. This is in contrast with blind post-facto simulation, model
checking or theorem proving based verification approaches that do not use any reasoning based on the properties of
the synthesis algorithms.
One criticism of this approach may concern the care and effort involved in the the manual process of converting the
formal assertions in higher-order logic into program assertions in C++. In our experience, this indeed proved to be
a process requiring considerable diligence. Often, we had to express the formal assertions in several different ways
in higher-order logic, each time carefully constructing the necessary data-structures in C++ to enable their implementation
as program assertions. This process had to be repeated until we discovered a form for the formal assertion
that lent itself to straight-forward transliteration into C++. We estimate the entire process of FDLS formalization,
verification and embedding of the assertions in the implementation took about 260-300 person hours.
Another criticism of this approach concerns the sufficiency of the assertions to isolate an error. An error cannot
be caught at its source, but only when it first causes an assertion violation. However, this is a problem with all
assertion-based approaches for program correctness. The sufficiency of the base correctness conditions is never formally
established; these conditions represent a formalization of our intuitive understanding of what a scheduler should do.
Effort is currently underway to adopt the verification strategy presented in this paper to formalize all the stages of a
high-level synthesis system. This approach will allow early detection of errors in the synthesis process before the RTL
design is completely generated.



--R

"Implementation Issues about the Embedding of Existing High Level Synthesis Algorithms in HOL"
"The Science of Programming"
"High-Level Synthesis,Introduction to Chip and System Design"
"Integration of Formal Methods with System Design"
"DSS: A Distributed High-Level Synthesis System"
"Introduction to HOL"
"An Engineering Approach to Formal System Design"
"Synthesis and Optimization of Digital Circuits"
"Synchronous Controller Models for Synthesis from Communicating VHDL Processes"
"Validation of Synthesized Register-Transfer Level Designs Using Simulation and Formal Verification"
"From VHDL to Efficient and First-Time Right Designs: A Formal Approach"
"Force Directed Scheduling for the Behavior Synthesis of ASICs"
"Scheduling and Binding Algorithms for High-Level Synthesis"
"High-Level VLSI Synthesis"
"Experiences in Functional Validation of a High Level Synthesis System"
"Some Experiments in Local Microcode Compaction for Horizontal Machines"
"PVS: A Prototype Verification System"
"User Guide for the PVS Specification and Verification System, Language and Proof Checker"
"Synthesis of Digital Designs from Recursion Equations"
"On the Interplay of Synthesis and Verification"
"A Survey of High-Level Synthesis Systems"
--TR
Scheduling and binding algorithms for high-level synthesis
High-level synthesis
Experiences in functional validation of a high level synthesis system
From VHDL to efficient and first-time-right designs
The Science of Programming
Synthesis of Digital Design from Recursive Equations
Synthesis and Optimization of Digital Circuits
High-Level VLSI Synthesis
DSS
An Engineering Approach to Formal Digital System Design
Implementation Issues About the Embedding of Existing High Level Synthesis Algorithms in HOL
On the Effectiveness of Theorem Proving Guided Discovery of Formal Assertions for a Register Allocator in a High-Level Synthesis System
PVS
Facet
Synchronous Controller Models for Synthesis from Communicating VHDL Processes
Theorem Proving Guided Development of Formal Assertions in a Resource-Constrained Scheduler for High-Level Synthesis
formal assertions;scheduler verification;formal synthesis;formal verfication;high-level synthesis;theorem proving