> For the complete documentation index, see [llms.txt](https://zeju.gitbook.io/lcm-team/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://zeju.gitbook.io/lcm-team/forgeeda/practical-downstream-tasks/practical-eda-applications.md).

# Practical EDA Applications

## RTL Synthesis

#### Task Statement

We performed a complete synthesis flow starting from **RTL code repository** input, which included logic optimization and technol- ogy mapping, to generate gate-level netlists.

#### Dataset

[Dataset](/lcm-team/forgeeda/dataset.md#rtl-code-repository)

#### Evaluation Metrics

Area / Delay (ps): reported by the abc STA command *stime*

#### Results

Tools: DCU (Design Compiler ® compiler\_ultra) / Yosys

<figure><img src="https://204291402-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2FqpjfvyQt0RAeOzMVWp4g%2Fuploads%2FfyPnzXbwxRkT7vrGEWmJ%2Fimage.png?alt=media&amp;token=707f0722-feda-43a5-be18-baaf430411f8" alt=""><figcaption></figcaption></figure>

## AIG Technology Mapping

#### Task Statement

We use the initial AIG as input to generate mapped netlists and evaluated the mapping efficiency based on netlist area and delay.

#### Dataset

[Dataset](/lcm-team/forgeeda/dataset.md#and-inverter-graph-aig)

#### Evaluation Metrics

Area / Delay (ps): reported by the abc STA command stime

#### Results

Tools / Commands: abc (\&nf), abc (dch+\&nf), abc (map), DCU

<figure><img src="https://204291402-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2FqpjfvyQt0RAeOzMVWp4g%2Fuploads%2FZWcL5VOXLS6T2yTCGrVM%2Fimage.png?alt=media&amp;token=fbff3ea9-11e5-4487-ad67-9f499ffa6f0c" alt=""><figcaption></figcaption></figure>

## AIG Optimization

#### Task Statement

Convert an initial AIG into a more optimized form, is assessed with area and delay metrics.

#### Dataset

[Dataset](/lcm-team/forgeeda/dataset.md#and-inverter-graph-aig)

#### Evaluation Metrics

Area: Number of nodes / Delay: Number of logic level

#### Results

Tools / Commands: resyn2rs, compress2rs, if -g, orchestrate

<figure><img src="https://204291402-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2FqpjfvyQt0RAeOzMVWp4g%2Fuploads%2FWFCww2xP1QvAsWfbiSZu%2Fimage.png?alt=media&amp;token=784d9264-5b93-4464-84c7-ac095bfb29d7" alt=""><figcaption></figcaption></figure>

## Logic Equivalence Checking

#### Task Statement

We target on Logic Equivalence Checking (LEC) task, which determines whether two given designs are functionally equivalent. Build upon our proposed dataset, a possible use-case is the construction of LEC instances to benchmark SAT solvers.

We generate equivalent circuits, which are then transformed into miter instances proven to be unsatisfiable. Additionally, we create non-equivalent circuits by modifying the AIG structure, resulting in satisfiable miter instances that demonstrate inequivalence.

#### Dataset

[Dataset](/lcm-team/forgeeda/dataset.md#and-inverter-graph-aig)

#### Evaluation Metrics

Time: Solving time / #Solved: Number of solved instances

#### Results

Solvers: Kissat / ABC Circuit-based Solver (csat) / Minisat (dsat)

<figure><img src="https://204291402-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2FqpjfvyQt0RAeOzMVWp4g%2Fuploads%2FMAfUM6WnP424do2BZazQ%2Fimage.png?alt=media&amp;token=e4de155a-df5c-4d3b-8faf-510af078fe14" alt=""><figcaption></figcaption></figure>