# Presentation: 186715

## Starfish: A Table-Centric Tool for Design Derivation 

- Alex Tsow
- The MITRE Corporation

- Affiliation with The MITRE Corporation is provided for identification purposes only, and is not intended to convey or imply MITRE's concurrence with, or support for, the positions, opinions or viewpoints expressed by the author.

**Notes:**
My name is Alex Tsow, and this talk is an overview of the results from my doctoral dissertation.  I graduated last summer from the Indiana University Computer Science Department under the direction of Steven D. Johnson.  I currently work for the MITRE corporation, however this work completed in its entirty prior to my employment with MITRE.  Use of the MITRE name is for identification purposes only and does not imply endorsement or support for this independent effort.

## Thanks to the NASA Langley Research Center

- This work was supported by a 3 year fellowship from the Graduate Student Researchers Program (GSRP).
- Sponsorship originated from
- NASA Langley Formal Methods Group
- Ricky Butler
- Paul S. Miner

**Notes:**
I have received significant support from the NASA Langley Formal Methods Group.  This work was funded under a three-year fellowship from NASA's Graduate Student Researcher's Program.  I want to extend special thanks to Ricky Butler, whose department sponsored the fellowship and to Paul Miner, my technical advisor at NASA.

I have with me a bound copy of the work including all software and derivations.  

Thank you.

## Design Derivation

- Formally generates systems
- Transformational algebra
- Contrast with post-design formal verification
- Synchronous stream networks
- Manual interaction
- How best to achieve interaction?
- How best to deliver a deep transformation space?

**Notes:**
My work follows the design derivation approach to formal methods. In this paradigm, a designer implements abstract systems by applying sequences of correctness preserving transformations. Contrast this with other approaches which have grown from a post design formal verification. 
The fundamental language of expression in design derivation is the synchronous stream network.
The methodology postulates that manual interaction is the essence of design process. The tools built to support it leave the discovery of novel properties to the human, while striving to manage the sea of details in sensible, but over-ridable way.

The core questions that my research addresses are
How best to achieve interaction?
How best to present an expressive transformation space?

## Two Common System Views

**Notes:**
System presentation has a profound impact upon a designer’s ability to forsee and apply transformations.

Here are two common view of a simple shift-and add multiplier.
the first is a control dominated expression in the form of an algorithmic state machine
The second is an architectural view emphasizing signal connectivity and component usage
Neither is ideally suited for contemplating transformations.

## Behavior Tables

- Decision Table

- Action Table

- Signals

- Updates

- Selector keys

- Branches

**Notes:**
My project settles upon hierarchies of behavior tables as its means of expression.
Behavior tables offer a compromise between behavioral and architectural views.
as a unit a behavior table is an architectural component with an I/O signature and bound by a connectivity network
Within a behavior table 
the left side--the decision table--represents control by enumerating the cases of the “next state function”
While the right side--the action table--represents architectural aspects with an enumeration of signals and how they are updated in a particular transition.

## Starfish 

- Tool for behavior table manipulation
- Implements transformation algebra
- b.t. display and derivation playback
- Explicit type system
- Data Refinement
- Interactive Serialization Tables
- Environment for high-level synthesis
- Retiming

**Notes:**
Here are the main contributions of my work.
Starfish is a tool to support design derivation with behavior tables.
It implements a transformation algebra
And it displays and executes derivation scripts
Starfish distinguishes itself from prior design derivation work by implementing an explicit type system which enables some basic kinds of data type translation.
Starfish develops interactive serialization tables, an environment for manually scheduling term operations over time.
Finally, Starfish adds a retiming transformation which allows the designer to convert between registered and combinational signals.

## Related Work

- Transformation systems
- Eisenbiegler & Kumar, *Formally Embedding Existing High Level Synthesis Algorithms *
- Teica, Radhakrishnan & Vemuri, *An Approach to High Level Synthesis & System Validation Using Formally Verified Transformations*
- Matthews & Launchbury, *Elementary* *Microarchitecture Algebra*
- Table-Oriented Engineering
- Heninger, Kallander, Parnas & Shore, *Software Requirements for the A-7 Aircraft*
- Heitmeyer, Labaw, et.al. *SCR**
- Leveson et.al., *RSML*
- Algebraic Specification
- Goguen, Thatcher, Wagner (ADJ), *Initial Algebra Approach to the Specification, Correctness, and Implementation of Abstract Data Types*
- Gurevich, *Evolving Algebras*

**Notes:**
Before going further I’d like to breifly recognize some related work outside of the Indiana University System Methods Design Group.
Eisenbeigler and Kumar, 
Teica Radikrishnan and Vemuri
Matthews and Launchbury
And their respective research groups have all furthered the cause of formal transformations. I’ve failed to include Mary Sheeran on the slide but much of her research is also closely related.
Table oriented engineering has been championed by many, including the software requirements work from the naval research lab and the statechart and table oriented expression language RSML.
And finally Starfish’s type system draws from a long list of work in algebraic specification work including that of the ADJ group and Gurevich’s evolving algebras.

## Behavior Table Semantics

*StackCalc(inst,a)=res*
*   **where*
* **res = (top s)*
* **s = {0} ! (sel (inst-cat instr)*
*                     **(push s a)*
*                     **(pop s)*
*                     **(push (pop (pop s))*
*                         **(alu (inst->op instr)*
*                             **(top s)*
*                             **(top (pop s)))))*

*Inputs*
*instr = (push, push, add ...)*
*a      = (5,      22,     2007, ...)*

*Internal Signals:*
*res = (  0,       5,          22,       27 ...)*
*s    = ({0}, {0,5}, {0,5,22}, {0,27}, ...)*

**Notes:**
This slide illustrates the stream semantics of behavior tables with a signal trace, 
and contrasts behavior table syntax with its s-expression counterpart.
This example is a simple stack calculator which takes two input streams-- instruction and data-- and produces a result--"res”--output stream.
Here, the external agent adds the numbers 5 and 22. 
The trace shows the difference between combinational updates, which are immediate and sequential updates which are delayed.
The result signal, res,  is a combinational projection of the stack signal, s, using the top accessor.

## Table Algebra

- Add/Remove signal
- Apply a term-level algebraic identity
- Instantiate a “don’t care” subterm
- Substitute combinational action for variable
- Tuple/Untuple signals
- Add/Remove decision key
- Instantiate decision branches
- Substitute branch value for decision key term
- Split a table into multiple tables

**Notes:**
Starfish implements a table algebra similar to the architectural transformations in previous design derivation tools
Under certain conditions the designer may:
<READ SLIDE>

## System Factorization

**Notes:**
Behavior Tables are well suited for imposing high-level architectures on state machine specifications through a process called system factorization.
This behavior table is equivalent to the control-dominated ASM chart of the shift and add multiplier shown earlier.
Factorization lets the designer separate abstract signals and abstract operations from control-dominated logic. 
This is the first step in architectural decompostion.

## System Factorization

**Notes:**
This is the the result of factoring a shift register and an ALU from the original specification.
The residual controller has been expanded to move selectors from the action table into the decision table, creating a more explicit enumeration of the control transition function.
Stream equations specify how the ports of each behavior table connect to each other.

## Creating Factorization Opportunities

- Retiming
- Serialization
- Data Refinement

**Notes:**
Starfish implements a number of technologies that expand the factorization space.
- Retiming which translates between combinational and sequential signals.
- Serialization --a behavioral refinement that is motivated by architectural constraints
- And data refinement which translates systems defined over abstract types into systems defined over representation types.

## Retiming

*update*

*top*

*res*

*s*

*{0}*

*update*

*top*

*res*

*s*

*{0}*

*0*

*instr*

*a*

*instr*

*a*

**Notes:**
Here is an example of retiming. 
In the top abstract stack calculator circuit, the result signal, res,  is a combinational projection of the stack signal, s.
The lower circuit turns res into a sequential signal by applying the top accessor to the stack signal’s update value.

## Retiming

- Retiming ‘res’ and ‘tl’’

**Notes:**
This sequence shows how retiming can enhance the system architecture.
I want to move from a system with a combinational projection of the stack top 
To a system that maintains registered copies of the stack top and stack tail.
First we introduce a combinational tail signal.
Then apply a sequence of term-level rewrites.
Apply the retiming to create registered head and tail signals.
Simplify terms algebraically.
Eliminate the stack signal.

## High-Level Synthesis

- push

- top

- alu

- top

- pop

- pop

- s

- instr

- Data Flow Graph for
- 	*(push (pop (pop s)) *
*	**	**(alu-op instr (top s) (top (pop s))))*

**Notes:**
Often times an initial specification loads too many operations into a single step.
In the stack calculator example, all of the stack update and arithmetic occurs in one term, shown above.
Target arch. has limited resources
E.g., number of execution units or simultaneous memory accesses
The signal update needs smaller steps. 
The following sequence shows how a high-level synthesis algorithm might schedule the actions.
The process begins with a data-flow graph of the signal update.

## High-Level Synthesis

- push

- top

- alu

- top

- pop

- s

- instr

**Notes:**
Behavioral optimization
- copy propagation in this case

## High-Level Synthesis

- push

- top

- alu

- top

- pop

- s

- instr

**Notes:**
Scheduling operations (_x0005_function allocation)

## High-Level Synthesis

- push

- top

- alu

- top

- pop

- s

- instr

**Notes:**
Register allocation

## High-Level Synthesis

- push

- top

- alu

- top

- pop

- s

- s

- s

- s

- s

- s

- s

- x

- x

- x

- x

- y

- instr

**Notes:**
Register Binding
- determines which register to store a value

## Serialization Tables

- Actions

- Scheduling Table

- Evaluation Table

- Term
- Eval

- Evaluation
- Requirements

**Notes:**
The same process may be manually dictated by the designer using Starfish’s serialization tables.
Similar to behavior tables, the vertical axis enumerates control steps and the horizontal access enumerates signals.
In this special case, control flow is linear so no decision table is necessary. 
The actions proceed sequentially without any branching.
Serialization tables add an "evaluation table” on the right side,  which show the cumulative symbolic interpretation of the signal updates.
The bottom row of the evaluation table shows the target requirements- the terms to which a valid schedule must evaluate.

## Serialization in Starfish

**Notes:**
In Starfish, the process begins with specifying the serialization subject, in this case, the alu-op row.
The initial serialization table shows the evaluation targets and an initial first step for all registered signals.
This next table adds two registers for holding intermediate values.
The designer proceeds by proposing successive updates.
When the schedule is valid--as determined by its symbolic evaluation--it may be reintegrated with the behavior table.

## Types in Starfish

- Multi-sorted structures with identities
- Enforces syntactic correctness
- Identity database for term manipulation
- Declarative structures
- Unbounded types; groups
- Enumerated types; booleans, states
- Parameterized types; stacks over data
- Inter-type functions and identities
- Special types and expressions
- Polymorphic tuples & selectors, bit vectors, integers

**Notes:**
Starfish implements an explicit type system based on multi-sorted structures.
This serves two purposes
This enforces syntactic correctness and exposes mistakes at an earlier stage.
Maintains an identity database for term-level manipulation.
There are 4 basic kinds of declarations:
- a single sorted structure with constants functions and identities -- models may be unbounded
- enumerated types where models correspond exactly to the constants
- Parameterized types such as stacks over a data type.
- Inter-type functions and identities.
Finally, the type system includes some distinguished types and expressions:
-polymorphic tuples and selectors, bit-vectors and integers

## Types in Starfish

- Type inferencing is necessary
- What’s the type of *empty-stack*?
- Type annotations
- Facilities for type translation
- One-to-one
- One-to-many
- Choice of representation contingent on current representation: ***A,R) ****R*
*Stateful refinement,* reference-state pattern

**Notes:**
Some degree of type inferencing is necessary because of type parameterization.
Some types are ambiguous such as empty-stack. It’s type may be inferred by its context.
Starfish implements a basic type inferencing heuristic. In case of inferencing failure, it is possible to provide hints through term annotation.

Finally, the type system permits declaration of data refinements
- This includes one-to-one refinements, where there is exactly one representation of each abstract type.
- one-to many refinements where there are multiple representations of each abstract type.
- And stateful refinements which allow multiple abstract types to be represented as references into a shared state.

## Stack to Array Transformation

- Apply to ‘s’

- Apply to instances of ‘top’

**Notes:**
In this example, Starfish applies a stack to array refinement to the signal s, as well as to instances of stack accessors.
s has been replaced by a random access memory m and an end-of-stack pointer i.
- push writes to the array and increments the pointer
- pop decrements the pointer
- tops are memory reads at the position before the pointer.

## Stack to Linked List

**Notes:**
In this example, there are two stack signals, s and tl.
The refinement replaces stack signals with references into a heap of cells. 
The cells chain together to represent stacks as linked lists. 
The result replaces s and tl with references into a shared state.
push constructs a new cell with the input value and pointer to old stack and increments the heap horizon pointer.
There is no garbage collection in this simplified model.
Pop returns one cell component, the pointer to the tail stack.
Top returns the other cell component, the cell’s value.
Starfish automatically serializes state access when there are concurrent stack accesses.
_x0016_

## Full StackCalc Decomposition

- Controller

- Memory

- ALU

**Notes:**
Combining the techniques of retiming, serialization, and data refinement, one may open up factorization opportunities.
This slide shows one possible derivation of the stack calculator which represents stacks as linked lists from a cell heap.
It splits into three components: a controller, a single ported memory and an ALU.
Notably, the stack implementation type has been split into separate components. 
-The stack pointer registers and heap horizon register reside in the controller.
- while the heap is implemented by a single-ported memory, made possible by designer specified serialization.

## Garbage Collector Derivation

**Notes:**
My thesis further examines two medium-scale examples which would not have been practical without the aid of a tool.
The first is a garbage collection routine.

## Garbage Collector Derivation

- Factor out
- abstract memories

- Encapsulate memory
- with function names

- Apply switch
- refinement

- Move sw
- into DT

**Notes:**
The algorithm is follows the stop and copy method, using an explicit swap of abstract memory signals to represent the exchange of old and new memory half-spaces.
The example factors out the abstract memory signals and algebraically manipulates the explicit signal swap into a reference swap implemented by a single flip flop.

## SECD Derivation

-  (letrec
-   ([exec
-    (lambda (s e c d)
-     (case (car c)
-      ('RTN (exec (cons (car s) (car d)) ...))
-      ('DUM (exec s (cons nil e) (cdr c) d))
-      ('AP (exec '()
- 	(cons (car (cdr s)) (cdr (car s)))
- 	(car (car s))
- 	(cons (cdr (cdr s))
- 	      (cons e (cons (cdr c) d)))))
-        ...
-       ('STOP (exec s e c d))))])
-     exec
-    ))

**Notes:**
The second example derives an architecture for an abstract SECD.
SECD is an abstract machine for specifying the operational semantics of LISP.
The derivation implements lists with a reference-heap model.
It introduces and instruction fetch stage, serializes memory accesses and adds registers for intermediate results.
The derivation dovetails with a previous study by Bob Wehrmeister which begins roughly at a level of detail corresponding to this derivation’s result. Wehrmeister’s derivation generates the physical organization level and was fabricated as an ASIC.

## Conclusion / Future Work

- Starfish expands factorization space
- Behavior table viewer and transformer
- Explicit type system and data refinement
- High Level Synthesis w/ Serialization tables
- Retiming
- Interface/Transaction Specification
- Integration with other tools
- DDD / Theorem provers / CASL
- Develop backends to synchronous targets
- FPGAs
- Multicore systems / real-time software

**Notes:**
In conclusion, I have implemented a tool which aids system factorization 
- with behavior tables
- an explicit type system
- data refinement
- serialization tables,
- and retiming.

There are several ways in which this work could be expanded
-- Behavior Tables were partially conceived to acommodate interface specification. The interface specification language ISL was developed by Kamlesh Rath and behavior tables were his medium of integration for the resulting protocols.
- A full design system based on Starfish must integrate with other tools.
 - DDD should be used used as a simulation environment for testing interfaces to hardware data paths and for its behavior transformations.
 - Starfish’s type system does not verify identites; it needs some kind of integration with theorem provers for specifying appropriate term theories.
 - My implementation of multi-sorted algebras is as naive as one can get and still do the transformations. There are mature tools -- such as CASL--for making algebraic specifications. Integration with these should be investigated.

Starfish would greatly benefit from the development of various backends into synchronous targets such as FPGAs or even into a synchronous software platform for multi-core systems or real time software.

That conclude my talk. Once again I’d like to thank the NASA formal methods group for their sponsoship of my dissertation research. I’d be happy to take any short questions.