Electronic Design Automation (EDA) is a crucial application domain for our constraint solving technologies. We develop advanced formal verification and testing tools to ensure the reliability and correctness of hardware designs.

Our Research Focus

Logic Equivalence Checking (LEC)

Verify the logical equivalence between different representations of circuit designs:

• RTL to gate-level equivalence checking
• Sequential equivalence verification
• Combinational equivalence checking
• Abstraction techniques for scalability
• Incremental verification methods

Model Checking (MC)

Bounded Model Checking (BMC)

Verify properties within bounded execution steps using SAT/SMT solvers:

• Efficient encoding techniques
• Bound selection strategies
• Property-specific optimizations
• Counterexample generation
• Incremental BMC algorithms

Property Directed Reachability (PDR)

Advanced formal verification through property-directed analysis:

• Forward/backward reachability
• Invariant generation
• Abstraction refinement
• Proof obligation management
• Parallel PDR algorithms

Automatic Test Pattern Generation (ATPG)

Generate test patterns for detecting manufacturing defects:

• Stuck-at fault testing
• Path delay fault testing
• Transition fault testing
• Test compression techniques
• Fault simulation and grading

The tools regarding EDA are all released as open-source, and can be found at Software Tools page.