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
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)
Last updated