MLIR+EqSat

GPU accelerated decision optimization

verl: Volcano Engine Reinforcement Learning for LLMs

GPU-based logic synthesis tool

EDA wiki

Rewrite Rule Inference Using Equality Saturation

Python version of tools to work with AIG formatted files

py-aiger: A python library for manipulating sequential and combinatorial circuits encoded using `and` & `inverter` gates (AIGs).

Integer Multiplier Generator for Verilog

Lean4 formalization of Gröbner basis (WIP)

Graph Neural Network Library for PyTorch

DHLS (Dynamic High-Level Synthesis) compiler based on MLIR

ACL2 System and Books as Maintained by the Community

Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays and uninterpreted functions and their combinations. Its name …

A General-purpose Parallel and Heterogeneous Task Programming System

ABC: System for Sequential Logic Synthesis and Formal Verification

Research paper based on or related to ABC.

LLMs as Copilots for Theorem Proving in Lean

Tactics for discharging Lean goals into SMT solvers.

SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows

RISC-V Formal Verification Framework

A (WIP) equality saturation tactic for Lean based on egg.

An awesome list of e-graph resources

本人的科研经验

Connecting Bitwuzla to LeanSAT

An HLS Complier for PyTorch/C/C++ Codes into HLS Dataflow Designs

All in one vscode plugin for HDL development