Scott R. Little
little@cs.utah.edu
Resume
The main focus of the Myers research group is modeling and analysis of hybrid and biological systems. My dissertation work explores the modeling and formal verification of hybrid systems with emphasis on analog/mixed-signal circuits as the motivating examples for the work. We have developed novel methods for automatic model generation from a set of simulation traces of the system. The model generation system produces labeled hybrid Petri nets, Verilog-AMS, and VHDL-AMS. These automatically generated models are used for automatic verification of desired system properties. The verification method finds the reachable state space of the hybrid model. This state space exploration is complicated by the need to represent continuously varying quantities. To increase the efficiency of the state space exploration my algorithm uses a restricted form of convex polyhedra to conservatively represent the state space. This work promises to find complex bugs not easily exposed by a simulation-only methodology. Furthermore, automatic abstract model generation can produce abstract models suitable for system-level simulation that perform up to 40x faster.
For more information regarding our research please see my research page.
S. Little, Efficient Modeling and Verification of Analog/Mixed-Signal Circuits Using Labeled Hybrid Petri Nets Dissertation pdf
S. Little, D. Walter, K. Jones, and C. Myers, Analog/mixed-signal circuit verification using models generated from simulation traces, in International Symposium on Automated Technology for Verification and Analysis (ATVA), October, 2007, pp. 114-128. pdf slides
D. Walter, S. Little, and C. Myers, Bounded model checking of analog and mixed-signal circuits using an SMT solver, in International Symposium on Automated Technology for Verification and Analysis (ATVA), October, 2007, pp. 66-81. pdf
D. Walter, S. Little, N. Seegmiller, C. Myers, and T. Yoneda, Symbolic model checking of analog / mixed-signal circuits, in Asia and South Pacific Design Automation Conference (ASPDAC), January, 2007. pdf
S. Little, N. Seegmiller, D. Walter, C. Myers, and T. Yoneda, Verification of analog/mixed-signal circuits using labeled hybrid Petri nets, in International Conference on Computer-Aided Design (ICCAD), November, 2006. pdf slides
H. Zheng, C. Myers, D. Walter, S. Little, and T. Yoneda, Verification of timed circuits with failure directed abstractions, in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), 25(3): 403--412, March, 2006.
S. Little, D. Walter, N. Seegmiller, C. Myers, and T. Yoneda, Verification of Analog and Mixed-Signal Circuits Using Timed Hybrid Petri Nets, in International Symposium on Automated Technology for Verification and Analysis (ATVA), November, 2004. © Springer-Verlag pdf slides
Please see my publications page for a complete list of my publications.
Last modified November 29, 2007