A Weighted Directed Graph-Based Algorithm for Group Routing in Printed Circuit Boards
-
摘要:
布线是印刷电路板设计中的重要一环. 现有的印刷电路板设计多依赖于电子设计自动化工具的处理，而传统的自动布线研究多聚焦于总线布线，没有将布线时确定的群组作为研究对象. 由于未经总线分组，可能存在群组中线网较多的情况，这将导致群组所占据的线宽与线间距比原先总线布线中各总线组分别占据的线宽与线间距更大，从而给实际布线带来了新的挑战. 为此，提出一种基于带权有向图的群组布线算法. 首先构建仅含有合并边以及它们之间邻接关系的Hanan网格图. 接着，利用合并边信息构建带权有向图，完成对电路板上布线资源的表示. 然后，使用一种具有多线避让功能的启发式搜索算法来进行布线规划. 最后，通过将布线归类为数种可能的情况分别考虑，完成详细布线并得到群组布线的最终结果. 实验结果表明，算法在已经测试过的工业界复杂例子上均能达到100%的布通率，并且不会违反所有工业印刷电路板基准用例的设计规则约束.
Abstract:Routing is considered an essential component in the design of printed circuit board (PCB). Current existing PCB designs mostly rely on the process results from electronic design automation tools, and traditional automatic routing research often focuses on only general bus routing without considering bus groups to be determined during the routing process. Due to the absence of general bus grouping, there may be situations where there are more nets in one group than in other groups, resulting in larger line width and line clearance occupied by this group when compared to other bus groups in the original bus routing, thereby posing new challenges to effective and efficient routing. To overcome this drawback, this paper focuses on studying PCB group routing. In this study, a group routing algorithm based on a weighted directed graph is proposed. A Hanan grid graph is constructed, containing only merged edges and their adjacent relationships. Following this, a weighted directed graph is developed using the merged edge information to represent the routing resources on the circuit board. For routing planning, a heuristic search algorithm equipped with multi-wire avoidance features is utilized. The routing situations are then classified into several potential scenarios, with each considered separately, to accomplish detailed routing and obtain a final result of group routing. Results from experiments demonstrate that a 100% routability is consistently achieved by using the algorithm on complex industrial examples that have been previously tested, and that the design rule constraints of all benchmark industrial PCB cases are not violated.
-
深度学习模型在图像识别、自然语言处理、机器人技术以及自动驾驶等诸多领域发挥了重要作用. 由此涌现出了一系列主流深度学习（deep learning，DL）框架，如PyTorch[1]，TensorFlow[2]，Caffe[3]，Keras[4]. 这些框架使程序员能够高效地开发、训练和评估模型. 尽管这些工具使得将深度学习集成到软件系统中变得容易，但它们都建立在动态类型语言Python之上，缺乏类型检查机制. 因此，许多错误无法在编译阶段通过类型检查加以排除. 此外，基于命令式语言构建的神经网络模型不利于代码优化，并且不便于进行模型正确性的形式验证.
由于深度学习应用程序独特的操作方式和数据要求，以及应用和部署的快速增长，这类程序中出现的错误也日益增多. 其中张量形状错误（shape error）是深度学习代码中的主要错误类型之一，可能在深度学习任务的各个阶段发生. Wu等人[5]的研究表明，形状错误占据了TensorFlow程序中45%的故障.
在使用深度学习框架（如Pytorch）构建人工智能（artificial intelligence，AI）模型时可能会出现张量形状不匹配错误. AI模型通常由多个层组成，每个层接受输入张量并产生一个输出张量. 每一层的输出张量形状必须与下一层的输入张量形状相匹配，否则，在运行时会出现形状错误. 以下是文献[6]中的一个示例：
1 class Net(nn.Module):
2 def __init__(self):
3 super(Net, self). __init__()
4 self.layers = nn.Sequential(
5 nn.Linear(28*28, 120),
6 nn.ReLU(),
7 nn.Linear(80, 10)
8 )
该例子定义了一个简单的神经网络模型，由一系列的层组成，包括一个线性层、一个激活函数ReLU和另一个线性层. 第1个线性层的输入是1个维度大小为28×28的1维序列，输出是一个大小为120的张量，最后1个线性层的输入是大小为80的张量，输出是一个表示分类的10维向量，其中激活函数不改变张量的形状. 然而，第2个线性层的权重张量尺寸（80×10）与实际传入的张量尺寸120不匹配，从而导致形状错误. 这种错误通常会导致程序崩溃，从而浪费大量的计算时间. 尤其是当错误出现在复杂模型的后期阶段时，可能需要运行很长时间才会发现错误，因为需要处理庞大数据集的冗长预处理过程. 这不仅会导致计算资源和时间的显著浪费，还会产生错误结果以及耗时的调试工作.
针对这种形状错误，现有的解决方案是分析学习框架中编写的代码. 已有一些研究尝试解决深度学习模型中的形状错误问题[6-9]. 然而，随着深度学习模型复杂性的增加，以及数据集和输入维度规模的扩大，形状错误的严重性愈发凸显. 这些方法并不能百分之百检查出所有形状错误.
DL框架可以被视为用于构建AI模型的领域特定编程语言，用于实现各种算法[10]. 然而，现有主流学习框架如PyTorch，TensorFlow等无法借助类型系统来排除网络模型中的形状错误. 一些强类型语言也曾尝试构建学习框架[11-12]，但是由于这些语言缺乏准确描述张量的类型系统，也没有实现自动检查形状错误的功能. 因此，在DL框架中加入自动检查形状错误的能力将是一个更好的解决方案.
本文提出了一种新的学习框架Ionia，该框架具有以下显著优势. 首先，该学习框架采用了带类型的网络描述和类型检查，能够自动解决深度学习模型中的形状错误问题. 这与以往的工作有所不同. Ionia并不是对使用现有框架编写的代码进行分析，而是从头开始定义了一个新的强类型学习框架. 与主流的动态类型Python语言的学习框架不同，Ionia是嵌入在Coq定理证明器中. Coq[13]是一个具有强大类型系统的定理证明助手. 本文充分利用了Coq的类型检查机制，定义了一个专门用于描述张量的类型系统，并为各种神经网络算子定义了类型以及具体语义. 通过这些类型化的算子，该学习框架的类型检查机制能够静态检查AI模型中是否存在形状错误并精准定位. 换句话说，能够通过类型检查的网络模型一定不存在形状不匹配错误. 这种方法为形状错误检测提供了更高效、更可靠的解决方案.
更重要的是，该学习框架为进一步优化和验证AI模型奠定了良好基础，这是本文选择在Coq定理证明器中构建DL框架的主要考量. 自动检查形状不匹配错误只是这一设计的一个有用的副产品和阶段性成果，但Ionia的潜力远不止于此. 由于Coq是一种函数式编程语言，以其强大的数学理论为基础，提供了几乎无法在传统命令式编程语言中实现的高级优化和形式化验证途径. 凭借Coq强大的推理能力，使得对模型进行严格的数学证明成为可能，确保其在逻辑上的一致性和正确性，这为AI编译器的优化和正确性验证提供了更为坚实的基础.
最终，高级函数式抽象需要转换为命令式代码，以满足现代并行硬件接口的要求. 本文在文献[14-16]的基础上在Coq中设计并实现了一系列重写转换规则，用于将带类型的函数式神经网络算子表达式转换为相应的命令式C代码. 虽然文献[16]在文献[14-15]的理论基础上实现了常见函数式矩阵程序，如矩阵加法、乘法到C代码的转换工作. 但该技术的表达能力有限，难以在函数式层面表示出如卷积、池化等神经网络算子. 因此，本文将该技术进一步扩展，定义了一个基于有限集的下标索引到元素值映射的张量构造函数，从而能够表示出100余个函数式神经网络算子表达式，并设计实现了一系列针对神经网络算子的重写转换规则，用于生成算子C代码. 这些重写转换规则便于后续在Coq中进行正确性的形式验证，以保证生成的神经网络算子C代码的可靠性. 利用该方法，本文成功生成了一批神经网络算子的C代码，该代码与手工编写的代码质量相当，且生成的多核并行OpenMP C代码相比顺序执行的算子C代码速度提升了4~10倍. 此外，该方法生成的C代码具有高安全性，能够有效避免常见手工编写代码时出现的下标越界和存储分配错误.
本文的主要贡献总结如下. 首先，基于Coq建立了一个带类型的函数式深度学习框架Ionia. 该框架具有带类型的张量结构以及强大的类型检查能力，能够确保构建的神经网络模型无形状错误. 实验结果表明，该框架能够自动静态检测到模型中的形状不匹配错误. 其次，设计并实现了一系列重写转换规则，用于将函数式神经网络算子表达式转换为高安全、高可靠的C代码. 这项工作实际上具备了一个小型AI编译器的功能，不仅在函数式层面构建了DL框架，而且实现了函数式表示的神经网络算子到OpenMP C代码的翻译. 最后，这项工作不仅为形状错误检测提供了方便，更为后续AI编译器的优化及正确性验证奠定了基础.
1. 相关工作
目前，已有多项工作致力于解决深度学习框架中的形状不匹配问题. Hattori等人[9]针对PyTorch应用，提出了一种半静态分析方法，用于推断动态计算图中的类型和形状. 然而，由于其路径不敏感和半静态的特性，该工具在实际应用的完全静态分析中并不适用. PyTea[6]是一个自动静态分析器，用于检测 PyTorch代码中的张量形状不匹配错误. 该分析器基于对所有可能执行路径的静态跟踪，收集张量形状约束，并检查这些约束是否不可满足. 然而，它并不执行通用的值分析，这限制了其在跟踪张量或数组索引非绑定异常时的能力. 相比之下，本文所提出的方法基于Coq这种依赖类型编程语言，允许直接通过索引对张量形状进行静态检查. 这使得张量形状的验证更为简单直接，并能够更全面直观地分析张量形状的依赖关系.
针对TensorFlow应用程序，已经提出了不同的方法来检测形状错误. Pythia[7-8]利用值流分析静态追踪整个程序中的张量形状，并警告可能的形状不匹配. 而ShapeFlow[17]则作为动态分析器，通过模拟TensorFlow库来监控形状变换. 然而，这些方法都存在局限性. Pythia对Python和TensorFlow的覆盖仍不足以满足实际应用的需求，而ShapeFlow需要一个缩小的虚拟数据集，并且无法检测由未经测试的输入数据集引起的潜在形状不匹配.
一些工具已经采用了类型系统来对张量形状进行静态检查. Hasktorch[18]提供了对libtorch[19]的Haskell[20]绑定，以静态检查张量形状. 然而，使用Haskell的类型级编程特性意味着张量不被视为一等对象. Relay[21-22]是一个深度学习编译器系统，支持丰富的张量形状类型推断，并支持动态和静态形状检查. 与此同时，文献[23]提出了一种基于类型的方法来检测张量形状不匹配，首先执行静态类型/形状推断，在静态推断无法保证形状一致性时添加动态检查. 文献[24-26]是关于依赖类型系统中的渐进类型研究. 这些工作特别关注于细化类型系统中谓词部分的渐进性，而底层简单类型则保持静态. 与这些方法相比，本文直接利用Coq内在的类型检查机制来实现静态类型检查.
以强类型的函数式语言为基础构建深度学习框架的研究也已有探索. DeepDSL[11]是一种嵌入在强类型语言Scala中的领域特定语言，支持直接构造神经网络模型，并提供早期的静态检查，最终将DeepDSL程序编译为Java源代码. 另外，文献[12]是一个基于OCaml编程语言的科学计算系统，包括各种由OCaml实现的库，如基于算法微分实现的数学优化、回归和深度神经网络等，专注于从头开始构建神经网络模型. 然而，这些工作由于缺乏对张量的准确定义，因此无法自动检测出张量形状错误.
从函数式编程模型出发，以函数式的方式表示各种操作和优化策略，然后将其转换为硬件接口所需的命令式程序，已成为解决高性能可移植性问题的一种流行方法. 例如，数据并行理想化（data parallel idealised algol，DPIA）[14-15]实现了一种策略保留（strategy preserve）的翻译方法，它基于一系列的重写规则将高级函数式代码翻译成低级、无数据竞争的并行命令式代码. 麻莹莹等人[16]在Coq定理证明器中形式化了DPIA技术，实现了矩阵代码生成技术，将高级函数式矩阵表达式转换为C代码. 然而，这些方法基于元素到元素的映射实现的函数式矩阵表达式虽然能够表示诸如向量/矩阵加法、乘法等常规矩阵操作，但在处理神经网络中的卷积、池化等算子时面临挑战. 例如，在表达卷积核在输入张量上的移动过程时存在困难. 相比之下，本文所定义的以有限集的下标索引到元素值的映射实现的张量表达式有助于全面表示函数式神经网络算子，从而设计出一系列重写转换规则，用于生成神经网络算子OpenMP C代码.
一个张量语言（a tensor language，ATL）[27]是轻量级的Coq框架，旨在优化以纯函数式数组语言编写的张量程序，实现了各种 Halide[28]优化调度指令，并最终将优化后的张量表达式翻译成C代码. 然而，它们的代码生成过程是直接将ATL程序降低为C代码字符串. 相比之下，本文利用延续传递（continuation passing）风格[29]的重写转换规则，将函数式张量表达式翻译成命令式原语，提供了更高的灵活性和可扩展性. 这有助于处理复杂的嵌套函数结构，并且便于后续在Coq定理证明器中对重写转换规则进行严格的证明，以保证生成代码的可靠性. 此外，ATL 采用基于列表的方式来表示数组/张量，并配有保护表达式以防止数组越界访问. 相比之下，本文使用了带长度的向量类型来表示数组，并利用有限集来确保安全的数组索引访问，更简洁直接. 因此，生成的命令式代码在内存安全性方面更具优势.
本文的显著优势在于，使用本文设计的强类型深度学习框架Ionia构建的神经网络模型，能够从根本上避免张量形状不匹配的错误，或者说，能够在模型构建过程中自动有效检测出张量形状相关的错误并精准定位. 这一特性极大地提升了模型开发的效率和可靠性. 此外，将函数式神经网络算子表达式翻译为高安全的多核并行OpenMP C代码. 生成的C算子不仅能够精确执行预期操作，还能够避免诸如下标越界和存储分配错误等人工编写代码时常见的问题.
2. 张量类型
本节将深入探讨张量类型的形式化定义方式. 这种形式化表示不仅要便于描述神经网络算子操作，还要能够捕获神经网络模型中固有的形状.
张量类型是神经网络中表示数据的关键概念，它们作为多维数组的抽象表示，用于存储输入、权重和输出数据. 已有一些研究专注于张量类型的形式化定义[30-32]. 本文采用嵌套数组的方式来定义张量类型，并基于一个有限集的下标索引到元素值的映射函数来构造具体的张量.
首先，在Coq中定义了一个归纳数据类型data，它作为各种数据结构的基础表示. 其中，构造器num和ary分别封装了数值和数组.
Inductive data : Set :=
| num : data
| ary : nat -> data -> data.
在张量的上下文中，有限集充当张量/数组的索引集，能够避免数组索引访问越界的错误. 在Coq中，存在多种定义自然数有限集的方法[13, 33]. 本文采用了一种简洁直观的方式，允许有限自然数集与自然数之间的直接转换. 其定义如下所示：
Definition fin (n : nat) : Set :=
match n with
| O => unit
| S n' => { i | i < (S n')}
end.
在这个定义中，O和S是自然数的构造函数. O表示0，S表示后继函数. 例如，自然数3可以用S (S (S O))来构造. 关键字Definition用于非递归函数或值的定义，而Fixpoint用于递归函数的定义.
fin的定义接受一个自然数n，返回一个集合. 通过对自然数n模式匹配. 当n为O时，返回一个空集合unit，当n不为O时(即为S n')，它包含一个自然数i以及i < S n'的证明. 在Coq的构造逻辑中，证明是编码证明过程的显式项，结构{i | P i}表示满足P i为真的i的集合，其包括了P i为真的证明. 例如，fin 5表示{0, 1, 2, 3, 4}这个集合中的元素，其中每个元素都小于5. 本文将该有限集作为张量的索引类型，可以确保下标索引保持在边界范围之内.
在定义张量类型时，形式化向量是一个关键步骤. 在Coq中，存在多种定义向量类型的方法，包括基于函数的方法[33]和标准库中的依赖类型[12]. 本文采用了Coquelicot[34]中使用的向量形式化方法，该方法使用元组构造向量.
Fixpoint vector (n : nat) : Set :=
match n with
| O => unit
| S n' => ((vector n') * B)%type
end.
本文定义的向量类型是通过元组表示构造的，这种方法的优势在于接近函数式语言中的数据结构，并且便于实现向量的一些基本操作及形式化验证. 然而，这种数据结构不便于根据索引访问数组元素. 因此，在定义涉及数组索引的一些函数时，这种数据类型不方便表示. 另一种建模向量的方式是将其视为从索引集到向量元素的函数映射. 在实际工作中，有时需要在这2种表示方法之间进行切换. 下面定义的函数mk_vec将基于函数的向量表示转换为基于元组的向量表示.
Fixpoint mk_vec{n : nat}: (fin n -> B) -> vector n :=
match n with
| O => fun ( _:_ ) => tt :vector 0
| S n' => fun (u : fin (S n') -> B) =>
(mk_vec (fun i : fin n' => u i), u [n'])
end.
此处，mk_vec是一个递归函数，用于构造包含n个元素的向量. 其接受一个从有限集fin n到类型为B的映射函数作为参数. 当n为O时，函数返回空向量tt. 当n不为O时，递归调用mk_vec构建前n–1(此处表示为n')个元素，然后调用参数函数u来构建最后一个元素，其中使用函数exist生成类型为fin (S n')的自然数n'(表示为{n' | n' < S n'}).
接着，引入了函数exp，它在类型data的元素与本文所实现的Coq系统内的类型之间建立了对应关系. 该函数使用模式匹配确定每个数据构造函数的Coq类型，将num映射到实数集ℝ，将ary映射到具有指定长度和元素类型的向量.
Fixpoint exp (d : data) : Set :=
match d with
| num => ℝ
| ary n d => vector (exp d) n
end.
这种形式化为构建张量类型和表示带类型的神经网络算子奠定了基础.
为了简化不同维度张量的表示方式，本文为Ionia框架中的张量引入了更简洁的定义. 大小为m的1维张量Tensor1 m即表示为exp (ary m num)，大小为m×n的2维张量Tensor2 m n表示为exp (ary m (ary n num)). 通过这种方式，可以方便地表示出不同维度的张量类型.
最后，通过mk_vec建立基于有限集的下标索引到元素值的映射函数mkvSeq{d}: fin n -> exp d -> exp (ary n d)构造出了带有维度大小的张量. 通过灵活应用嵌套的函数mkvSeq，我们能够构造出具有任意维度的张量，并且可以根据索引方便地访问张量中的任意元素. 这极大地简化了诸如Conv2d等神经网络算子的表示. 例如，大小为m×n且元素为默认值的2维张量构造如下：
Definition mkTensor2 (m n : nat) : Tensor2 m n :=
mkvSeq (fun i : fin m => mkvSeq (fun j : fin n => exp_default num)).
这种方法不仅便于构造任意维度的张量，而且确保了更高的安全性和可靠性. 通过有限集对元素进行映射，有效地避免了在访问张量元素时可能出现的索引越界错误.
3. 带类型的AI模型描述
本节首先在第2节张量类型的形式化定义基础上表示出一组函数式神经网络算子表达式，这些表达式不仅足以构建大多数神经网络模型，还具备检查形状错误的能力. 多组实验验证，使用带类型的算子并结合Coq的类型检查机制，能够确保所构建的模型不存在形状错误. 这些算子涵盖了多种神经网络操作，包括卷积、反卷积、池化、全连接、归一化等. 最终，这些函数式表示的神经网络算子表达式将作为第5节代码生成工具的输入层，根据重写转换规则将其翻译为命令式C代码.
3.1 基本操作函数
在形式化表示神经网络算子之前，介绍几个针对不同数据类型的基本操作函数. 其中结构化数组的基本操作函数如表1所示：
表 1 数组的基本操作函数Table 1. Basic Operation Functions of Array函数 功能 符号表示 mkvSeq 构造数组/张量 ⊞ let_binding 中间变量值绑定 tlet x := e in y idx 根据下标索引访问数组
第i个元素a |[ i ] max 求数组元素最大值 - sum 求数组元素的和 ∑ 表1中的let_binding是在第5节生成命令式C代码的上下文中，用于存储代码生成的中间结果. 虽然在Coq的语法结构中有类似的let绑定，但是这会忽略函数式表达式中的临时变量，导致该临时变量在最终的表达式中不会显式出现. 这样在后续命令式代码生成过程中，翻译器无法利用延续传递规则翻译中间变量的存储结构，最终使函数式表达式到命令式代码的翻译不完整. 因此，本文在Coq中形式化了中间变量值的绑定.
数组/张量构造函数mkvSeq和元素访问函数idx满足idx_mkvSeq性质.
定理1. 对于任意的d n (f : fin n -> exp d) i，满足n > 0 -> (mkvSeq f)|[i] = f i.
证明.该定理的证明采用了对数组元素数量n的归纳法. 当n为O时，直接根据定义展开即可验证该定理成立；对于非基础情况，即n为非O时(即元素个数为S n)，将包含S n个元素的构造函数转换为基于前n个元素的向量构造和最后一个元素的对偶形式，即(mkvSeq f, e)，然后通过索引访问新构造的向量元素，并利用n的归纳假设条件证明包含S n个元素的构造数组函数也满足该定理.
针对数值型的基本操作函数如表2所示：
表 2 数值型的基本操作函数Table 2. Basic Operation Functions of Numerical Type函数 功能 zero，one 分别代表实数R0，R1 negate 数值型元素取反的操作 add/sub/mul/div 2个数值型元素的加/减/乘/除操作 scal 实数与数值型元素的乘积操作 div_n 数值型元素除以自然数的操作 pow/log/pExp 数值型元素的幂次方/对数/指数操作 sqrt 数值型元素的平方根操作 leExp/gtExp 2个数值型元素的小于等于/大于关系 以上数值型的基本操作函数是基于Coq库中实数集ℝ上的基本操作. 基于上述数值与数组的基本操作函数，我们可以方便地表示出各类函数式神经网络算子表达式.
3.2 函数式神经网络算子表达式
本节将以2维张量的卷积算子为例，详细阐述如何在函数式层面精确地表示神经网络算子表达式. 对于其他神经网络算子，可以采用类似的方式表示，以确保每种操作都能得到准确的描述.
2维卷积操作的示例如图1所示.
在Coq中实现的2维卷积算法如算法1所示：
算法1. Coq中实现的2维卷积算法.
输入：填充因子p，步长s，大小为n1×n2的卷积核张量w，以及大小为m1×m2的输入张量input；
输出：大小为((m1－n1＋2p)/s＋1)×((m2－n2＋2p)/s＋1)的2维张量.
① 填充操作. 根据输入张量input以及填充因子 p计算出填充后的张量，该2维张量的维度 大小分别为(m1＋2p)和(m2＋2p). 具体地， 采用了嵌套的张量构造方式，外层构建行， 内层构建列. 通过if条件判断当前索引是 否在输入张量的范围内. 若在范围内，则将 输入张量input中对应的元素赋给当前索 引处的元素. 如果当前索引超出了输入张 量的索引范围，则使用默认元素zero在该 特定索引处进行填充；
② 引入一个中间张量pad用来存储①计算出的 结果. 接着，构建嵌套的2维张量结构，其 中外层结构表示输出张量的行(i0)，内层结 构表示输出张量的列(j0). 当前索引处的输 出元素通过嵌套的求和操作(sum)计算得 出，该操作遍历2维张量结构，以迭代卷积 核中的每个元素. 卷积核w的对应元素与 pad在指定索引处的元素相乘，并将结果相 加，以获得最终的输出元素.
2维张量的函数式卷积表达式如下所示：
在该表达式中，“⊞”表示所构造的张量结构，紧接着的i，j等符号表示张量的下标索引，张量的维数决定了下标索引的个数，“[ ]”括号内的内容对应下标索引处的张量元素值. 符号“[ b ] a1 | a2 ”表示if条件判断，即当b为True时，选择a1；当b为False时，选择a2. 利用这种符号表示便于直观简洁地表示出函数式神经网络算子表达式.
图1中的2维卷积示例在Coq中的计算结果可进行正确性验证，如图2(Coq截图)所示. 其中填充因子p和步长s均为1.
以这种方式定义的卷积算子融入了类型检查机制，增强了张量表达式的健壮性和可靠性，有效解决了传统深度学习框架中常见的类型不匹配问题.
本文在Coq中实现了100余个函数式神经网络算子表达式，涵盖了多种操作类型，包括元素级操作、元素复合操作以及张量重塑等. 这些算子的实现旨在丰富Ionia框架的表达能力和应用场景. 通过引入这些类型化算子，Ionia能够有效地支持各种神经网络模型的描述和类型检查. 部分的函数式神经网络算子表达式如表3所示：
表 3 函数式神经网络算子表达式Table 3. Functional Neural Network Operator Expression分类 函数 功能
元素操作ReLU1d/ReLU2d/
ReLU3d/ReLU4d对不同维度的张量元素取激活函数ReLU Softmax1d/Softmax2d/
Softmax3d/ Softmax4d对不同维度的张量元素取激活函数Softmax Tanh2d/Tanh4d 对不同维度的张量元素取激活函数Tanh Tadd2d/Tadd4d 对相同维度张量元素相加 Tmul2d/Tmul4d 对相同维度张量元素相乘 复合操作 Conv2d/Conv4d 不同维度张量的卷积操作 Avgpool2d/Avgpool3d/
Avgpool4d不同维度张量的平均池化操作 Maxpool2d/Maxpool3d/Maxpool4d 不同维度张量的最大池化操作 Linear/Linear2d 不同维度张量全连接操作 NLLLoss2d 损失函数NLLLoss ConvTranspose2d/
ConvTranspose4d反卷积操作，扩大张量尺寸 重塑操作 Flatten3d/Flatten4d 平铺操作 Truncl1d/Truncl2d 向左/右截断张量k个元素 Padl/Padr 向左/向右填充k个元素 Concat 连接2个张量 3.3 构造带类型的神经网络模型
在本节中，将重点展示如何使用3.2节中定义的函数式神经网络算子构建AI模型，重点关注其类型正确性的自动验证. 借助带类型的网络描述以及Coq的类型检查机制，可以确保模型形状的可靠性. 通过一系列AI模型的构建，证实了本文提出的类型化学习框架能够自动验证AI模型中的类型正确性.
本文通过经典卷积神经网络(convolutional neural networks，CNN)模型LeNet-5[35]来展示如何在Coq中构建AI模型，并确保所构建的AI模型不存在张量形状错误. LeNet-5模型的结构图如图3所示：
通过带类型的神经网络算子表达式构建网络时，每一层的参数都受到严格的约束，确保在各个阶段输入和输出张量形状相匹配. LeNet-5模型的类型化设计以及Ionia框架的静态类型检查机制确保了该模型中不存在张量形状错误.
Coq中实现的带类型LeNet-5模型如下所示：
Definition LeNet_5 (input : Tensor3 1 32 32)
(w1 : Tensor4 6 1 5 5) (b1 : Tensor1 6)
(w2 : Tensor4 16 6 5 5) (b2 : Tensor1 16)
(fw1 : Tensor2 120 (16*5*5)) (fb1 : Tensor1 120) (fw2 : Tensor2 84 120) (fb2 : Tensor1 84)
(fw3 : Tensor2 10 84) (fb3 : Tensor1 10)
:=
tlet fm1 := Conv3d 0 1 b1 w1 input in
tlet rm1 := ReLU3d fm1 in
tlet pm2 := Maxpool3d 2 rm1 in
tlet fm3 := Conv3d 0 1 b2 w2 pm2 in
tlet rm3 := ReLU3d fm3 in
tlet pm4 := Maxpool3d 2 rm3 in
tlet fm5 := Linear fw1 fb1 (Flatten3d pm4) in
tlet rm5 := ReLU1d fm5 in
tlet fm6:= Linear fw2 fb2 rm5 in
tlet rm6 := ReLU1d fm6 in
tlet fm7:= Linear fw3 fb3 rm6 in Softmax1d fm7.
LeNet-5神经网络模型通过一系列算子构建而成，每个算子操作都经过Coq的静态类型检查，以确保张量形状的正确性. 该模型的输入张量为1×32×32，首先经过一个操作Conv3d和激活函数ReLU3d，然后是Maxpool3d操作. 这一过程在第2个卷积块中重复执行. 之后，输出被展平并通过3个Linear层，中间使用激活函数ReLU1d. 最后一层采用函数Softmax1d产生模型的输出. 在每个操作中，Coq的类型检查机制均严格确保了张量维度的精确匹配. 一旦检测到张量形状不匹配的问题，Coq将自动定位并报告问题所在，从而确保了经过Coq类型检查的AI模型能够完全避免形状相关的错误.
为进一步展示该框架的表达能力，本文实现了更复杂的AI模型，包括GoogLeNet[36]，ResNet[37]，VGG[38]，LSTM[39]等神经网络模型. 在模型构建过程中，充分利用了Ionia对张量的静态类型检查能力，确保每个模型在构建时都能避免形状错误. 表4列出了这一学习框架中已实现的AI模型.
表 4 带类型的神经网络模型Table 4. Typed Neural Network Model分类 模型 介绍
CNNLeNet 一个经典神经网络模型，由2个卷积层和
3个全连接层组成AlexNet 一种经典的深度CNN模型，由5个卷积层和
3个全连接层组成ResNet-34 一种经典的残差CNN模型 GoogLeNet 一种网中网的深度CNN模型，引入了
Inception模块VGG-16 深度CNN模型，适用于迁移学习 DenseNet-121 一种稠密CNN模型，引入了DenseBlock块与
前面所有层连接GM DCGAN 一种深度卷积生成对抗网络 VAE 一种深度生成模型，由1个编码器和
1个解码器组成RNN LSTM 一种特殊的递归神经网络，引入了3个门和1个细胞状态以处理序列中的长期依赖关系 4. 形状错误检测
在本节中，通过一系列实际的应用程序验证了该类型化学习框架可以自动、精准、有效地检测出张量形状不匹配的错误，这对于确保AI模型的可靠性至关重要.
针对引言中AI模型形状错误的示例，可以利用Ionia框架在Coq中构建出相同的模型，示例如下：
1 Definition example_mismatch (input :
2 Tensor1 (28*28)) (fw1 : Tensor2 120 (28*28))
3 (fb1 : Tensor1 120) (fw2 : Tensor2 10 80)
4 (fb2 : Tensor1 10)
5 :=
6 tlet fmap1 := Linear fw1 fb1 input in
7 tlet rmap2 := ReLU1d fmap1 in
8 Linear fw2 fb2 rmap2.
Coq的类型系统使得在定义中可以自动发现类型不匹配错误，并在第8行报告错误信息：“The term "rmap2" has type "Tensor1 120" while it is expected to have type "Tensor1 80"”. 此错误表明最后一个算子Linear的实际输入张量rmap2的类型是Tensor1 120，而参数权重是Tensor2 10 80，导致维度大小为120的1维张量与10×80的2维张量相乘时尺寸大小不匹配，导致形状错误.
尽管运行相应的PyTorch应用程序也会出现错误信息：“RuntimeError: mat1 and mat2 shapes cannot be multiplied(1×120 and 80×10)”. 但是该错误信息仅能提供整个层的提示，而无法精确指向具体某层中的某个操作. 此外，获取此类错误信息需要完整运行整个应用程序. 然而，由于复杂的深度学习模型可能需要较长时间的训练，因此发现错误可能需要花费大量时间，导致显著的开销. 相比之下，本文利用Coq的静态类型检查机制，能够直接将错误精准定位到具体操作上. 更重要的是，由于这种检查方式是静态的，因此能够立即发现问题，而无需等待整个应用程序运行完成，从而大大缩短了响应时间. 这一优势不仅提高了错误检测的效率，也降低了调试的复杂性.
解决方法：调整第2个全连接层fw2权重的尺寸，将其更改为Tensor2 10 120以匹配上一层的输出维度. 在做出相应更改后，得到了修正后的代码：
1 Definition example_mismatch (input :
2 Tensor1 (28*28)) (fw1 : Tensor2 120 (28*28))
3 (fb1 : Tensor1 120) (fw2 : Tensor2 10 120)
4 (fb2 : Tensor1 10)
5 :=
6 tlet fmap1 := Linear fw1 fb1 input in
7 tlet rmap2 := ReLU1d fmap1 in
8 Linear fw2 fb2 rmap2.
该代码通过了Coq的类型检查，表明此时该模型描述不包含任何形状错误.
为了评估该学习框架在形状错误检测方面的实际应用能力，本文研究了PyTorch应用程序，并从StackOverflow平台收集了与形状错误相关的典型案例. 随后，展示了Ionia凭借其强大的静态类型检查能力，能够精准有效检测出张量形状不匹配的问题.
首先，在Coq中实现了基于GitHub上pytorch/examples[40]官方PyTorch示例项目的AI模型. 为了验证Ionia框架在检测和纠正张量形状不匹配方面的有效性，我们在模型中主动引入了形状错误. 同时，利用该框架复现了从StackOverflow平台中收集到的错误案例[41]，以测试Ionia框架的形状检查能力. 为验证Ionia的检测能力，本文将检测结果与PyTea[6]和Hattori等人[9]的检测工具对比，结果如表5所示：
表 5 形状错误检测结果Table 5. Shape Error Detection Results结果表明，Ionia均成功快速地检测到了每个形状不匹配的情况，并且能够精准定位问题所在. 与此同时，尽管PyTea[6]能够检测到大部分PyTorch应用程序的形状错误，但无法分析出TensorFlow中的错误，并且其需要一定的响应时间，相比之下效率较低. 而Hattori等人[9]的分析器在测试中均未能成功检测出形状错误. 值得注意的是，本文提出的方法不仅能够精准定位到形状不一致的具体位置，而且几乎无响应时间，足够快速有效. 这种能力潜在地节省了调试时间，因为它可以快速准确地定位并解决形状不匹配的问题，而无需执行整个程序.
通过多个模型构建和形状错误检测的实例后，可以得出：学习框架Ionia不仅具有足够大的表达能力，而且具备卓越的类型检查功能. 这一能力能够极大地协助用户进行高效的模型调试，帮助用户快速发现并精准定位模型中存在的形状不匹配错误. 此外，该框架提供了丰富的API和库函数，用户可以轻松构建各种类型的神经网络模型，而无需担心形状错误.
5. 代码生成工具
在本节，提出了一种神经网络算子代码生成工具，用于将3.2节中定义的函数式神经网络算子表达式翻译为相应的命令式C代码. 该代码生成方法受到DPIA[14-16]的启发. 其中文献[16]是DPIA的Coq实现，通过重写机制将函数式矩阵程序转换为C代码. 然而，该方法针对的是常规矩阵操作，如矩阵加法、乘法，并不支持神经网络算子如卷积、池化的代码生成. 因此，本文在此基础上，进一步扩展了该技术，设计并实现了一系列重写转换规则，用于将函数式神经网络算子表达式转换为OpenMP C代码.
代码生成方法主要由5部分组成. 第1部分是Ionia框架所描述的神经网络模型及函数式算子表达式，作为代码生成的输入层. 第2部分是基本的函数式原语，包括3.1节中定义的数值与数组的基本函数. 第3部分是中间命令式组合子，作为函数式表示的命令式中间结构. 第4部分是低级命令式原语，对应于命令式C代码中的语句. 第5部分是生成的命令式程序. 其中第1部分的函数式算子是由第2部分的基本函数构造，第3部分的中间命令式组合子是由第4部分命令式原语组成. 因此，这2部分的转换只要展开相应的定义即可. 基本的函数式原语通过翻译器A和翻译器C的重写转换规则转换为中间命令式组合子，而命令式原语通过显示翻译规则(explicit translation rules)直接转换为C语句字符串. 通过这一过程，以函数式形式表示的算子表达式最终翻译成对应的C程序. 图4是整个代码的生成过程.
图4中的函数式神经网络算子表达式和基本的函数式原语在第3节中已定义，接下来将分别介绍命令式原语、中间命令式组合子、重写转换规则以及显示翻译规则.
5.1 命令式原语
在命令式C代码中，常将表达式的值赋给某个变量，该变量充当被赋值对象的作用. 在DPIA[14-16]中表示为接收器类型，该类型是一组由输入数据类型确定的数据访问路径，定义如下：
Fixpoint acc (d : data) : Set :=
match d with
| num => path
| ary n d => vector (acc d) n
end.
其中path是归纳定义的路径，由字符串组成.
DPIA提出了一组用于描述C语句的命令式原语. 为生成带有选择语句的C程序，本文增加了If条件命令，现有的命令式原语包括：
comm ::= skip | seq | If | assign | new | for | parfor.
本文在Coq中用归纳定义的数据结构实现comm，它包括7个构造子. 其中，skip 表示空命令或无操作命令. seq 表示顺序组合，即2个命令按顺序执行，用符号“p1 ; p2”表示. If表示条件命令，根据布尔条件决定命令的执行. assign 表示赋值命令，将表达式的值e赋给接收器变量a，用符号“a |:= e”表示. new 表示声明新变量的命令，该命令由一个函数生成，该函数接受一个接收器和表达式的对偶以及另一个命令作为参数，并返回一个新的命令. for 表示循环，根据有限集合中的元素，重复执行一个命令. parfor表示并行循环，其接受一个变量接收器，用于存储并行操作时的临时变量.
5.2 中间命令式组合子
本节将带有高阶的基本函数式原语定义为由命令式原语组成的中间命令式组合子. 包括张量构造函数mkvSeq的中间命令式组合子mkvSeql，并行操作张量的中间命令式组合子mkvParl，中间变量绑定值let_binding的中间命令式组合子letl，以及对数组元素求最大值、规约求和的中间命令式组合子maxl和suml. 具体定义如表6所示.
表 6 中间命令式组合子Table 6. Intermediate Imperative Combinators函数 具体实现 mkvSeql Definition mkvSeql {n:nat} {d:data} (f:fin n -> acc d -> comm) (out:acc(ary n d)) := for (fun i:fin n => f i out|{i}). mkvParl Definition mkvParl {n:nat} {d:data} (f:fin n -> acc d -> comm) (out:acc(ary n d)):= parfor out (fun i o => f i o). letl Definition letl{s t}(e:exp s)(f:exp s -> acc t -> comm)(out:acc t) := f e out. maxl Definition maxl {n:nat} (xs:exp (ary n num)) (f:exp num -> acc num -> comm) (c : exp num -> comm) := new (fun tmp => let (w,v) := tmp in (w |:= xs |[0]) ; (for (fun i => If (gtExp xs|[i] v) (f xs|[i] w, f v w)) ; c v)). suml Definition suml {n:nat} (xs : exp (ary n num)) (f:exp num -> acc num -> comm) (c : exp num -> comm) := new (fun tmp => let (w,v) := tmp in (w |:= zero) ; (for (fun i => f (add xs|[i] v) w)) ; c v). 表6中的mkvSeql接受一个函数 f，该函数将有限集映射到具有输出访问路径的命令上. 通过for命令对有限集中的每个元素i执行f操作，其中out|{i}表示输出张量接收器的第i个元素. 该定义以函数式的方式表示出命令式的数组循环操作. 在5.3节中，将利用翻译器A和翻译器C的重写转换规则将张量构造函数mkvSeq转换为命令式表示的mkvSeql，从而实现从函数式原语到命令式原语的转换. mkvParl是针对有限集到元素映射的并行操作，具体地，通过parfor命令并行执行数组的循环操作，其中添加了临时变量. letl，maxl，suml是中间变量绑定值、数组最大值、数组元素和的命令式表示.
5.3 重写转换规则
重写转换规则是将函数式表达式转换为命令式原语的核心机制. 这些转换规则通过翻译器A和翻译器C互相定义. 翻译器A的具体定义为A(a, e)，表示为命令的赋值操作，具体地，将表达式的值e赋给接收器变量a. 而翻译器C的具体定义为C(e, c)，其中e代表给定的表达式，c是表达式到命令的映射函数，具体形式为exp d -> comm，该函数将表达式域中的元素映射到命令域中的元素. 通过将表达式e作用于映射函数c上，可以继续根据映射结果翻译后续的命令，最终返回一个新命令.
根据本文所实现的函数式神经网络算子表达式，我们设计并实现了翻译器A的重写转换规则，这些重写转换规则旨在将基本的函数式原语有效转换为低级命令式原语的组合形式. 具体地，翻译器A的重写转换规则如图5所示.
A1至A8是针对数值型的重写转换规则. 例如，A2将2个数值型的表达式求和结果赋给接收器a，相当于依次对两个表达式翻译后再求和的赋值操作. A9至A14是高阶数组的重写转换规则，该重写转换规则将函数式原语转换为由命令式原语组成的中间命令式组合子. 例如，A9中对于给定的函数f和表达式e将中间变量绑定值let_binding e f赋给接收器a，相当于letl中将变量绑定值赋给变量a. A10表明将整个张量赋给接收器等价于逐个对张量中的元素进行赋值操作. A11是张量赋值的并行循环实现，其中mkvPar的实现与mkvSeq相同，该规则表示对张量整体的赋值等价于并行地对张量中的每个元素进行赋值(相当于mkvParl). 重写转换规则A12和A13是将张量元素的最大值以及张量元素规约求和转换为中间命令式组合子maxl和suml. A14用于将if判断的函数式表示等价地转换为命令式条件原语If分别进行赋值.
相应地，翻译器C的重写转换规则如图6所示：
C1至C8是翻译器C针对数值型的重写转换规则. C9至C14是高阶数组的重写转换规则，其中C9表示将中间变量绑定值let_binding e f传给映射函数c(表达式到命令的映射函数)，等价于命令式语句中声明一个临时变量，将中间变量绑定值赋给该临时变量，并在后续命令中继续使用该变量的值，这是生成命令式C代码中临时变量存储结构的核心. 通过存储中间变量，有效解决了代码生成中部分代码翻译不完整的情况. C10和C11是张量构造函数的顺序和并行重写转换规则. C12和C13是针对数组的最大值和元素求和操作的重写转换规则，分别将函数式表示的max和sum转换为中间命令式组合子maxl和suml，并对数组表达式继续应用翻译C的重写转换规则. C14是将函数式表示的if判断操作转换为低级命令式原语If，并对每个判断条件的分量继续翻译.
5.4 显示翻译规则
该部分将命令式原语、数值型的表达式以及数值型的接收器显示翻译为C语句字符串. 显示翻译规则如图7所示：
规则（1）~（7）是针对5.1节中的命令式原语的显示翻译，将命令式原语显示翻译为C语句字符串. 规则（8）~（13）是数值型表达式的显示翻译，规则（14）（15）是数值型接收器的显示翻译.
由于本文采用的是基于有限集的下标索引到元素值的映射函数所构造的张量表达式，因此生成的命令式C代码不存在下标越界的错误. 下面是基于上述重写转换规则和显示翻译规则生成的2维张量卷积算子Conv2d的命令式OpenMP C代码：
float v0[2 * p ＋ m1][2 * p ＋ m2];
for (int i1 = 0; i1 < 2 * p ＋ m1; i1 ＋= 1){
for (int i2 = 0; i2 < 2 * p ＋ m2; i2 ＋= 1){
if (i1 < p && i2 < p){
v0[i1][i2] = 0; }
else{if (p <= i1 && i1 < p ＋ m1 && p <= i2
&& i2 < p ＋ m){
v0[i1][i2] = input[i1 － p][i2 － p]; }
else{
v0[i1][i2] = 0;}
}
}
}
# pragma omp parallel for
for (int i2 = 0; i2 < (m1 － n1 ＋ 2 * p) / s ＋ 1; i2 ＋= 1){
# pragma omp parallel for
for (int i3 = 0; i3 < (m2 － n2 ＋ 2 * p) / s ＋ 1; i3 ＋= 1){
float v4;
v4 = 0;
for (int i5 = 0; i5 < n1; i5 ＋= 1){
float v6;
v6 = 0;
for (int i7 = 0; i7 < n2; i7 ＋= 1){
v6 = ((v0[i2 * s ＋ i5][i3 * s ＋
i7] * kernel[i5][i7]) ＋ v6);
}
v4 = (v6 ＋ v4);
}
out[i2][i3] = v4;
}
}
具体的翻译步骤如下.
输入：变量接收器out，带并行策略的函数式2维张量卷积算子表达式Conv2d，填充因子p，步长s，卷积核kernel2d，输入张量input2d；
输出：命令式2维卷积算子OpenMP C代码.
①展开函数式卷积算子Conv2d得到：
A(vwt "out", tlet pad := Padding2d p input2d in mkvPar (λi0. mkvPar (λj0. sum (mkvSeq (λi1. sum (mkvSeq (λj1. mul (pad |[i0 × s ＋ i1]) |[j0 × s ＋ j1] (kernel2d |[i1]) |[j1]))))))).
②应用翻译器A的重写转换规则A9(Alet)，将中
间变量绑定值tlet转换为中间命令式组合子letl，得到如下表达式：
C(Padding2d p input2d, λx. letl x (λx1 o. A(o, mkvPar (λi0. mkvPar (λj0. sum (mkvSeq (λi1. sum (mkvSeq (λj1. mul (x1|[i0 × s ＋ i1]) |[j0 × s ＋ j1] (kernel2d |[i1]) |[j1])))))))) (vwt "out")).
③展开中间命令式组合子letl得到：
C(Padding2d p input2d, λx. A(vwt "out", mkvPar (λi0. mkvPar (λj0. sum (mkvSeq (λi1. sum (mkvSeq (λj1. mul (x|[i0 × s ＋ i1]) |[j0 × s ＋ j1] (kernel2d |[i1]) |[j1])))))))).
④展开Padding2d的定义得到：
C(mkvSeq (λi. mkvSeq (λj. if (i < p) && (j <p) then zero else if (p <= i) && (i < p ＋ m1) && (p <= j) && (j < p ＋ m2) then (input2d |[i － p]) |[j － p] else zero)), λx. A(vwt "out", mkvPar (λi0. mkvPar (λj0. sum (mkvSeq (λi1. sum (mkvSeq (λj1. mul (x|[i0 × s ＋ i1]) |[j0 × s ＋ j1] (kernel2d |[i1]) |[j1])))))))).
⑤应用翻译器C的重写规则C10(CmkvSeq)，将
整个表达式转换为2部分. 首先声明一个类型为2维张量的临时变量tmp(tmp为接收器变量w和表达式v的对偶(w, v))，并将表达式的值赋给该变量w. 接着，在后续命令中继续使用该变量的值v：
CG_comm (new (λtmp. A(w, mkvSeq (λi. mkvSeq (λj. if (i < p) && (j < p) then zero else if (p <= i) && (i < p ＋ m1) && (p <= j) && (j < p ＋ m2) then (input2d |[i － p]) |[j － p] else zero)))) ;
A(vwt "out", mkvPar (λi0. mkvPar (λj0. sum (mkvSeq (λi1. sum (mkvSeq (λj1. mul (v|[i0 × s ＋ i1]) |[j0 × s ＋ j1] (kernel2d |[i1]) |[j1])))))))).
⑥接着，应用命令的显示翻译规则(5)(CGnew)和
规则(3)(CGseq)，显示翻译出接收器变量v0，以及命令的顺序执行：
“float v0[((2) * (p)) ＋ (m1)][((2) * (p)) ＋ (m2)];” ++ A(v0, mkvSeq (λi. mkvSeq (λj. if (i < p) && (j < p) then zero else if (p <= i) && (i < p ＋ m1) && (p <= j) && (j < p ＋ m2) then (input2d |[i － p]) |[j － p] else zero))) ++ A(vwt "out", mkvPar (λi0. mkvPar (λj0. sum (mkvSeq (λi1. sum (mkvSeq (λj1. mul (v0|[i0 × s ＋ i1]) |[ j0 × s ＋ j1] (kernel2d |[i1]) |[j1]))))))).
其中“++”是字符串的连接. 此时整个表达式的翻译分为2部分：第1部分是针对填充操作的翻译，第2部分是针对卷积的翻译.
⑦第1部分针对填充操作的翻译，分别应用2次
A10(AmkvSeq)，1次A14(Aif)，并展开中间命令式组合子mkvSeql，以及2次显示翻译规则(6)(CGfor)，1次显示翻译规则(2)(CGif)和规则(6)(CGfor)即可得到相应命令式C代码.
⑧第2部分卷积的翻译. 首先，应用翻译器A的
重写转换规则A11(AmkvPar)，并展开mkvParl，将mkvPar转换为并行执行的命令式循环操作：
CG_comm (parfor (vwt "out") (λi o. A(o, mkvPar (λj0. sum (mkvSeq (λi1. sum (mkvSeq (λj1. mul (v0|[i × s ＋ i1]) |[ j0 × s ＋ j1] (kernel2d |[ i1]) |[ j1])))))))).
⑨接着，应用显示翻译规则(7)(CGparfor)将命令
式原语parfor显示翻译为字符串：
“#pragma omp parallel for
for (int i2=0; i2 < ((((m1) － (n1)) ＋ ((2) * (p))) / (s)) ＋ (1); i2 ＋= 1) {” ++ A((vwt "out") |{i2}, mkvPar (λj0. sum (mkvSeq (λi1. sum (mkvSeq (λj1. mul (v0|[ i2 × s ＋ i1]) |[ j0 × s ＋ j1] (kernel2d |[ i1]) |[ j1])))))).
⑩继续翻译后面的表达式. 应用翻译器A的重写
转换规则A11(AmkvPar)，展开mkvParl，并应用显示翻译规则(7)(CGparfor)得到：
“#pragma omp parallel for
for (int i3=0; i3 < ((((m2) － (n2)) ＋ ((2) * (p))) / (s)) ＋ (1); i3 ＋= 1) {” ++ A(((vwt "out") |{i2}) |{i3}, sum (mkvSeq (λi1. sum (mkvSeq (λj1. mul (v0|[ i2 × s ＋ i1]) |[ i3 × s ＋ j1] (kernel2d |[ i1]) |[ j1]))))).
⑪应用翻译器A的重写转换规则A13(Asum)，
并展开命令式组合子suml和翻译器C：
CG_comm (new (λtmp. w |:= zero ; for (λi. A(w, add (mkvSeq (λi1. sum (mkvSeq (λj1. mul (v0|[ i2 × s ＋ i1]) |[ i3 × s ＋ j1] (kernel2d |[ i1]) |[ j1])))) |[i] v)) ; A(((vwt "out") |{i2}) |{i3}, v))).
⑫应用命令的显示翻译规则(5)(CGnew)，声明1
个数值型的临时变量. 此时，剩余的表达式包含3个命令的顺序执行，重复应用显示翻译规则(3)(CGseq)得到：
“float v4;” ++ CG_comm (v4 |:= zero) ++ CG_comm (for (λi. A(v4, add (mkvSeq (λi1. sum (mkvSeq (λj1. mul (v0|[ i2 × s ＋ i1]) |[ i3 × s ＋ j1] (kernel2d |[ i1]) |[ j1])))) |[i] v4))) ++ CG_comm (((vwt "out") |{i2}) |{i3} |:= v4).
⑬剩余的命令中，第1和第3个是简单的赋值命
令，应用显示翻译规则(4)(CGassign)即可完成翻译. 针对第2个命令的翻译，首先应用显示翻译规则(6)(CGfor)得到：
“for(int i5 = 0 ; i5 < n1; i5 ＋= 1) {” ++ A(v4, add (mkvSeq (λi1. sum (mkvSeq (λj1. mul (v0|[ i2 × s ＋ i1]) |[ i3 × s ＋ j1] (kernel2d |[ i1]) |[ j1])))) |[i5] v4).
⑭接着，应用3.1节中mkvSeq与idx之间的引理
idx_mkvSeq得到：
A(v4, add (sum (mkvSeq (λj1. mul (v0|[ i2 × s ＋ i5]) |[ i3 × s ＋ j1] (kernel2d |[ i5]) |[ j1]))) v4).
⑮应用翻译器A的重写转换规则A2(Aadd)得到：
C(sum (mkvSeq (λj1. mul (v0|[ i2 × s ＋ i5]) |[ i3 × s ＋ j1] (kernel2d |[ i5]) |[ j1])), λx. C(v4, λy. v4 |:= add x y)).
⑯应用翻译器C的重写转换规则C13(Csum)并
展开suml和翻译器C的定义得到：
CG_comm (new (λtmp. w |:= zero ; for (λi. A(w, add (mkvSeq (λj1. mul (v0|[ i2 × s ＋ i5]) |[ i3 × s ＋ j1] (kernel2d |[ i5]) |[ j1])))|[i] v) ; (v4 |:= add v v4))).
⑰接下来，重复步骤⑪~⑭即可将表达式中剩
余的所有函数式原语转换为命令式原语，最后应用显示翻译规则翻译为OpenMP C代码的字符串.
从函数式卷积表达式到OpenMP C代码的翻译在Coq中的验证过程如图8(Coq截图)所示.
本文成功从函数式神经网络算子表达式出发，生成了一批神经网络算子的OpenMP C代码.
我们将生成的神经网络算子C代码与手工编写的算子C代码，以及顺序执行的算子C代码与带OpenMP并行执行的算子C代码进行性能比较. 本次测试使用的处理器为Intel(R) i7-12700H @ 2.30GHz(6核＋8核). 主要测试结果如表7所示：
表 7 测试结果Table 7. Test Results算子操作 张量规模 顺序执行时长/s 并行执行时长/s 加速比 生成代码 手工编写 生成代码 手工编写 生成代码 手工编写 Conv2d (p, s = 1) 700×700
300×3005.910 935 6.978 041 0.720 788 0.823 746 8.20 8.47 Avgpool2d (k = 2) 8 000×8 000 0.130 755 0.142 020 0.016 803 0.059 553 7.78 2.38 Maxpool2d (k = 2) 8 000×8 000 0.141 180 0.065 849 0.022 787 0.047 422 6.20 1.39 ReLU2d 8 000×8 000 0.081 935 0.082 872 0.022 103 0.023 369 3.71 3.55 Linear2d 2 000×3 000 3 000×4 000 13.760 259 13.848 600 1.355 773 1.418 254 10.15 9.76 实验结果表明，使用代码生成工具生成的神经网络算子C代码与手工编写的算子C代码在质量上可以相媲美，执行结果一致且性能相当. 同时，该工具生成的多核并行OpenMP C算子相比于顺序执行的神经网络算子C代码表现出了显著的性能提升，速度提高了4~10倍. 值得注意的是，本文生成的神经网络算子C代码具有高安全性，能够有效避免人工编写代码时常见的下标越界和存储分配错误.
6. 总结与展望
本文实现了一个基于Coq的带类型函数式深度学习框架Ionia. 该框架具有足够大的表达能力，所构建的模型涵盖了生成对抗网络、卷积神经网络及循环神经网络等. 同时，实验验证了该学习框架能够自动静态检测到神经网络模型中的张量形状不匹配错误，且无任何时间开销. 此外，本文设计并实现了一系列重写转换规则，用于将函数式神经网络算子表达式翻译为命令式C代码. 最终成功生成了一批高可信高安全的神经网络算子OpenMP C代码，相比顺序执行的算子C代码，速度有了大幅提升.
后续计划包含以下3部分：1）在Coq定理证明器中严格证明从函数式神经网络算子表达式到命令式原语的重写转换规则的正确性，以此严格证明生成的神经网络算子C代码的可靠性；2）在函数式层面对神经网络算子进行优化及正确性验证，包括各种优化调度策略，如循环融合、循环拆分、循环重组等Halide调度指令，并将优化后的算子翻译为相应的C代码，以保证生成代码的高效可靠性；3）将代码生成扩展到GPU和其他AI加速器上，使得生成的代码能够充分利用AI硬件的并行计算能力. 本文所做的工作为构建高可靠、高安全、高性能的AI编译器提供了一种新的方案.
作者贡献声明：张晓丽负责完成实验并撰写论文；陈钢提出实验方案设计思路并修改论文；麻莹莹提出基础方案设计；胡萍提供方案思路.
-
![]()
图 3 顶点对应合并边相互平行时构造边的几种情形
Figure 3. Vertices correspond to several cases in which edges are constructed when merged edges are parallel to each other
![]()
图 4 顶点对应合并边相互垂直时构造边的几种情形
Figure 4. Several cases of constructing edges when vertices correspond to merging edges perpendicular to each other
![]()
图 6 带权有向图G构造结果示意图
Figure 6. Diagram of the construction result of weighted directed graph G
![]()
图 7 取点的几种限制关系示意图
Figure 7. Schematic diagram of several limiting relationships of acquisition points
![]()
图 13 经预先分层后权重weight(e)为100时PCB9的布线结果
Figure 13. Routing results of PCB9 with weight(e) of 100 after pre-layering
表 1 基准印刷电路板设计统计
Table 1 Benchmark Printed Circuit Board Design Statistics
设计 引脚数 焊盘数 过孔数 未布线线网数 总线群组组数 PCB1 10 10 0 5 1 PCB2 10 10 5 5 1 PCB3 16 32 22 8 1 PCB4 20 40 31 10 1 PCB5 20 40 31 10 2 PCB6 30 163 12 15 5 PCB7 84 172 86 42 3 PCB8 140 286 173 140 4 PCB9 6 12 12 3 1 
下载: 导出CSV
表 2 各方法的布线结果比较
Table 2 Comparison of Routing Results Between Method 1, Method 2 and the Method in This Paper
设计 布通率 /% 运行时间 /s DRV次数 方法1 方法2 本文方法 方法1 方法2 本文方法 方法1 方法2 本文方法 PCB1 100 100 100 0.03 0.008 0.001 0 0 0 PCB2 100 100 100 0.11 0.025 0.003 0 0 0 PCB3 100 100 100 0.7 0.19 0.023 1 0 0 PCB4 100 100 100 1.5 0.35 0.041 3 0 0 PCB5 100 100 100 1.5 0.37 0.048 3 0 0 PCB6 93.3 100 100 8.2 2.4 0.21 7 0 0 PCB7 57.1 97.6 100 94.7 13.2 2.1 15 2 0 PCB8 - 64.8 100 - 109.7 16.4 - 106 0 “-”表示未布通
下载: 导出CSV
表 3 各方法的群组布线性能指标比较
Table 3 Comparison of Group Routing Performance Metrics Between Method 1, Method 2 and the Method in This Paper
设计 方法1 方法2 本文方法 CW CS CC Ctotal CW CS CC Ctotal CW CS CC Ctotal PCB1 1.04 1.67 4.04 6.75 1.01 1.00 3.50 5.51 1.16 1.67 1.00 3.83 PCB2 1.06 1.67 4.21 6.94 1.12 2.00 1.00 4.12 1.16 1.50 1.00 3.66 PCB3 1.07 2.00 4.36 7.43 1.17 1.50 1.00 3.67 1.29 1.32 1.00 3.61 PCB4 1.05 2.33 4.56 7.94 1.21 1.86 1.00 4.07 1.39 1.35 1.00 3.74 PCB5 1.05 2.33 4.56 7.94 1.14 2.00 1.00 4.14 1.17 1.22 1.00 3.39 PCB6 1.34 2.75 3.98 8.07 1.40 2.50 1.00 4.90 1.37 2.40 1.00 4.77 PCB7 1.20 2.13 4.29 7.62 1.20 1.82 1.00 4.02 1.18 1.60 1.00 3.78 PCB8 - - - - 1.35 1.90 1.00 4.25 1.37 1.72 1.00 4.09 “-”表示未布通
下载: 导出CSV
-
[1] Hsu J, Hung G, Tseng J, et al. High-speed data center PCB design challenges and findings by Intel® automatic in-board characterization[C/OL]// Proc of the 17th Int Microsystems, Packaging, Assembly and Circuits Technology Conf. Piscataway, NJ: IEEE, 2022[2024-04-08]. https://ieeexplore.ieee.org/document/9966724
[2] Tan Yan. Algorithmic studies on PCB routing[D]. Urbana-Champaign: University of Illinois at Urbana-Champaign, 2010: 15−27
[3] Lin S T, Wang H H, Kuo C Y, et al. A complete PCB routing methodology with concurrent hierarchical routing[C]//Proc of the 58th ACM/IEEE Design Automation Conf. Piscataway, NJ: IEEE, 2021: 1141−1146
[4] Lin T C, Merrill D, Wu Y Y, et al. A unified printed circuit board routing algorithm with complicated constraints and differential pairs[C]//Proc of the 26th Asia and South Pacific Design Automation Conf. New York: ACM, 2021: 170−175
[5] 邓新国,叶似锦,陈家瑞,等. 结合改进A*算法与拆线重布的有序逃逸布线[J]. 电子与信息学报,2021,43(6):1609−1616 doi: 10.11999/JEIT201033 Deng Xinguo, Ye Sijin, Chen Jiarui, et al. Ordered escape routing combining improved A* algorithm with rip-up and reroute[J]. Journal of Electronics & Information Technology, 2021, 43(6): 1609−1616 (in Chinese) doi: 10.11999/JEIT201033
[6] Save Y D, Rakhi R, Shambhulingayya N D, et al. Oscad: An open source EDA tool for circuit design, simulation, analysis and PCB design[C]//Proc of the 20th Int Conf on Electronics, Circuits, and Systems. Piscataway, NJ: IEEE, 2013: 851−854
[7] Goyal P, Agrawal H, Paradiso J A, et al. BoardLab: PCB as an interface to EDA software[C]//Proc of the 26th Annual ACM Symp on the Djunct Publication of the User Interface Software and Technology. New York: ACM, 2013: 19−20
[8] CAMA). Piscataway,NJ:IEEE,2018[2024-04-08]. https://ieeexplore.ieee.org/document/8530652 (没有届 Wane S, Patton R, Gross N. Unification of instrumentation and EDA tooling platforms for enabling smart chip-package-PCB-probe arrays co-design solutions using advanced RFIC technologies[C/OL]//Proc of the 2018 IEEE Conf on Antenna Measurements & Applications
[9] Sherwani N A. Algorithms for VLSI Physical Design Automation[M]. 3rd ed. Berlin: Springer, 2012
[10] Fang S C, Chang K E, Feng W S, et al. Constrained via minimization with practical considerations for multi-layer VLSI/PCB routing problems[C]//Proc of the 28th ACM/IEEE Design Automation Conf. Piscataway, NJ: IEEE, 1991: 60−65
[11] Zhang Cong, Jin Huilin, Chen Jienan, et al. A hierarchy MCTS algorithm for the automated PCB routing[C]//Proc of the 16th Int Conf on Control & Automation. Piscataway, NJ: IEEE, 2020: 1366−1371
[12] Kahng A B,Lienig J. 超大规模集成电路物理设计:从图分割到时序收敛[M]. 于永斌,冯策,徐宁,等,译. 2版. 北京:机械工业出版社,2024 Kahng A B, Lienig J. Software Engineering: A Practitioner's Approach[M]. Translated by Yu Yongbin, Feng Ce, Xu Ning, et al. 2nd ed. Beijing: China Machine Press, 2024 (in Chinese)
[13] Kong Hui, Ma Qiang, Yan Tan, et al. An optimal algorithm for finding disjoint rectangles and its application to PCB routing[C]//Proc of the 47th Design Automation Conf. Piscataway, NJ: IEEE, 2010: 212−217
[14] Zhang Jixin, Xu Ning, Liu Mingyu. FanoutNet: A neuralized PCB fanout automation method using deep reinforcement learning[C]// Proc of the 37th AAAI Conf on Artificial Intelligence. Palo Alto, CA: AAAI, 2023: 8554−8561
[15] He Youbiao, Li Hebi, Jin Tian, et al. Circuit routing using monte carlo tree search and deep reinforcement learning[C/OL]//Proc of the 2022 Int Symp on VLSI Design, Automation and Test. Piscataway, NJ: IEEE, 2022[2024-04-08]. https://ieeexplore.ieee.org/document/9768074
[16] 刘郭庆,钱宇华,张亚宇,等. 给定预算下基于相对熵置信区间的蒙特卡洛树搜索最优动作识别算法[J]. 计算机研究与发展,2023,60(8):1780−1794 doi: 10.7544/issn1000-1239.202330257 Liu Guoqing, Qian Yuhua, Zhang Yayu, et al. Best action identification algorithm in Monte Carlo tree search based on relative entropy confidence interval with given budget[J]. Journal of Computer Research and Development, 2023, 60(8): 1780−1794 (in Chinese) doi: 10.7544/issn1000-1239.202330257
[17] Goh Y, Jung D, Hwang G, et al. Consumer electronics product manufacturing time reduction and optimization using AI-based PCB and VLSI circuit designing[J]. IEEE Transactions on Consumer Electronics, 2023, 69(3): 240−249
[18] Hung S C, Chen Hao, Sun Fankeng, et al. A DAG-based algorithm for obstacle-aware topology-matching on-track bus routing[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2020, 40(3): 533−546
[19] Chen Jingsong, Kuang Jian, Zhao Guowei, et al. PROS 2.0: A plug-in for routability optimization and routed wirelength estimation using deep learning[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2022, 42(1): 164−177
[20] Zhang H T, Fujita M, Cheng C K, et al. SAT-based on-track bus routing[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2020, 40(4): 735−747
[21] Chen Jingsong, Liu Jinwei, Chen Gengjie, et al. MARCH: Maze routing under a concurrent and hierarchical scheme for buses[C/OL]// Proc of the 56th Annual Design Automation Conf 2019. Piscataway, NJ: IEEE, 2019[2024-04-08]. https://ieeexplore.ieee.org/document/8807035
[22] Kim D, Do S, Lee S Y, et al. Compact topology-aware bus routing for design regularity[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2019, 39(8): 1744−1749
[23] Cheng Yihao, Yu Taochun, Fang Shaoyun. Obstacle-avoiding length-matching bus routing considering nonuniform track resources[J]. IEEE Transactions on Very Large Scale Integration Systems, 2020, 28(8): 1881−1892
[24] Yan Jintai,Chen Zhiwei. Obstacle-aware length-matching bus routing[C]//Proc of the 2011 Int Symp on Physical Design. New York:ACM,2011:61−68(没有届 [25] Yan Jintai. Single-layer obstacle-aware multiple-bus routing considering simultaneous escape length[J]. IEEE Transactions on Components, Packaging and Manufacturing Technology, 2022, 12(6): 902−915
[26] Kong Hui, Yan Tan, Wong M D F. Automatic bus planner for dense PCBs[C]//Proc of the 46th ACM/IEEE Design Automation Conf. Piscataway, NJ: IEEE, 2009: 326−331
[27] Wu Peici, Ma Qiang, Wong M D F. An ILP-based automatic bus planner for dense PCBs[C]//Proc of the 18th Asia and South Pacific Design Automation Conf. Piscataway, NJ: IEEE, 2013: 181−186
[28] Tang Hao,Liu Genggeng,Chen Xiaohua,et al. A survey on steiner tree construction and global routing for VLSI design[J]. IEEE Access,2020,8:68593-68622(只有卷 [29] Zachariasen M. A catalog of Hanan grid problems[J]. Networks: An International Journal, 2001, 38(2): 76−83
[30] 赵奇,赵阿群. 一种基于A*算法的多径寻由算法[J]. 电子与信息学报,2013,35(4):952−957 Zhao Qi, Zhao Aqun. A multi-path routing algorithm base on A* algorithm[J]. Journal of Electronics & Information Technology, 2013, 35(4): 952−957 (in Chinese)
[31] 马博宇,徐宁,吴皓莹,等. 面向柔性电路通道区的自动布线算法[J]. 计算机辅助设计与图形学学报,2022,34(8):1179−1185 Ma Boyu, Xu Ning, Wu Haoying, et al. Routing Algorithm for flexible printed circuit channel area[J]. Journal of Computer-Aided Design & Computer Graphics, 2022, 34(8): 1179−1185 (in Chinese)
计量
- 文章访问数: 8
- HTML全文浏览量: 4
- PDF下载量: 4
