没有合适的资源?快使用搜索试试~ 我知道了~
混合信号电路准静态行为的有界模型检查验证方法
理论计算机科学电子笔记153(2006)23-35www.elsevier.com/locate/entcs混合信号电路准静态行为的性质形式验证检查MartinFreibothe,JensSchoünherr,BerndStraube1弗劳恩霍夫集成电路研究所(IIS)埃尔兰根设计自动化部门EAS德国德累斯顿摘要本文提出了一种混合信号电路的验证方法。所提出的流程是基于“有界模型检查”,一种正式的验证方法。混合信号电路的模拟部分的行为分别在电路描述和属性中借助有理数来描述。我们实现的属性检查在有限的时间间隔内给定的混合信号电路设计的形式属性。有理数的内部表示具有几乎任意的精度。通过使用所提出的流程,可以详尽地验证混合信号电路的准静态行为。关键词:有界模型检验,混合信号,准静态1引言在当今的电路设计中通常在这种设计中,模拟部分只占整个芯片面积的相对较小的一部分。相反,混合信号电路的大部分开发时间都花在模拟部分上。数字电路设计可以通过形式验证来发现设计错误。与基于模拟的验证相比,1电子邮件:{freibothe,schoenherr,straube} @ eas.iis.fraunhofer.de1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2006.01.02724M. Freibothe等人/理论计算机科学电子笔记153(2006)23正式验证技术达到100%覆盖电路设计的功能然而,在当前应用于混合信号电路的验证流程中,模拟和数字部分分别通过仿真和正式验证进行验证然后,基于仿真对电路的整体行为进行验证,从而对模拟和数字部分的连接进行验证所有基于模拟的验证方法都有需要测试台和模拟激励的缺点提供这两种功能需要大量的手动操作。尽管有这种缺点,但只能实现电路功能性的相对低的在这项工作中,验证流程的形式验证混合信号电路的准静态行为。所提出的方法是基于“有界模型检查”的方法。这种方法是数字电路设计验证的最新技术我们扩展了这种方法,以使其应用到模拟电路。目前,“有界模型检验”的大多数应用然而,在本文中,我们还允许在描述电路行为和规范的公式使用算术使用此扩展,我们现在可以将此验证流程应用于由模拟和数字部件组成的电路,即混合信号电路。2现有技术文献中介绍了混合信号电路的形式验证的不同方法[10,11]的作者提出了一种在功能级验证混合信号电路设计的方法。设计的模拟部分的功能行为由表示电路的准静态行为的符号模型来描述在这些模型中,模拟电压由有限间隔的这些数字使用有限长度的布尔向量进行编码这些向量的有限长度一方面限制了这种验证流的准确性,另一方面也引入了对验证流的算术问题。这些问题极大地限制了这种方法的可用性。定性建模[6,5,15]是基于电路的模拟部分表示的定性方程(连续性)来自DAE,并用于表示一个抽象的,电路的行为代表模拟电压和电流的实数由三元素集合M={−, 0,+}抽象,从而还原为它们的符号。 可以从该模型导出的所有语句都是M. Freibothe等人/理论计算机科学电子笔记153(2006)2325仅限于集合M的定性值。正如[15]所认识到的,即使是简单的线性系统也不能使用这种方法充分建模‘Timed然而,这种方法的扩展是混合自动机[1,12]。它们用于由离散部件和连续部件组成的系统建模简单的混合信号电路可以用这种确定自动机来表示。然后,通过对自动机的状态空间进行可达性分析来进行电路设计。即使在强约束下,例如变量的分段常数导数,可达性问题对于这类自动机仍然是不可判定的,因为状态空间通常是无限的[13,14]。最近的混合自动机的验证方法利用不同的技术来近似可达状态集。然后将标准模型检查算法应用于这些有限状态抽象[8,9]。文[3]中提出的方法建议对一类混合系统进行可达性分析,以得到精确解的分段线性逼近,这些混合系统这些方法的缺点是它们引入了近似误差,不是合理的[9],或者它们的性能取决于可达状态集的形状[3]。[ 2 ]中提出了一种混合离散-连续系统的“有界模型检验”和归纳验证方法的概念一个混合离散-连续系统描述被转换成一个组合SAT/算术问题的实例这种转换的结果表示实际问题的分段线性过度近似。建议将不同的验证和分析方法结合起来,以解决SAT和优化问题,如MILP作为验证过程的结果可能出现的反例将被反向转换到原始的离散-连续域。这种方法的一个主要缺点是实际问题的分段线性过度近似。因此,任何生成的反例再次只是一个过度近似,并且其到混合自动机的有效路径的反向转换不是微不足道的。这个翻译任务被转换成一组搜索问题,而状态转换的输入值的可能范围决定了必须遍历的搜索空间由于在这种方法中使用整数来表示混合信号电路的模拟部分,因此必须处理诸如有限的精度和在流水线上的算术等问题这些问题限制了该方法用于验证模拟元件的可用性。26M. Freibothe等人/理论计算机科学电子笔记153(2006)23在[16]中,提出了一种混合信号电路准静态行为的半形式验证方法所提出的方法是基于SAT的属性检查。所述验证流程的起点是VHDL中混合信号电路的准静态行为描述。在这样的电路描述中,使用VHDL给出了这样一个混合信号电路描述,一个面向验证的模型推导出SAT为基础的属性检查进行。在面向验证的模型中,用于描述模拟行为的浮点型实数被抽象为有限区间的整数这种模型由有限Mealy自动机表示,因此可以使用完善的形式验证方法进行验证。然而,面向验证的模型只是电路的VHDL行为描述的量化表示。因算术运算而可能产生的过流在这种情况下,必须调整量化参数,并且必须重新运行验证。选择的模型精度越高,验证问题就越复杂这种验证流程的缺点是一方面利用抽象(所谓的“面向验证”)模型进行验证,另一方面在创建面向验证的3验证流程验证的任务是检查电路设计是否符合其规范。为了检查给定的混合信号电路是否没有设计错误,建议的验证流程需要正式规范。这样一个规范必须作为一组形式属性来提供。这些形式属性是从电路的语言规范中手动推导出来的。本文提出的混合信号电路设计的形式验证方法是基于“有界模型检验”的原理这种验证技术在有限的时间间隔内检查给定电路的形式属性我们已经实现了一个原型,属性,为所提出的验证流程。该属性检查器利用有效性检查器SVC [17]来检查公式的有效性SVC支持要检查的公式中的算术表达式图1左侧描述了使用属性验证的整体正式验证流程该原型期望混合信号电路设计作为自动机,并以属性的形式作为输入的形式规范。结果,属性检查器返回信息,即给定的属性是否适用于该混合信号电路M. Freibothe等人/理论计算机科学电子笔记153(2006)2327质量标准自动机正式财产SVC误差财产持有误差财产持有图1. 拟议的核查流程使用财产权我们提出的使用有效性检查器SVC检查混合信号电路的属性的有效性的流程如图1所示。利用性质中的假设条件确定迭代阵列的长度,将表示混合信号电路的自动机转化为其内部的迭代阵列表示再次使用该属性的假设,在后续步骤中从该迭代数组导出一阶逻辑公式。该公式的正确性体现了该性质在数模混合电路设计中的正确性该公式被移交给SVC,在那里检查其有效性结果,人们得到的信息是否为电路的属性。如果该属性无法保持,将生成一个反例,可用于调试。3.1电路描述我们认为,用DAE表示模拟行为过于详细,因此不适合对混合信号电路的模拟和数字组件的相互作用进行正式验证。相反,我们提出的验证流程是基于对电路行为的更抽象的看法。混合信号电路被描述为一个确定性的抽象Mealy自动机作为输入的属性-转换器。由于电路表示为自动机,只有它的准静态,稳态行为可以在模型中描述我们选择了一个简单的XML语法物业-酒店正式财产XML-自动机电路设计一阶逻辑迭代数组28M. Freibothe等人/理论计算机科学电子笔记153(2006)23作为自动机形式的混合信号电路设计的描述语言,因为这需要开发相当简单的解析器。这种自动机由内部变量、输入和状态变量以及状态转移函数δ和输出函数λ描述。对于这些描述,可以使用类型bool和rat 这两种类型可以分别用于定义常数、变量和二值逻辑和有理数的表达式。此外,语言元素,如if-then-else语句,通常的布尔运算和算术运算,如加,减,乘和除与常数除数在有理数范围内可用。由于允许在自动机的描述中使用有理数,因此这种自动机的输入符号集是无限的因此,所提出的方法中表示混合信号电路的自动机是无限的。在这种电路描述中,混合信号电路的数字元件通过使用有理数(类型:rat),可以额外描述模拟元件的行为。使用有理数来描述模拟行为是非常精确的,因为有理数是密集的。图2显示了一个时序混合信号电路的示例该电路的XML行为描述如图3所示。这样的XML描述被用作属性查询的输入。根据价值i模式DFFin0 in1MUX+ 2:1输出V型时钟DFFMUX二比一500 Ω1000 Ω2000 Ω图2.示例混合信号电路的原理图在混合信号电路的数字输入I模式中,在下一个时钟周期中选择两个模拟输入IN0或 IN1 中的 一个 所选模 拟输 入端的 电压 将分别 以( 1 + 1000Ω/2000Ω)或(1 + 1000Ω/ 500Ω)的系数放大,具体取决于数字M. Freibothe等人/理论计算机科学电子笔记153(2006)2329在前一时钟周期期间输入V模式。放大后的电压可以在电路在自动机的XML描述中,定义内部变量或输出变量值的输出函数λi在关键字def之后指定。状态转移函数δi在自动机的描述中在关键字next之后指定,为状态变量si返回下一个时钟周期中的相应值。<模块名称=“示例”><在名称=“v_mode”类型=“bool”/><在名称=“i_mode”类型=“布尔”/> <输出名称=“输出”类型=“大鼠”def=“(o1)”/> <内部名称=“j1”type =“rat”def =“(ite(i_mode_d)in1 in0)”/><内部名称=“r1”type =“rat”def =“(ite(v_mode_d)500| 1 2000| 1)”/><内部名称=“o1”type=“rat”def=“(* j1(/(+1000| 1 r1)r1))”/>模块>图3. 示例混合信号电路3.2物业描述给定混合信号电路设计的形式规范通常由一组形式属性组成。如果所有的形式性质都被证明是有效的性质,规格为混合信号电路。作为所提出的流程的输入,需要以离散的线性时间命题逻辑的语言提供要检查的形式属性。形式属性基本上由关于混合信号电路的输入、输出、状态和内部线路的时间戳假设组成我们的验证流程中使用的模型从连续时间抽象到离散时间点。在属性中,时间点由有限间隔的整数Z表示因此,它只可能指定准静态,稳态行为的混合信号电路设计的性质。我们建议的验证流程中执行“有界模型检查”的范围以下语言元素可用于制定有关混合信号电路行为的30M. Freibothe等人/理论计算机科学电子笔记153(2006)23(i) 布尔常量和变量simplebool::= constbool|varbool,时间点时间点∈ Z(ii) 表示有理数的常数和变量简单大鼠::=常数大鼠|变量大鼠,时间点时间点∈ Z(iii) 布尔表达式exprbool::= simplebool|(exprbool)|∈{(exprrate* exprrate)|*∈ {=,<,>,≤,≥}(if(exprbool)then exprboolelse exprboolendif)(iv) 表示有理数Q的类型上的表达式exprrat::=简单rat|(exprrat)|∈{+,−,<$}(exprrate/constrate)|(if(exprbool)then exprratelse exprratendif)有一些常用的布尔运算可用于描述混合信号电路的数字行为,这些布尔运算可借助类型bool上的表达式来实现。模拟元件的行为通过使用表示有理数速率类型的常数和变量的表达式的假设来描述。对于这些表达式,可以使用与电路描述中相同的算术运算变量的下标时间点表示该变量在属性中关联的时间点下面给出一个定义形式属性的例子。该特性部分描述了图2所示混合信号电路的行为。((in 0 0≥ 0. 0)n(在0 0≤ 2. 5))→(输出1=src(i模式0)输出1= src(v模式0))(1)src(ai:布尔):=if(ai=false)then in0i+1elsein 1i+1endif(2)ampl(bi:boolean):= if(bi=false)then 1. 5其他3. 0endif(3)一般来说,一个属性被写为一个蕴涵。在它的左边有关于电路的输入和状态在所考虑的间隔的第一时间点的假设。这样的蕴涵的右边通常包含关于电路的输出和下一个状态的假设。含义(1)表示关于待验证的混合信号电路的行为的假设。在含义的左侧,假设0中的模拟输入电压在0和0之间的范围内。0 V和2。在时间点“0”时为5V。在暗示在时间点M. Freibothe等人/理论计算机科学电子笔记153(2006)2331通过电路在给定的示例中,检查属性有效性的验证窗口由区间[0, 1]表示。在给定的性质中,(2)和(3)定义了两个宏。第一个src在下一个时钟周期返回模拟输入0或1,具体取决于其参数a的值。第二个宏ampl返回有理数1。5或3。0,取决于其参数b的值。这个有理数表示放大因子。3.3属性的语义由属性定义的验证窗口确定了“有界模型检查”中的在属性中,时间步长由两个连续整数时间点的差值定义。这等于一个时钟周期的表示的混合信号电路作为自动机。在内部表示中,对于验证窗口给出的有限间隔的每个时间点,混合信号电路被复制一次这样,一个给定的顺序混合信号电路的组合表示,即所谓的验证窗口的左边界始终是整数“0”表示的但是,在写入属性时允许使用负时间戳。在这种情况下,将适当调整核查在时间点图4示出了时序电路作为区间[0,z]内的迭代阵列的表示,z∈Z。在电路的内部表示的每个副本下方,描绘了该副本在迭代阵列内表示的时间点基于混合信号电路出0输出1出Z在0状态0λin1δ态1λinzδ态zλδ态z+10 1z图4. 将电路表示为z+1个时钟周期作为一个迭代数组,一个一阶逻辑的公式,表示要验证的属性的有效性。这样的公式是通过将属性中的变量替换为以下相应的表达式而得出的:32M. Freibothe等人/理论计算机科学电子笔记153(2006)23表示与要替换的变量相同的时间点的电路的副本例如,对于第3.1节中描述的混合信号电路,以下表达式将替换时间点“1”处的变量输出输出1:((if(i mode0)then in11else in 01endif)(((if(v mode0)then500else2000endif)+1000)/1 1 1(if(v mode0)then500else2000endif)1 1在所提出的方法中,主要出现在验证更复杂的电路设计时,避免了“状态空间爆炸”的问题这是因为没有对自动机的状态变量进行可达性分析。因此,拟议核查的结果不存在可能的假阴性。由于时间点“0”处的所有状态变量这也包括电路在现实情况下处于不可达状态的可能性 因此,必须检查任何不成立的属性的反例,以确保它不代表假阴性。在识别出假阴性的情况下,可以将限制时间点“0”处的状态变量的值的假设添加到属性,以便避免不可达的初始状态。3.4调用有效性检查器对于混合信号电路的形式规范所包含的每一个形式属性,该公式的正确性代表了混合信号电路相应性质的正确性在当前版本的Property-100中,使用SVC检查公式的有效性。这个软件是由斯坦福大学开发的。SVC是一个有效性检查器,支持一阶逻辑的可判定子集。它还允许在公式中使用算术表达式可以在算术表达式中使用的有理数使用GMP [7]库表示。因此,有理数表示的准确性仅受可用的本地存储器量的使用GMP库避免了运算过度的发生。到目前为止,SVC只支持公式中线性不等式和线性算术表达式如果形式属性和Mealy自动机表示的混合信号电路是分段线性的,那么这些要求是由属性转换器交给SVC的公式满足的。如果公式被证明是有效的,则该性质对电路成立。其他-M. Freibothe等人/理论计算机科学电子笔记153(2006)2333否则财产就失败了。在这种情况下,将产生一个反例反例可以用来找出导致房产失败的设计错误。有效性检查器SVC无法处理包含具有常数除数的减法或除法算术表达式的公式因此,包含这样的表达式的公式等价地转换为不包含这样的表达式的公式然后将所得公式用作有效性检查器SVC的输入利 用 任 何 其 他 软 件 进 行 公 式 的 有 效 性 检 查 是 容 易 的 。 已 经 使 用Mathematica和SVC的后继者CVCL [4]进行了初步实验CVCL另外支持公式中的某些非线性。由于SVC的局限性,迄今为止,只有分段线性Mealy自动机表示的混合信号电路的分段线性性质才能在性质检验器的帮助下得到形式化的验证。当使用Mathematica等其他工具来检查公式的有效性4评价和结论与混合信号验证领域的其他方法不同,在本文中,模拟元件的行为使用有理数表示。两者的内部表示,混合信号电路和属性提供了一个几乎任意精度的有理数。使用有理数超过整数的两个主要优点是,一方面,有理数表示模拟行为与任意精度,而使用整数的精度是有限的,并在任何情况下引入量化误差。另一方面,验证问题通过使用GMP库来表示有理数,避免了其他方法在算术运算和有限的精度通过这种方式,在数字验证领域建立良好的验证流程“有界模型检查”已经扩展到模拟和混合信号电路。使用这种方法,可以正式验证混合信号电路的准静态行为。以两个简单的混合信号电路为例,将特性验证器的性能与[16]中提出的验证器的性能进行了比较这里介绍的方法基于布尔SAT检查-34M. Freibothe等人/理论计算机科学电子笔记153(2006)23ing.使用属性表的验证流程在运行时间和内存消耗方面实现了更好的性能同时,使用有理数表示模拟分量的精度是任意高的。相反,[16]的方法使用了有限的准确度,必须由用户在验证过程之前指定,因此可能会发生对数据流的算术运算在这种情况下,必须调整量化参数然而,运行时间以指数方式增加,具有为模拟行为建模而选择的精度使用当前版本的属性检查器,只能检查分段线性混合信号电路的分段线性属性。为了允许验证非线性行为,财产管理局必须使用SVC以外的另一种工具来检查公式的有效性。可以很容易地采用由属性检查器移交给该工具的公式的输出格式,以任何其他有效性检查器也可以将特性和混合信号电路的内部表示扩展到其他类型(例如,实数)和运算在他们(例如,求幂和对数函数)。与许多其他数字和混合信号验证方法一样,所提出的使用属性的方法也将连续时间抽象因此,只有混合信号电路的稳态、准静态行为才能使用此验证流程进行验证。然而,即使电路的准静态行为已经被验证,电路的瞬态响应通常也存在约束,这不能用当前版本的特性曲线来验证。因此,未来的工作将集中在验证混合信号电路的动态行为。引用[1] R.巴尔角Courcoubetis,T. A. Henzinger和P. - H.何混合自动机:一种算法方法 到 规格 和 核查 混合系统。In R. L. 格罗斯曼,A. Nerode , A. P. Ravn 和 H. Rischel , 编 辑 , 混 合 系 统 , LNCS 第 736 卷 , 第 209-229 页 。Springer,1993年。[2] B. Becker,M. 别担心,弗。 我是说,我的兄弟。 Franzle,M. Herbstritt,C. He rde,J. 霍尔曼,D. K ron i ng,B. Nebebel,I. 波兰人,和R。 我知道了。离散-连续混合系统的边界建模与验证 ITG/GI/GMM- 讲 习 班 “Methoden und Beschreibungssprachen zur Modelierung und Verifikation von Schaltungen und Systemen”,2004年[3] A. 本波拉德湾Ferrari-Trecate和M.莫拉里分段线性和混杂系统的能观性和能控性IEEE自动控制学报,45:1864[4] Cooperating validity checker lite(CVCL),版本1.1.0。http://verify.stanford.edu/CVCL/,2004年。大学 斯坦福大学[5]J. de Kleer 电路如何工作 《人工智能》,24:205M. Freibothe等人/理论计算机科学电子笔记153(2006)2335[6] J.deKleer和J.S.布朗一种基于连续性的定性物理学。《人工智能》,24:7[7] Gnu多精度算术库,4.1.2版。http://www.swox.com/gmp/,2003年。[8] S. Gupta,B.H. Krogh和R.A.鲁滕巴模拟设计的正式验证。计算机辅助设计,2004年。ICCAD-2004年。IEEE/ACM国际会议,第210- 217页,11月。2004年[9] W.哈通湖 Hedrich和E. 狗吠 用于模拟验证的模型检查算法。在DACACM Press,2002.[10] S. Hendricx和L.克莱森综合混合模式系统形式验证的符号建模方法。在Proceedings of 3rdDesigning Correct Circuits(DCC),1996年9月。[11] S. Hendricx和L.克莱森一个符号核心的方法来正式验证集成的混合模式应用程序。欧洲设计测试会议论文集(ED TC),第432-436页IEEE计算机学会,1997年。[12] T. A.亨辛格混合自动机理论。在Proceedings of the 11 th Annual IEEE Symposium on Logicin Computer Science(LICS 1996)中,第278[13] T. A. Henzinger,P. W. Kopke,A. Puri和P. Varaiya。混合自动机的可判定性是什么?第27届ACM计算理论研讨会(STOC 1995),第373-382页ACM,1995年。[14] T. A. Henzinger和J. - F.拉斯金定时与混杂系统的鲁棒不可判定性。 在南希A. Lynch和Bruce H.Krogh,编辑,混合系统:计算与控制,第三届国际研讨会(HSCC 2000),LNCS第1790卷,第145-159页。斯普林格,2000年。[15] J. Lunze. KünstlicheIntelligenzfurürIngenieure,volumeII. R. OldenbourgVerlag,Muénchen,Wien,1995.[16] J. S chéonh err,M. 弗雷伯,B。 Str au be,and d J. 我是博。 通过基于SAT的属性检查,对混合信号电路的准静态行为进行了详细的验证。 见ISoLA,2004年。[17] Stanford validity checker(SVC),1.1版。http://verify.stanford.edu/SVC/网站,2003.大学 斯坦福大学[18] S. 尤文模型检查时间自动机。In G.Rozenberg和F.Vaandrager,编辑,嵌入式系统讲座,LNCS第1494卷,第114Springer,1998年。
下载后可阅读完整内容,剩余1页未读,立即下载
![application/x-rar](https://img-home.csdnimg.cn/images/20210720083606.png)
![docx](https://img-home.csdnimg.cn/images/20210720083331.png)
![application/x-rar](https://img-home.csdnimg.cn/images/20210720083606.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://profile-avatar.csdnimg.cn/default.jpg!1)
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
我的内容管理 收起
我的资源 快来上传第一个资源
我的收益
登录查看自己的收益我的积分 登录查看自己的积分
我的C币 登录后查看C币余额
我的收藏
我的下载
下载帮助
![](https://csdnimg.cn/release/wenkucmsfe/public/img/voice.245cc511.png)
会员权益专享
最新资源
- 利用迪杰斯特拉算法的全国交通咨询系统设计与实现
- 全国交通咨询系统C++实现源码解析
- DFT与FFT应用:信号频谱分析实验
- MATLAB图论算法实现:最小费用最大流
- MATLAB常用命令完全指南
- 共创智慧灯杆数据运营公司——抢占5G市场
- 中山农情统计分析系统项目实施与管理策略
- XX省中小学智慧校园建设实施方案
- 中山农情统计分析系统项目实施方案
- MATLAB函数详解:从Text到Size的实用指南
- 考虑速度与加速度限制的工业机器人轨迹规划与实时补偿算法
- Matlab进行统计回归分析:从单因素到双因素方差分析
- 智慧灯杆数据运营公司策划书:抢占5G市场,打造智慧城市新载体
- Photoshop基础与色彩知识:信息时代的PS认证考试全攻略
- Photoshop技能测试:核心概念与操作
- Photoshop试题与答案详解
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035111.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)