顾及BDS-3星钟约束的GNSS超快速轨道钟差解算方法

BDS-3高稳定星载原子钟作为北斗星座的显著技术优势,在GNSS数据处理中尚未得到充分利用。针对严格时效性限制下GNSS超快速轨道钟差参数精度受限问题,本文提出顾及BDS-3星钟约束的GNSS超快速轨道钟差解算方法。首先,以GNSS轨道钟差参数间相关性为基础,构建顾及BDS-3星钟参数特性的GNSS定轨模型;然后,基于GNSS精密钟差产品,分析星钟约束对GNSS轨道钟差参数精度的影响规律;最后,为克服预报钟差精度与约束筛选对定轨影响,建立BDS-3星钟建模与GNSS超快速轨道钟差估计的同步处理方法。试验结果表明,在BDS-3星钟参数最优约束下,BDS-3与GPS轨道钟差精度可分别提升27.5%、5.1%和20.2%、5.2%;且较传统BDS-3星钟单历元处理策略,基于BDS-3星钟建模与GNSS超快速定轨同步处理方法,GNSS超快速轨道钟差精度可分别提升至4.8%与34.2%,轨道精度实现了毫米级改善。因此,顾及BDS-3星钟约束的GNSS超快速轨道钟差解算方法可有效对BDS-3高稳星钟信息模型化,并实现GNSS超快速轨道钟差精度的优化处理。

安全关键的信息物理系统中时序行为的组合与精化

信息物理系统(cyber physical systems, CPS)通常被应用于安全关键的场景中,需要进行实时监控,并计算反馈信息,实现对外部环境的自动控制与管理.基于模型驱动的开发方法是针对实时的、异构的CPS进行开发的,而模型的可组合性是其中的核心关键点.针对时序行为的可组合问题,首先通过时序约束语言(clock constraint specification language, CCSL)建立系统的时序行为需求模型,在此基础上通过迁移系统描述CCSL的时序行为语义,并给出其组合操作方法及可组合性的形式化定义.进一步地,对时序行为进行精化操作,给出从时序行为需求模型到任务执行模型的转换方法.同时,基于L*方法对模型行为进行学习,实现组合验证以缓解状态爆炸问题,并验证精化后模型的可组合性.最后通过仿真实验及主从智能小车实例对精化与验证方法进行评估.相关数据显示,精化与组合验证方法在处理时间和内存使用上具有一定的性能优势.

RapidIO交换芯片的静态时序约束设计

静态时序分析是目前通用的芯片时序验证的重要方法,其依赖于时序模型和时序约束。时序约束是检验设计电路时序的准则,好的时序约束可以正确地体现芯片的设计需求。针对RapidIO交换芯片中存在的多时钟域构成、高速通道的高速时钟频率要求,2x/4x绑定模式下多lane时钟同步等的特殊要求,以及较多的跨异步时钟处理存在的问题,文中提出一种多分组的全芯片时序约束,通过设置时钟定义、时钟组定义、端口延迟定义、时序例外和虚假路径等,以及修正和优化必要的setup time/hold time违例,解决RapidIO交换芯片静态时序分析中的时序违例等时序问题,实现时序收敛的目的。实验验证及流片测试结果表明,所有时序路径均满足时序要求,RapidIO芯片的时序约束设计正确、完备。

铁路信号安全关键软件形式化建模

针对现行建模方法不能满足铁路信号系统安全关键软件的时钟约束需求和模型复杂度较高的问题,分析SyncCharts建模方法,针对其缺少形式化规范和时钟约束的问题,扩展出具有时钟属性的Timed SyncCharts建模方法。首先,采用Z语言系统地给出了Timed SyncCharts的形式化定义;其次,结合Timed SyncCharts的组件元素,确定Timed SyncCharts的宏步转移机制;然后,提出将Timed SyncCharts转化为Kripke结构的规则,保证了模型分析的可行性;最后,建立计算机联锁软件道岔定位需求的Timed SyncCharts模型,证明该方法的可行性和有效性。

基于28nm工艺的CCOpt技术高效时钟树设计

为了设计合理高效的时钟树网络,对建立和保持时间约束以及时钟偏差进行分析,基于28 nm工艺设计了一款高速数字芯片,采用Innovus工具实施布局布线,在时钟树综合(CTS,clock tree synthesis)阶段采用CCOpt(clock concurrent optimization)技术,合理利用时钟偏差,同时优化时钟路径和逻辑路径,对时钟网络进行优化,并考察时钟树延时、时序和时钟网络功耗等指标。结果标明:与传统CTS技术相比,采用CCOpt技术时,最差时序违例和违例路径数量减少50%;布局布线时间减少2 h;芯片时钟网络内部互连功耗减少55%,泄漏功耗减少80%,有效提高了数字芯片的性能。

一种CDC信号滑动窗口时序分析方法

异步时钟域设计中CDC信号的时序分析及收敛是超大规模高频数字电路设计功能正确的重要保证。为了减少设计面积,提出了一种CDC信号滑动窗口时序分析方法,该方法在每种corner的每条CDC通路上单独设置适当的时序约束窗口进行时序计算与分析,有效避免了常用的固定约束分析方法由于约束条件过严导致的虚假时序违反及不必要的时序修复,而使设计面积增大的问题,减轻了CDC电路的后端设计工作量。在16 nm工艺下的实验结果表明,该方法在时钟树偏差较大时与固定约束分析方法相比显著节省了设计面积。

铁路信号系统软件测试建模方法

针对铁路信号系统软件测试模型不能系统地描述测试需求的问题,提出风险时间状态机建模方法.首先,分析铁路信号系统软件测试建模的特点,并提出建模需求;然后,以有限状态机理论为研究基础,在有限状态机的变迁和状态中分别扩展出时钟和风险等级元素,提出风险时间状态机建模方法,满足功能逻辑、时间约束和风险等级3个方面的建模需求,采用Z规格说明语言给出风险时间状态机的形式化定义和格局转移机制;最后,以计算机联锁系统中的道岔转换功能为例,建立风险时间状态机测试模型,并与时间自动机建模方法进行了对比,结果表明,建模方法上,所建立风险时间状态机比时间自动机节省62%的变迁数,描述能力更强,能够满足铁路信号系统软件测试的建模需求.

面向无人驾驶时空同步约束制导的安全强化学习

无人驾驶系统综合了软件和硬件复杂的交互过程,在系统设计阶段,形式化方法可以保证系统满足逻辑规约和安全需求;在系统运行阶段,深度强化学习被广泛应用于无人驾驶系统决策中.然而,在面对没有经验的场景和复杂决策任务时,基于黑盒的深度强化学习系统并不能保证系统的安全性和复杂任务奖励函数设置的可解释性.为此提出了一种形式化时空同步约束制导的安全强化学习方法.首先,提出了一种形式化时空同步约束规约语言,接近自然语言的安全需求规约使奖励函数的设置更具有解释性.其次,展示了时空同步自动机和状态动作空间迁移系统,保证强化学习的状态行为策略更加安全.然后,提出了结合形式化时空约束制导的安全强化学习方法.最后,通过无人驾驶汽车在高速场景变道超车的案例,验证所提方法的有效性.

带时间约束的LTL性质的模型检测的实现

针对当前的模型检测工具不能对时间自动机直接检测带时间约束的线性时序逻辑性质的问题,对带时间约束的线性时序逻辑性质的模型检测进行了研究。带时间约束的线性时序逻辑公式转Büchi自动机后,性质自动机的迁移边上含有了时间约束,在对性质自动机和模型自动机的复合进行空性检测时,通过使用不同方法对如何获取性质自动机迁移边上的时间约束进行了研究,实现了对带时间约束的线性时序逻辑性质的检测,扩展了工具CATV的检测范围,方便了用户的使用。

采用CCSL仿真与分析反应式系统事件链模型

目前,能够对汽车电子领域中复杂嵌入式系统安全关键软件功能建模和时间分析的方法尚在研究中,而这些系统作为反应式控制系统,应该确保其具有准确的、可分析的时间行为.时钟约束规范语言CCSL是反应式系统的标准描述语言中描述时钟约束的规范语言.采用CCSL时钟模型对事件链模型中的时间约束进行分析与仿真;设计了事件链模型到时钟模型的转换规则,将事件链中的时间约束表达为时钟模型的时间约束;使用CCSL仿真工具Time Square对转换得到的时钟模型进行仿真分析,验证事件链是否满足相应的时间约束.

基于异步时钟的SoC功耗约束测试调度优化

测试调度是一种能有效减少片上系统(system-on-chip,SoC)测试耗时(test application time,TAT)以降低测试成本的经典技术.然而,随着功耗问题的日益加剧,功耗约束成为测试调度中必须考虑的重要问题.可以调节各测试周期长度的异步时钟测试在对单个电路进行测试用时优化时效果显著,但直接将其应用于SoC测试调度并非总能获得最优的调度结果,使用传统测试调度模型往往会产生明显非最优的结果.在结合图论中团(clique)的概念,并分析异步时钟机制的特点后,提出一种将异步时钟特性应用于功耗约束SoC测试调度的方案.使用测试兼容图(test compatibility graph,TCG)和混合整型线性规划(mixed integer linear programming,MILP)建立相对应数学模型,理论分析和在ITC02基准SoC集上的模拟实验结果表明,该方案能有效地减少测试耗时.

ASIC中时钟MUX电路结构时序约束的方法分析

时钟切换在数字集成电路设计中十分常见,对时钟MUX电路结构的正确时序约束显得非常重要。介绍几种常见的时钟MUX电路结构,使用业界标准Synopsys设计约束(SDC)对不同MUX电路结构分别给出几种时序约束方法。详细分析了各MUX结构约束的原理。给出约束方法在40 nm、16 nm、7 nm等工艺下均成功流片。

基于时间扩展的ASEHA建模与验证

为了有效地分析实时系统,在原计算模型的基础上,引入了时钟变量,在迁移上增加了时钟约束,扩展了异步扩展层次自动机的语义。运用基于时间扩展的ASEHA,分析了ATM系统,建立了用户和ATM的模型,并使用模型检测工具UPPAAL对模型进行验证,从无死锁、活性及可达性性质出发,验证了ATM系统的安全性。实验表明,提出的基于时间扩展的ASEHA能够降低系统分析的复杂性,有助于实时系统的建模与验证。

基于时间扩展的Web服务模型检测

由于传统的形式化方法不能保证带时间约束的组合Web服务安全可靠地运行,为了有效地分析并确保带时间约束的组合Web服务的正确性,利用时间自动机验证工具UPPAAL将带时间约束的组合Web服务的每个原子服务建立自动机模型,给出ASEHA语义描述,并用模拟器模拟带时间约束的Web服务的运行过程,对带有时间约束的Web服务的属性进行分析。最后,以旅行预订票组合系统为例,验证其死锁、活性和安全性。实例证明此方法有效。

工艺参数变化下的基于统计时序分析的时钟偏差安排

针对工艺参数变化的情况,提出一种成品率驱动的时钟偏差安排算法.提出统计时序约束图的概念,利用统计时序分析的结果将时序电路转换为统计时序约束图;将寻找关键环问题转换为最小费用/时间比值环问题,并按比例分配关键环中的时钟偏差的安全余量.实验结果表明,该算法有助于提高集成电路的成品率.

FPGA静态时序约束的策略研究及探讨

在目前的大规模FPGA设计中,必须将被测试设计的时序验证及逻辑功能验证分开进行才能得到较高的测试覆盖率。为此需要用即静态时序分析验证电路时序的正确性。静态时序约束是FPGA设计中的重要环节,对FPGA的时序收敛起着重要的作用。简述了FPGA静态时序约束设计中的基本概念,分析了时序电路的基本原理,介绍了常用的几种约束方法,重点研究了时钟约束,I/O约束,例外约束等几种情形。从而减小逻辑面积和布线延时,提高FPGA工作频率。

基于CCTL的软件可靠性测试输入特性描述方法

软件可靠性测试是指为了保证和验证软件的可靠性要求而对软件进行的测试。由于目前缺少满足被测软件输入的时序性、并发性和约束性等输入特性的有效的形式化描述方法,软件可靠性测试数据的生成无据可依,全面的软件可靠性测试难以实现。利用钟控计算树逻辑（CCTL）公式在模型检测领域能够准确描述模型内部时序关系的优势,提出了基于CCTL的软件可靠性测试输入特性描述方法,该方法对输入特性准确有效的描述,可为可靠性测试数据的生成提供依据。最后,通过对一个实例的输入特性进行描述,验证了方法的可行性和有效性。

具有可信约束的分布式存储因果一致性模型

目前,关于分布式存储因果一致性的研究领域中鲜有考虑安全风险的成熟方案。在混合逻辑时钟和HashGraph的基础上,结合可信云平台中的可信云联盟技术,提出了具有可信约束的分布式存储因果一致性模型(CCT模型)。CCT模型在客户端、服务端分别设计了身份认证和一致性数据可信校验机制,并对云存储集群中数据副本之间同步数据的过程进行了安全约束。通过仿真实验验证,CCT模型在造成了较小性能开销的前提下,能对客户端和服务端中身份签名伪造、非法第三方等安全风险进行识别并验证,为系统提供可信约束。

基于通信系统编解码芯片的逻辑综合研究

未来大批量、小型化、低功耗设备对专用处理芯片的需求迫切,本文针对通信系统编解码芯片复杂的时钟、复位、IO设计,分别采用多生成时钟、内部复位、虚拟时钟的设置,有效的实现芯片时序的收敛,达到了较好的综合结果。

一种附加钟速约束的GNSS TDCP测速改进方法

GNSS(global navigation satellite system)载波相位历元间差分(time-differenced carrier phase,TDCP)测速方法因其高精度、无收敛等优势而被广泛应用于动态导航定位中,但受限于观测环境引起的多维粗差与数据异常,TDCP的实际测速精度和稳定性通常难以保证。本文提出了一种附加钟速约束的TDCP测速改进方法,利用GNSS接收机钟速低频变化的特性,通过多项式拟合进行接收机钟速参数的短期预测,当钟速估计值偏离预测时,将拟合值作为约束条件回代到观测模型中重新进行速度估计,从而克服粗差的影响,提升TDCP测速的精度与稳定性。通过Ublox-F9P接收机和Huawei Mate40手机在城市复杂环境下的车载实测数据进行了算法验证,结果表明:附加钟速约束后,Ublox-F9P和Huawei Mate40的E、N、U方向测速精度RMS分别为0.11 m/s、0.10 m/s、0.14 m/s和0.20 m/s、0.19 m/s、0.18m/s,水平测速精度分别提升了84%和45%,高程测速精度分别提升了33%和10%。