Affordable Access

Formal Analysis of Electronic System Level Models using Satisfiability Modulo Theories and Automata Checking

  • Chang, Che-Wei
Publication Date
Jan 01, 2015
eScholarship - University of California
External links


For a system-level design which may be composed of multiple processing elements runningin parallel, various kinds of unwanted consequences may happen if the systemis constructed carelessly. For example, deadlock may happen if improper executionorder and communication between processing elements is used in the system. Anotherproblem which may be caused by the concurrent execution is race condition, asshared variables in the system-level model could be accessed by multiple concurrentthreads in parallel. Those unwanted behaviors definitely have negative influence onthe functionality of the system. Furthermore, the functionality is not the only concernin system design as timing constraints are critical as well. If the system cannotfinish the job within timing constraints, it is still considered an unwanted design. Toaddress these issues, we propose two formal analysis approaches in this dissertationto analyze three types of properties we discussed above, which are1). liveness,2). satisfiability of timing constraint, and3). May-Happen-in-Parallel access.These two approaches are based on Satisfiability Modulo Theories (SMT) and UPPAALautomaton model respectively. We run these two approaches on our in-housesystem models, including a JPEG encoder, MP3 decoder, AMBA AHB and CANbus protocol models. The experimental results show our approaches are capable ofanalyzing those properties meeting our expectation within reasonable analysis time.

Report this publication


Seen <100 times