RT DF A1 Zhang, Hongce. T1 The Hardware-Software Interface for Systems-on-Chip: Formal Modeling and Modular Verification