Research Interests : Complementary Synthesis
In communication chip design projects, one of the most risky and lengthy jobs is to design and verify varies complementary cores,such as coder/decoder, framer/deframer, sliding window mechanism, and so on.
To ease this job, we try to automatically synthesize a circuit's complementary circuits, such as synthesizing a decoder from an encoder.
Selected Publications:
This is the first paper about complementary synthesis. It determines the decoder's existence by checking whether the encoder's input letter can be uniquely determined by its output sequence. And it characterizes the decoder's Boolean function with ALLSAT based on XOR discovering.
This paper improves ICCAD'09 by speeding up the characterizing algorithm with unsatisfiable core extraction.
This paper proposes the first halting algorithm that determines the decoder's existence.
This paper proposes a faster halting algorithm that falsifies the decoder's existence by detecting loops in the encoder's state transition sequences.
This paper proposes the first algorithm that infers assertions for complementary synthesis, by iteratively detecting and removing those configuration values leading to the decoder's nonexistence.
Research Interests: Counterexample Explanation
Model checking technology is widely employed to verify software and hardware system. One of its major advantages in comparison to such method as theorem proving is the production of a counterexample, which explains how the system violates some assertion.
However, it is a tedious task to understand the complex counterexamples generated by model checker. Therefore, how to automatically extract useful information to aid the understanding of counterexample, is an area of active research.
Selected Publications:
Other publication in Chinese instead of English, including my PhD thesis.
Book Project:
Research Support
Software Download:
Please refer to
Related:
Teaching:
