Home Publications Presentations Teaching Resume

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

Research Resources



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.

Copyright 2004-2006 Xi Chen - Last Update: 10/30/2005