随着大规模集成电路技术和EDA技术的发展，片上系统(SoC)成为嵌入式系统的发展方向。片上系统带来了一些技术上的问题，对设计正确性的要求更加迫切。如何减少系统设计中的错误，提高系统设计的可靠性成为备受关注的问题。传统的设计方法由于系统规范缺少精确性，而验证也不能提供百分之百的覆盖，出错的可能性很大。为了解决这个问题，形式化方法被应用在软硬件设计中。所谓形式化方法，就是利用严格的数学方法，从给出系统设计的规范开始并逐步地推导或者验证系统的方法。 投影时序逻辑PTL(projection temporal logic)是一种具有离散的时间模型的时序逻辑，可处理同时具有顺序和并行的复合计算，为复杂系统的设计提供了强大的规范和证明技术。程序设计语言Extended Tempura是PTL的一个可执行的子集，可用来开发系统的原型，对系统进行模拟。 本文介绍了形式化方法及投影时序逻辑和其可执行子集的基本内容，讨论了PTL对SoC不同层次的描述方法，对把状态图转换为PTL公式的问题进行了探讨，在此基础上提出基于PTL的SoC设计方法。这种方法强调系统设计中的形式描述和验证，通过在不同的设计阶段引入形式化的方法，提高系统设计的可靠性。