Research Topics
1. Verification for Embedded System Designs at Multiple
Levels of Abstraction
- Formal verification checks the entire state space of a design
to verify some specified property without any uncertainty.
Specification at the system level makes formal verification possible.
Designers can prove a property of a specification by formally
specifying the property in some logic (e.g. Linear Temporal Logic (LTL))
and use a formal verification tool (e.g. the model checker SMV and
Spin) to run the exhaustive verification. In general, system level
design specifications are automatically abstracted and transformed
to verification models for formal verification using existing tools.
Main contributions:
- X.
Chen, H. Hsieh, F. Balarin, and Y. Watanabe, "Formal
Verification for Embedded System Designs", Journal of Design Automation for Embedded Systems, Special Issue of
Covalidation of Embedded Hardware/Software System , edited
by Ian G. Harris, Kluwer Academic Publishers, 8(2/3),
June/September 2003. [PDF]
- X.
Chen, H. Hsieh, F. Balarin, and Y. Watanabe, "Case
Studies of Model Checking for Embedded System Designs", in Proceedings of the Third International Conference on Application of
Concurrency to System Design (ACSD '03), Guimaraes, Portugal,
June 2003. [PDF]
- Project: a formal verification backend tool in
the Metropolis design environment utilizing
the model checker
Spin.
|
- Simulation verification becomes the
primary means for verification, as the designs are refined to lower level
specifications and the
complexity of formal verification quickly overwhelms the existing
automatic tools. Compared to formal
verification, simulation verification is much more efficient,
but its confidence mainly depends on the design of test cases.
Simulation monitors can be automatically generated from functional and
performance assertions to verify the simulation traces.
Main contributions:
- X. Chen, A. Davare, H. Hsieh, A. Sangiovanni-Vincentelli, and Y.
Watanabe, "Simulation Based Deadlock Analysis for System
Level Designs", to appear,
in Proceedings of Design Automation Conference (DAC
'05), Anaheim, CA, June 2005.
- X. Chen, H. Hsieh,
F. Balarin, and Y. Watanabe, "Logic of Constraints: A
Quantitative Performance and Functional Constraint
Formalism",
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,
23(8), August 2004. [PDF]
- X.
Chen, H. Hsieh, F. Balarin, and Y. Watanabe, "Automatic
Trace Analysis for Logic of Constraints", in Proceedings of Design
Automation Conference (DAC '03), Anaheim, CA, June 2003. [PDF]
- Project: PAC ( Performance Assertion Checker) - an automatic
checker generation tool for LOC (Logic of Constraints).
|
- Combination of simulation verification and
formal verification can take advantage of the good features from both
verification techniques, i.e. efficiency and high confidence. The
general idea is to use simulation to search for probable design
violations and isolate potential problems to a small part of the
design. Then, only that part of the design is feed to a formal
verifier to exactly identify and locate the design errors.
- Project: a deadlock detection mechanism for system level designs with
combination of simulation and formal verification techniques.
|
2. System-Level Design Frameworks and Methodologies
- Metropolis project
is developing a next-generation integrated design environment for heterogeneous
embedded systems. The system-level platform-based design methodology
and various models of computation (MoC) are natively incorporated in
the Metropolis design framework. Xi Chen is an active member of
Metropolis project team and has contributed to several projects for
both the development of Metropolis infrastructure and verification
backend tools.
Main contributions:
- Project: a compile-time network structure and constraint elaboration tool in
the Metropolis design environment.
- Project: a template resolution mechanism for the system-level modeling
language Metropolis Meta-Model.
- Project: simulation based refinement checking for
system level designs.
|
3. Architecture Modeling, Verification and Exploration
- Due to the heterogeneity of modem computing systems and the design
methodology of function-architecture orthogonalization, high
level architecture modeling becomes an very important research topic
and directly determines its verification and exploration processes. An
assertion-based automatic architecture verification, power/performance
analysis and design exploration methodologies are proposed and
experimented in the network processor architectures with low power techniques.
Main contributions:
- J. Yu, W. Wu, X. Chen, H. Hsieh, J. Yang, and F. Balarin.
"Assertion-Based Design Exploration of DVS in Network
Processor Architectures", in
Proceedings of Design Automation and Test in Europe (DATE '05),
Munich, Germany, March, 2005.
- X. Chen, Y. Luo, H.
Hsieh, L. Bhuyan, and F. Balarin, "Utilizing Formal
Assertions for System Design of Network Processors",
in Proceedings of Design Automation and Test in Europe
(DATE '04), Designers' Forum, Paris, France, February 2004. [PDF]
- Y. Luo, L. Bhuyan,
X. Chen, "Shared Memory Multiprocessor Architectures for
Software IP Routers",
IEEE Transactions on Parallel and Distributed Systems,
14(12), December 2003. [PDF]
- Project: architecture verification and exploration
with orthogonalization of function and architecture in the
platform-based design.
|
| [Publications] [Presentations] |
Academic Activities
- Served as a paper reviewer for
|
|
|
Research Resources
Conferences:
Journals:
Related Tools and Documentations:
-
FoCs
(Formal Checkers) - an automatic checker generation tool for PSL/Sugar2.0
developed by IBM.
-
OpenVera
- an open source hardware verification language originally proposed by
Synopsys.
-
Metropolis
- an integrated design environment for heterogeneous systems.
-
NePSim -
a cycle-accurate network processor simulator with power evaluation
capability.
-
PAC
(Performance Assertion Checkers) - an automatic
checker generation tool for LOC (Logic of Constraints).
-
PSL
(Property Specification Language) - a formal hardware assertion language
standardized by Accellera.
-
SMART
- Stochastic Model checking Analyzer for Reliability and Timing.
-
Spin
- a formal verification tool for distributed software systems.
-
SystemVerilog
Assertions - an assertion verification language extension for
SystemVerilog standardized by Accellera.
|
