LCM-Team
  • Datasets of Large Circuit Model
  • DeepCircuitX
    • Introduction
    • Source RTL code
    • RTL code annotations by GPT
    • Other modality information
    • RTL-Language Data for LLM Finetune
    • Data for PPA prediction
    • Tasks, experiments and results
      • LLM Finetune Results
      • PPA Prediction Results
  • ForgeEDA
    • Introduction
    • Data Preparation
    • Dataset
    • Practical Downstream Tasks
      • Practical EDA Applications
      • AI for EDA Applications
  • ForgeHLS
Powered by GitBook
On this page
  • RTL Synthesis
  • AIG Technology Mapping
  • AIG Optimization
  • Logic Equivalence Checking
  1. ForgeEDA
  2. Practical Downstream Tasks

Practical EDA Applications

PreviousPractical Downstream TasksNextAI for EDA Applications

Last updated 2 months ago

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

Evaluation Metrics

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

Results

Tools: DCU (Design Compiler ® compiler_ultra) / Yosys

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

Evaluation Metrics

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

Results

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

AIG Optimization

Task Statement

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

Dataset

Evaluation Metrics

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

Results

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

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

Evaluation Metrics

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

Results

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

And-Inverter Graph (AIG)
And-Inverter Graph (AIG)
And-Inverter Graph (AIG)
RTL Code Repository