Temporal Logic

CTL*

CTL vs. LTL

Model checking

Symbolic Model Checking



Kripke Structure: M = (S,R,L)



- transform a FSM with guarded transition to M, by modeling original transitions as states in M



you can unroll M to get an execution tree



formulas and logic:

- Ef, Af

- Xf, Ff, Gf, fUg

-

Multi-level Logic Synthesis

RTL === (logic synthesis) ==> netlist

Decomposition
Extraction
Factoring
Substituttion
Collapsing/Flattening

F = d * q + r

algebraic expressions
- product
- divisor

Boolean vs. Algebraic

What's an algebraic expression?
What's a cube-free expression?
What's a primary divisor?

Weak division

Rectangle Covering

What's a kernel?
- what is the level of a kernel?
What's a co-kernel?
- how to extract kernels and co-kernels from a function?

Retiming

Leiserson and Saxe

- moving registers to minimize area, time (clock period), or both (given one is constrained)
- it is done under several (untrivial) assumptions

- D matrix - path delay matrix
- W matrix - path matrix for min #register for any pair of vertices.

Floyd-Warshall

Bellman-Ford
- n - 1 iterations
- an extra iteration to check negative weigh cycle
- d(v) < d(u) + w(u,v) <== relaxation

clock skew vs. retiming

Peripherial retiming
- use retiming to augment the circuit
- and perform optimization on the combinational parts

The initial value problem
- decreasing the number of registers, then there are less initial values
- if initial values determine the behavior for the circuit, then retiming may not preserve the original circuit

Technology Binding (DAGON)

Technology independent mapping of circuit to cell library components. They called this technique DAG rewriting. The complexity of finding a minimal match, or cover, is NP-complete.

It assumes non-local optimizations are done at global optimization or decomposition stages.

Two essential steps
- partitioning into forest of trees (special case of DAG)
- partitioning split any fanout > 1 and is O(G).
- optimally match trees to patterns based on cost (e.g. time, area, or both)
- matching is done with twig (based on Aho-Corasick) is O(T).

It borrows from code generator in compilers
- the use of grammar to specify families of patterns
- peehole optimizer to handle cross-tree boundary opt.

Quality enhancements:
- use annotations to export local information globally
- e.g. inverse, signal, and fanout

--------------------------------------------

(circuit) base function ==> subject graph

(library) base function ==> pattern graphs

Partitioning

- single fanout - split multiple fanout

- single cone - traverse from sink nodes

- may have overlap clustering because of the input-output constraint from patterns

Dynamic programming

- store intermediate best result for each stage

- at each new stage, compute best matches using previous best results

Linear Algebra

adjoint, or adj(A), is the transpose of the cofactor matrix of A.

Crame's Rule:
- solves AX = B
- xi = det(Ai) / det(A), where Ai is replacing the i-th column with B.

vs. Gaussian Elimination
- Crame's Rule requires computing (n+1) determinants
- computing each determinant requires as much work as solution using G.E.

Jacobian is the det(M'), where M' is the partial derivative matrix of M containing F(f1,....,fn).


Vector:
- v dot product,
- projection, +, -, norm
- span of vector(s)