Simulation remains a predominant method for design verification, but requires extensive processing time. One of the ways to shorten the simulation time is to perform distributed parallel simulation, where the design is decomposed into several modules and each module is simulated on a different machine or a processor. However, distributed simulation suffers from serious communication and synchronization overhead, which significantly reduces or negates the potential performance gain offered by parallel simulation. An entirely new approach to parallel simulation has been recently proposed, aimed at completely eliminating the communication and synchronization overhead between processors. In contrast to traditional (spatial) distributed simulation, which partitions the design into multiple modules and simulates all modules in parallel, the proposed multi-threaded simulation partitions single simulation into multiple simulation runs in the temporal domain.

The main idea of Parallel Temporal Simulation is described in the following paper . The goal of this project is to run several experiments by performing parallel gate-level timing simulation of a synthesized design, using the original RTL design as a reference point, and analyze the results.

Specifically, it involves the following steps:

1. Finding a set of suitable example of RTL designs (benchmarks) written in verilog along with simulation testbenches.
2. Synthesizing the original RTL design using logic synthesis tools, such as Synopsys' Design Compiler (for standard cells) or Altera' Quartus II (for FPGAs or PLDs), followed by physical synthesis, where all the gates/LUTs are placed and routed. The result is the final mapped netlist (in verilog) and the SDF file, containing timing details of the synthesized netlist (gates and interconnections).
3. Simulating the original RTL design with a given TestBench (to be provided).
4. Using formal verification tool, such as Formality (Synopsys) to find matching points between the RTL and gate-level signals at the register boundaries (check points).
5. Using a prototype software for parallel temporal simulation (to be provided), perform simulation of the gate-level designs using the names of signals at check points.
6. Analyze the results by recording the total time required for simulation as a function of the number of simulators/processors; time overhead for first (RTL) simulation run, etc.

Continuation of this project can easily lead to a good MS thesis project.

One of the tasks of formal verification is to verify the equivalence of the design between two consecutive design phases, for example: between the original behavioral design (written in C or behavioral HDL) and the synthesized RTL design (written in structural HDL) produced by the high-level (architectural) synthesis tool; or between the RTL design and the synthesized gate-level design, etc. This task is very difficult, because of the disparity in the level of details provided by the two abstractions.

The purpose of this project is to analyze the degree of difficulty of the verification process as a function of certain parameters and the RTL structure of the synthesized designs. The following observations have been made in literature regarding the relationship between the results of high-level synthesis and verification: (1) increased resource sharing introduces Multiplexers, which are difficult to verify by current verification tools; (2) creation of new signal names that do not match those from original design complicates the task of finding match points, on which verification relies heavily; (3) increased latency increased sequential depth of the design, which naturally complicates the verification task. We would like to confirm or verify these observations by analyzing the synthesized RTL designs in terms of their structure and composition, and observing their effect on the equivalence verification performed by a commercial formal verification tool, Formality (from Synopsys). The result of this work can then be used in behavioral synthesis by favoring "verification-friendly" transformations during the synthesis. Specific tasks of this project include:

1. Finding a set of suitable examples of behavioral designs (benchmarks) written in C or behavioral HDL. The high-level synthesis system GAUT has a list of such designs from digital signal processing domain.
2. For each design, performing RTL synthesis using high-level synthesis tool, such as GAUT, with varying objectives (latency, resource) and constraints (on resources, latency, clock cycle, etc.). Both pipelined and non-pipelined synthesis should be performed.
3. Characterizing the synthesized designs by their execution time (latency), number and type of resources, amount of steering logic, registers, etc.
4. Performing equivalence checking of each synthesized RTL design w.r.t. its behavioral design and recording time and verification difficulty reported by the verification tool. We plan to use formal verification tool Formality (Synopsys) for this purpose.
5. Analyzing the results by comparing the verification time for different designs.

This project can probably lead to a conference paper.

This project is related to formal verification project listed above. In this case we are interested in learning how to assist the verification tool (such as Formality of Synopsys) by providing a record of transformation steps performed during the behavioral and architectural synthesis to the verification tool.

The following simple experiment explains the main idea. Consider a simple computation F1 = A*B + A*C, synthesized into a gate level design, G1. This computation can be transformed (during behavioral synthesis) into an equivalent expression, F2 = A*(B+C), and subsequently synthesized into a gate level design, G2. Formality can verify equivalence of F1 w.r.t. G1, or of F2 w.r.t. G2, in a matter of seconds. However, for bit-widths larger than 12 bits, this verification problem becomes unsolvable when comparing F1 with G2 or F2 with G1. (In fact, even the equivalence between F1 and F2 cannot be established by Formality for datapaths larger than 12 bits, because both representations are first synthesized into standard gate-level netlists, and the two gate-level netlists are verified for equivalence). The reason for this inefficiency is that the verification tools strongly rely on finding equivalence between internal "match points", such as the outputs of two multipliers of F1 and G1, or the output of a single multiplier in F2 and G2. However, the tools experience serious difficulties in the absence of such match points, which is the case when comparing designs F1 with G2, or F2 with G1.

It would be interesting to learn how the information about the behavioral transformations (such as F1 --> F2) which result in equivalent behaviors, can be passed to the verification tool. This is a more ambitious project and requires learning how to interface with Formality, or similar tools, how to use existing behavioral verification tools, such as TEDify (currently limited to simple polynomial expressions), or how to develop your own formal verification/equivalence tool to effect such a verification for behavioral designs.

This project can easily lead to a M..S. or Ph.D. thesis.