SpaceWire D的调度表生成方法

针对航天高速SpaceWire D提出了一种调度表生成方法。该方法基于贪婪算法和SMT求解器。贪婪算法是主体，在每次迭代中以调度表的分布均匀性为优化原则产生一个约束集作为SMT求解器的输入参数，然后调用SMT求解器。SMT求解器是重要工具，用于对输入参数的可满足性进行判定，如果可满足则将输出的模型作为生成的调度表。此外，还提出了设置分片长度、确定时间槽大小以及划分冲突域的策略。最后，通过试验对方法的效果进行了验证。结果表明，生成调度表的时间较短且调度表具有良好的分布均匀性。

A method of SpaceWire D schedule generation

Being aimed at high speed SpaceWire D, a method of schedule generation was put forward, implemented with greedy algorithm combined with SMT Solver. The greedy algorithm was designed to generate a set of constraint for SMT Solver and to make the frames and frame chips distribute more uniformly in the generated schedule. The SMT Solver is an important tool and its function is to determine the satisfiability of input parameters. If it is satisfiable, the output module is the schedule wanted. In addition, new policies were proposed about setting the length of frame chips, the size of time slots, and collision area division. The method was verified with experiments. The results show that the generation algorithm can acquire a schedule featured by approximate uniform distribution in hundreds of milliseconds.