ASIP体系结构形式化建模与验证方法研究
摘要
专用指令集处理器(Application Specific Instructions Set Processor,ASIP)是专为某个或某类应用而设计的处理器。随着ASIP体系结构的不断发展,设计的复杂性不断增加,如何有效地验证体系结构设计的正确性问题在ASIP设计中日益突出。ASIP体系结构本身具有指令行为定义的多样性和逻辑结构设计的灵活性等特点,使得构造验证模型与精确地刻画系统特征非常困难,尚未形成一套能够有效地解决ASIP体系结构层设计自动验证问题的理论和方法。
本文针对上述问题,在分析ASIP体系结构的层次化设计特征的基础上,提出了基于Petri网理论和模型检测方法的ASIP体系结构验证框架,对ASIP体系结构进行描述和验证。通过对已有的ASIP体系结构设计的分析,将ASIP体系结构需要满足的属性分为静态属性和动态属性两个方面,分别进行研究。静态属性是指系统中的结构特征和单条指令的执行情况的检测,动态属性关注的是指令并发执行设计的正确性,主要包括与数据相关、控制相关等方面相关的控制结构设计的正确性的检测。主要研究工作包括:
(1)基于Petri网描述ASIP体系结构。首先根据ASIP体系结构设计的特点提出一个新的扩展的Petri网——HDPN(Hardware design based-on Petri Net),用其描述ASIP体系结构,刻画处理器设计中的结构和行为特征。然后给出ASIP设计需要满足的静态属性,用以检测ASIP设计中的静态需求是否得到满足。
(2)基于模型检测方法对动态属性进行验证。首先建立待验证的ASIP体系结构模型并提取该模型需要满足的动态属性,然后采用模型检测工具对模型和动态属性的一致性进行验证。本文给出了基于模型检测方法建立ASIP体系结构模型的方法,针对流水线处理器和乱序处理器两种抽象处理器描述了具体的建模方法,分析了它们的动态属性,并对其进行了验证,证明了此方法的有效性。
(3)结合ASIP设计的层次化特点,提出了层次化和局部化的建模方法。采用抽象模型描述设计的整体特性,采用细化模型来刻画局部设计的细节,从而控制模型的规模,规避模型检测方法中的状态空间爆炸问题。
(4)提出了从HDPN描述到模型检测描述的转换规则。在此基础上,实现了一个支持结构检测和指令执行正确性检测的体系结构验证框架。
本文做出的贡献主要体现在:
(1)面向体系结构建模的需求,基于Petri网理论,提出了一种ASIP体系结构描述方法——HDPN。HDPN继承了Petri网的直观性特点,可以很好地刻画体系结构中模块间的互连关系;在此基础上加强了对设计中的存储单元、功能单元以及数据通路的刻画,通过对Petri网中的基本元素——库所、变迁和弧的扩展,分别对存储单元中存储的数据添加了类型定义,对功能部件添加了接口参数、执行条件和具体的行为描述,对数据通路定义了所传递的参数,提高了模型的描述能力。基于HDPN描述提出ASIP设计需要满足的静态属性,对设计的结构描述正确性和单条指令执行的正确性进行验证。
(2)将模型检测方法应用于ASIP体系结构验证中。提出了基于模型检测方法建立ASIP体系结构模型的方法,针对流水线处理器和乱序执行处理器描述了具体的建模方法,并给出了处理器正确执行所需满足的属性。在建模时采用分层和局部建模的方法有效规避模型检测方法中的状态空间爆炸问题,提高了模型检测方法的可用性。
(3)建立了HDPN描述和模型检测描述之间的转换规则,形成一个完整的ASIP体系结构验证框架。将ASIP体系结构的验证问题合理地划分为静态属性(结构正确性和单条指令执行的正确性问题)和动态属性(指令并行执行的正确性问题)两个子问题,分别通过基于Petri网的静态属性检测方法和基于模型检测的动态属性的检测方法对其描述和验证。
Application Specific Instructions Set Processors(ASIP) is a kind of special processor designed for a particular type of applications.With the continuous development of ASIP design,the complexity of the design is also increasing,and the verification efforts on the correctness of design are increasingly prominently accordingly.Due to the diversity of instructions' behaviors and the flexibility of logical structures,it is very difficult to build a general method to verify the correctness of the ASIP design automaticly.So far,there is not any effective theory and methodology on the automatic verification of ASIP design at architecture level.
On the problems mentioned above,the hierarchy characteristics of ASIP architecture design were analyzed deeply.A framework on the verification of ASIP architecture design,which is based on Petri Net and Model Checking theory and methodology,is presented in this thesis.The properties which an ASIP design needs to satisfy are divided into static properties and dynamic properties.Static properties are used to specify the requirements of structure and individual instructions' execution,while dynamic properties are used to specify the requirements of concurrent instructions.The main research works include:
(1) Description of the ASIP architecture based on Petri net.Hardware Design based-on Petri Net(HDPN),an extended Petri net,is used to describe the structural and behavioral characteristics of ASIP architecture.The static properties which an ASIP design should obey are also proposed.
(2) Verification of the dynamic properties based on Model Checking.Firstly, the model of ASIP architecture to be validated is constructed,and the dynamic properties which a processor should obey are extracted from customer-built requirements.Then model checker is used to check the consistency of the model and of the properties.The method is applied to a pipeline processor and an out-of-order processor to prove the availability.
(3) Modeling method based on the hierarchical and local characteristic of ASIP design.In order to efficiently verify the design,the models' scale should be restricted.Two kinds of models,global design and local models are constructed in this method.The global design,in which many details are hidden to reduce the scale of the model,is used to check the validity of the interaction between the components. While local models,in which concrete designs of each individual component are described,are used to verify detailed specifications.In this situation,the other parts of the design are treated as outer environment,and the interface parameters of the model are set as stochastic values in the possible range.
(4) The translation rules from HDPN based description to model checker based description.Based on the translation procedure,a verification framework which supports the validation on the correctness of structures and instructions' execution of an ASIP architecture design is constructed
The main contributions of this thesis are as follows:
(1) Aiming to the design of ASIP architecture,a novel extended Petri Net model named HDPN is introduced.It can describe target architecture in a succinct and precise way.In HDPN,tokens are endowed with concrete information according to the specific design,but not only a black dot in traditional Petri Net.Therefore the elements in the Places are added with types.And transitions,which are used to describe the function units,are appended with interface parameters,execution conditions and concrete action description.Arcs,which are used to describe data path,are also appended with parameters.To sum up,as a modeling tool,HDPN can sufficiently describe the structural information and individual instructions' execution of the ASIP architecture.The method based on HDPN,taking advantage of it,can efficiently verify the static properties accordingly.
(2) Model checking is applied to the verification of ASIP architecture. Modeling method based on hierarchical and local description is presented and used to abstract models from a pipeline processor and an out-of-order execution processor. These modeling methods are effective to avoid state space explosion.The dynamic properties used to check the correctness of a processor execution are also proposed.
(3) The translation rules from HDPN description to the input language of model checker-NuSMV are presented.Therefore,an integrated framework for ASIP architecture verification is built.The properties for the verification are divided into static properties and dynamic properties.They are checked through the static property checking method based on HDPN and dynamic property checking method based on model checking,separately.
本文针对上述问题,在分析ASIP体系结构的层次化设计特征的基础上,提出了基于Petri网理论和模型检测方法的ASIP体系结构验证框架,对ASIP体系结构进行描述和验证。通过对已有的ASIP体系结构设计的分析,将ASIP体系结构需要满足的属性分为静态属性和动态属性两个方面,分别进行研究。静态属性是指系统中的结构特征和单条指令的执行情况的检测,动态属性关注的是指令并发执行设计的正确性,主要包括与数据相关、控制相关等方面相关的控制结构设计的正确性的检测。主要研究工作包括:
(1)基于Petri网描述ASIP体系结构。首先根据ASIP体系结构设计的特点提出一个新的扩展的Petri网——HDPN(Hardware design based-on Petri Net),用其描述ASIP体系结构,刻画处理器设计中的结构和行为特征。然后给出ASIP设计需要满足的静态属性,用以检测ASIP设计中的静态需求是否得到满足。
(2)基于模型检测方法对动态属性进行验证。首先建立待验证的ASIP体系结构模型并提取该模型需要满足的动态属性,然后采用模型检测工具对模型和动态属性的一致性进行验证。本文给出了基于模型检测方法建立ASIP体系结构模型的方法,针对流水线处理器和乱序处理器两种抽象处理器描述了具体的建模方法,分析了它们的动态属性,并对其进行了验证,证明了此方法的有效性。
(3)结合ASIP设计的层次化特点,提出了层次化和局部化的建模方法。采用抽象模型描述设计的整体特性,采用细化模型来刻画局部设计的细节,从而控制模型的规模,规避模型检测方法中的状态空间爆炸问题。
(4)提出了从HDPN描述到模型检测描述的转换规则。在此基础上,实现了一个支持结构检测和指令执行正确性检测的体系结构验证框架。
本文做出的贡献主要体现在:
(1)面向体系结构建模的需求,基于Petri网理论,提出了一种ASIP体系结构描述方法——HDPN。HDPN继承了Petri网的直观性特点,可以很好地刻画体系结构中模块间的互连关系;在此基础上加强了对设计中的存储单元、功能单元以及数据通路的刻画,通过对Petri网中的基本元素——库所、变迁和弧的扩展,分别对存储单元中存储的数据添加了类型定义,对功能部件添加了接口参数、执行条件和具体的行为描述,对数据通路定义了所传递的参数,提高了模型的描述能力。基于HDPN描述提出ASIP设计需要满足的静态属性,对设计的结构描述正确性和单条指令执行的正确性进行验证。
(2)将模型检测方法应用于ASIP体系结构验证中。提出了基于模型检测方法建立ASIP体系结构模型的方法,针对流水线处理器和乱序执行处理器描述了具体的建模方法,并给出了处理器正确执行所需满足的属性。在建模时采用分层和局部建模的方法有效规避模型检测方法中的状态空间爆炸问题,提高了模型检测方法的可用性。
(3)建立了HDPN描述和模型检测描述之间的转换规则,形成一个完整的ASIP体系结构验证框架。将ASIP体系结构的验证问题合理地划分为静态属性(结构正确性和单条指令执行的正确性问题)和动态属性(指令并行执行的正确性问题)两个子问题,分别通过基于Petri网的静态属性检测方法和基于模型检测的动态属性的检测方法对其描述和验证。
Application Specific Instructions Set Processors(ASIP) is a kind of special processor designed for a particular type of applications.With the continuous development of ASIP design,the complexity of the design is also increasing,and the verification efforts on the correctness of design are increasingly prominently accordingly.Due to the diversity of instructions' behaviors and the flexibility of logical structures,it is very difficult to build a general method to verify the correctness of the ASIP design automaticly.So far,there is not any effective theory and methodology on the automatic verification of ASIP design at architecture level.
On the problems mentioned above,the hierarchy characteristics of ASIP architecture design were analyzed deeply.A framework on the verification of ASIP architecture design,which is based on Petri Net and Model Checking theory and methodology,is presented in this thesis.The properties which an ASIP design needs to satisfy are divided into static properties and dynamic properties.Static properties are used to specify the requirements of structure and individual instructions' execution,while dynamic properties are used to specify the requirements of concurrent instructions.The main research works include:
(1) Description of the ASIP architecture based on Petri net.Hardware Design based-on Petri Net(HDPN),an extended Petri net,is used to describe the structural and behavioral characteristics of ASIP architecture.The static properties which an ASIP design should obey are also proposed.
(2) Verification of the dynamic properties based on Model Checking.Firstly, the model of ASIP architecture to be validated is constructed,and the dynamic properties which a processor should obey are extracted from customer-built requirements.Then model checker is used to check the consistency of the model and of the properties.The method is applied to a pipeline processor and an out-of-order processor to prove the availability.
(3) Modeling method based on the hierarchical and local characteristic of ASIP design.In order to efficiently verify the design,the models' scale should be restricted.Two kinds of models,global design and local models are constructed in this method.The global design,in which many details are hidden to reduce the scale of the model,is used to check the validity of the interaction between the components. While local models,in which concrete designs of each individual component are described,are used to verify detailed specifications.In this situation,the other parts of the design are treated as outer environment,and the interface parameters of the model are set as stochastic values in the possible range.
(4) The translation rules from HDPN based description to model checker based description.Based on the translation procedure,a verification framework which supports the validation on the correctness of structures and instructions' execution of an ASIP architecture design is constructed
The main contributions of this thesis are as follows:
(1) Aiming to the design of ASIP architecture,a novel extended Petri Net model named HDPN is introduced.It can describe target architecture in a succinct and precise way.In HDPN,tokens are endowed with concrete information according to the specific design,but not only a black dot in traditional Petri Net.Therefore the elements in the Places are added with types.And transitions,which are used to describe the function units,are appended with interface parameters,execution conditions and concrete action description.Arcs,which are used to describe data path,are also appended with parameters.To sum up,as a modeling tool,HDPN can sufficiently describe the structural information and individual instructions' execution of the ASIP architecture.The method based on HDPN,taking advantage of it,can efficiently verify the static properties accordingly.
(2) Model checking is applied to the verification of ASIP architecture. Modeling method based on hierarchical and local description is presented and used to abstract models from a pipeline processor and an out-of-order execution processor. These modeling methods are effective to avoid state space explosion.The dynamic properties used to check the correctness of a processor execution are also proposed.
(3) The translation rules from HDPN description to the input language of model checker-NuSMV are presented.Therefore,an integrated framework for ASIP architecture verification is built.The properties for the verification are divided into static properties and dynamic properties.They are checked through the static property checking method based on HDPN and dynamic property checking method based on model checking,separately.
引文
Alomary A.,Nakata T.,et al.(1993).An ASIP Instruction Set Optimization Algorithm with Functional Module Sharing Constraint[C].International Conference on Computer-Aided Design (ICCAD1993),Santa Clara,California,United States
Arons T.(2004).Verification of an Advanced MIPS-Type Out-of-Order Execution Algorithm[C].Computer Aided Verification (CAV2004),Springer-Verlag Berlin Heidelberg 2004.
Arons T.and Pnueli A.(1999).Verifying Tomasulo's Algorithm by Refinement[C].International Conference on VLSI Design 1999.
Binh N.N.,Imai M.,et al.(1996).A New HW/SW Partitioning Algorithm for Synthesizing the Highest Performance Pipelined ASIPs with Multiple Identical FUs[C].European Design Automation Conference (EURODAC1996),Geneva,Switzerland.
Barrett C,Dill D.L.,et al.(1996).Validity Checking for Combinations of Theories with Equality [C].International Conference on Formal Methods in Computer-Aided Design (FMCAD1996),Stanford,CA,USA,Springer-Verlag.
Bashford S.,Bieker U.,et al.(1994).The MIMOLA Language Version 4.1,University of Dortmund.
Benders L.P.M.and Stevens M.P.J.(1992).Petri Net Modelling in Embedded System Design[C].European Computer Conference (CompEuro1992).
Burch J.,Clarke E.M.,et al.(1990).Sequential Circuit Verification using Symbolic Model Checking[C],Design Automation Conference (DAC1990),Los Alamitos.
Burch J.and Dill D.(1994).Automatic Verification of Pipelined Microprocessor Control[C].Computer Aided Verification (CAV1994),Springer-Verlag.
Burch J.R.,Clarke E.M.,et al.(1991).Symbolic Model Checking with Partitioned Transition Relations[C].International Conference on Very Large Scale Integration (VLSI1991).
Burch J.R.,Clarke E.M.,et al.(1994).Symbolic Model Checking for Sequential Circuit Verification[J].IEEE Transactions on CAD of Integrated Circuits and Systems 13:401-424.
Burch J.R.,Clarke E.M.,et al.(1998).Symbolic Model Checking:1020 States and Beyond[J].Information and Computation 2:141-170.
Chattopadhyay A.,Sinha A.,et al.(2006).Integrated Verification Approach during ADL-Driven Processor Design[C].International Workshop on Rapid System Prototyping (RSP2006).
Choi H.,Park I.-C,et al.(1998).Synthesis of Application Specific Instructions for Embedded DSP Software[C].International Conference on Computer-Aided Design (ICCAD1998).Digest of Technical Papers.
Cimatti A.,Clarke E.,et al.(1999).NuSMV:A New Symbolic Model Verifier[C].Computer Aided Verification (CAV1999),Trento,Italy,Springer.
Cimatti A.,Clarke E.,et al.(2000).NuSMV:A New Symbolic Model Checker[J].International Journal on Software Tools for Technology Transfer (STTT2000)2(4).
Clarke E.M.,Emerson E.A.,et al.(1986).Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications[J].ACM Transactions on Programming Languages and Systems 8:244-263.
Clarke E.M.and Wing J.M.(1996).Formal Methods:State of the Art and Future Directions[J].ACM Computing Surveys 28(4):626-643.
Cleavel R.,Parrow J.,et al.(1993).The Concurrency Workbench:a Semantics-based Verification Tool for the Verification of Concurrent Systems[J].ACM Transactions on Programming Languages and Systems 5(1):36-72.
Cortes L.A.,Eles P.,et al.(2000).Verification of Embedded Systems Using a Petri Net Based Representation[C].International Symposium on System Synthesis (ISSS2000).
Cyrluk D.(1993).Microprocessor Verification in PVS:A Methodology and Simple Example,SRI Computer Science Laboratory.
Damm W.and Pnueli A.(1997).Verifying out-of-order executions[C].D.Probst (Ed.),CHARME'97,Chapman & Hall,London.
Fauth A.,Praet J.V.,et al.(1995).Describing Instruction Set Processors using nML[C].European Conference on Design and Test (ED&TC1995).
Gao Y.,Li X.,et al.(2008).Validation of ASIP Architecture Description[C].International Symposium on Embedded Computing (SEC2008),BEIJING,CHINA.
Garcez E.H.A.and Rosenstiel W.(1998).CVF-Coverification Framework[C].Brazilian Symposium on Integrated Circuit Design.
Gerth R.,Peled D.,et al.(1995).Simple on-the-fly Automatic Verification of Linear Temporal Logic[C].Protocol Specification Testing and Verification (PSTV1995),Warsaw.
Ghazal N.,Newton R.,et al.(2000).Retargetable Estimation Scheme for DSP Architecture Selection[C].Conference on Asia South Pacific Design Automation (ASP-DAC2000).
Gloria A.D.and Faraboschi P.(1990).An Evaluation System for Application Specific Architectures[C].Annual Workshop and Symposium on Microprogramming and Microarchitecture.Micro 23.
Godefroid P.(1997).VeriSoft:A Tool for the Automatic Analysis of Concurrent Reactive Software[C].Computer Aided Verification (CAV1997),Berlin:Springer-Verlag.
Gong J.,Gajski D.D.,et al.(1995).Performance Evaluation for Application-Specific Architectures[J].IEEE Transactions on VLSI Systems 3(4):483-490.
Gordon M.J.and EMelham T.(1993).Introduction to HOL:A Theorem Proving Environment for Higher-order Logic.Cambridge,UK,Cambridge University Press.
Gschwind M.(1999).Instruction Set Selection for ASIP Design[C].International Workshop on Hardware/Software Codesign (CODES 1999),Rome Italy.
Gu Z.and Shin K.G (2003).An Integrated Approach to Modeling and Analysis of Embedded Real-time Systems based on Timed Petri Nets[C],International Conference on Distributed Computing Systems (ICDCS2003).
Gupta T.V.K.,Sharma P.,et al.(2000).Processor Evaluation in an Embedded Systems Design Environment[C].International Conference on VLSI Design 2000
Gyllenhaal J.C.(1994).A Machine Description Language for Compilation[D]:[Master].Dept.of ECE,UIUC.
Hack M.(1976a).Decidability Questions for Petri Nets[D]:[Ph.D].Cambridge,MA,USA Massachusetts Institute of Technology
Hack M.(1976b).Petri Net Languages.Cambridge,Massachusetts Institute of Technology.
Hadjiyiannis G.,Hanono S.,et al.(1996).ISDL:An Instruction Set Description Language for Retargetability[C].Design Automation Conference (DAC1996).
Halambi A.,Grun P.,et al.(1999).EXPRESSION:A Language for Architecture Eexploration through Compiler/Simulator Retargetability[C].Design,Automation and Test in Europe (DATE1999).
Hanono S.and Devadas S.(1998).Instruction Selection,Resource Allocation,and Scheduling in the AVIV Retargetable Code Generator[C].Design Automation Conference (DAC1998).
Harris D.,Stokes D.,et al.(2000).Executing An RTOS On Simulated Hardware Using Co-Verification[C].Embedded Systems Conference (ESC2000).
Hatcher P.J.and Tuller J.W.(1988).Efficient Retargetable Compiler Code Generation[C].International Conference on Computer Languages 1998,Miami Beach,FL,USA.
Hennessy J.L.and Patterson D.A.(2007).Computer Architecture:A Quantitative Approach,Elsevier.
Holzmann G.J.(1991).Design and Validation of Computer Protocols.New Jersey,Prentice Hall.
Holzmann G.J.(1997).The Model Checker SPIN[J].IEEE Transactions on Software Engineering 23(5):279-295.
Hosabettu R.,Srivas M.,et al.(1999).Proof of Correctness of a Processor with Reorder Buffer using the Completion Functions Approach[C].Computer Aided Verification (CAV1999),Trento,Italy.
Huang I.-J.and Despain A,M.(1995).Synthesis of Application Specific Instruction Sets[J].IEEE Transactions on CAD of Integrated Circuits and Systems 14(6):663-675.
Intel.(2001).“Intel XScale Microarchitecture Programmers Reference.” Retrieved April,2009,from http://vvww.intel.com/design/intelxscale/273436.htm.
Jacobi C.(2002).Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving[C].Computer Aided Verification (CAV2002),LNCS 2404.
Jacobi C.and Kroening D.(2000).Proving the Correctness of a Complete Microprocessor[C].GI Jahrestagung 2000,Springer.
Jain M.K.,Balakrishnan M.,et al.(2001).ASIP Design Methodologies:Survey and Issues[C].International Conference on VLSI Design 2001 Bangalore,India.
Jensen K.(1983).High-level Petri nets:Applications and Theory of Petri net,Informatik Fachberichte:166-180.
Jensen K.(1992).Coloured Petri Nets.Berlin,Springer-Verlag.
Jhaia R.and McMillan K.L.(2001).Microarchitecture Verification by Compositional Model Checking[C].Computer Aided Verification (CAV2001),LNCS 2102.
Karlsson D.,Eles P.,et al.(2006).Formal Verification of Systemc Designs using a Petri-net based Representation[C].Design,Automation and Test in Europe (DATE2006),Munich,Germany
Kaufmann M.and Russinoff D.(2000).Verification of Pipeline Circuits.ACL2 Workshop 2000.Austin,Texas.
Kienhuis B.,Deprettere E.,et al.(1998).The Construction of a Retargetable Simulator for an Architecture TemplatefC].International Workshop on Hardware/Software Codesign (CODES/CASHE1998).
Kin J.,Lee C,et al.(1999).Power Efficient Mediaprocessors:Design Space Exploration[C].Design Automation Conference (DAC1999).
Klein R.(2003).Hardware/Software Co-Verification[C].Embedded Systems Conference (ESC2003).
Koo H.-M.and Mishra P.(2008).Specification-based Compaction of Directed Tests for Functional Validation of Pipelined Processors[C].International Workshop on Hardware/Software Codesign (CODES2008),Atlanta,Georgia,USA.
Koo H.-M.and Mishra P.(2009).Functional Test Generation using Design and Property Decomposition Techniques [J].ACM Transactions on Embedded Computing Systems.
Kreuzer W.,Gotschlich M.,et al.(1996).A Retargetable Optimizing Code Generator for Digital Signal Processors[C].International Symposium on Circuits and Systems (ISCAS1996).
Lahiri S.K.and Bryant R.E.(2003).Deductive Verification of Advanced Out-of-Order Microprocessors[C].Computer Aided Verification (CAV2003),Springer-Verlag Berlin Heidelberg 2003.
Lam W.K.(2005).Hardware Design Verification:Simulation and Formal Method-based Approaches.
Leupers R.and Marwedel P.(1996).Instruction Selection for Embedded DSPs with Complex InstructionsfC].European Design Automation Conference (EURODAC1996),Geneva,Switzerland.
Leupers R.and Marwedel P.(1997).Retargetable Generation of Code Selectors from HDL Processor Models[C].European Conference on Design and Test (ED&TC 1997).
Levitt J.and Olukotun K.(1996).A Scalable Formal Verification Methodology for Pipelined Microprocessors[C].Design Automation Conference (DAC1996),Las Vegas NV.
Levitt J.and Olukotun K.(1997).Verifying Correct pipeline Implementation for Microprocessors[C].International Conference on Computer-Aided Design (ICCAD 1997).
Liem C,May T.,et al.(1994).Instruction-Set Matching and Selection for DSP and ASIP Code GenerationfC].European Design Automation Conference (EURODAC1994).
LIN Y.-N.,LIN Y.-D.,et al.(2008).Modeling and Analysis of Core-centric Network Processors[J].ACM Transactions on Embedded Computing Systems,Article 41 7(4).
Loitz S.,Wedler M.,et al.(2008).Proving Functional Correctness of Weakly Programmable IPs-A Case Study with Formal Property Checking[C].Symposium on Application Specific Processors(SASP2008).
Lu L.,Li X.,et al.(2002).XM-ADL,an Extensible Markup Architecture Description Language[C].Annual IEEE International ASIC/SOC Conference 2002,New York,USA.
McLellan E.(1993).The Alpha AXP Architecture and 21064 processor[J].IEEE Micro.
McMillan K.L.(1992).Symbolic Model Checking:an Approach to the State Explosion Problem,Camegie-Melon University,Department of Computer Science.
McMillan K.L.(1993).Symbolic Model Checking.Boston,Massachusetts,Kluwer Academic Publishers.
Mcmillan K.L.(1998).Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking[C].Computer Aided Verification (CAV1998).
Mishra P.and Dutt N.(2005).Functional Coverage Driven Test Generation for Validation of Pipelined Processors[C].Design,Automation and Test in Europe (DATE2005),Munich,Germany.
Mishra P.and Dutt N.(2008).Specification-driven Directed Test Generation for Validation of Pipelined Processors[J].ACM Transactions on Design Automation of Electronic Systems 13(2):36.
Mishra P.,Dutt N.,et al.(2001).Architecture Description Language driven Validation of Processor,
Memory,and Co-processor Pipelines,California,Irvine:Dept.of Information and Computer Sience,UCI.
Mishra P.,Tomiyama H.,et al.(2002).Automatic Verification of In-Order Execution in Microprocessors with Fragmented Pipelines and Multicycle Functional Units[C].Design,Automation and Test in Europe (DATE2002),Paris,France.
Mishra P.,Tomiyama H.,et al.(2004).Automatic Modeling and Validation of Pipeline Specifications driven by an Architecture Description Language[J].ACM Transactions on Embedded Computing Systems:114-139.
Moona R.(2000).Processor Models for Retargetable Tools[C].International Workshop on Rapid System Prototyping (RSP 2000).
Murata T.(1989).Petri Nets:Analysis and Applications[C].Proc.IEEE.NuSMV.(2008).“NuSMV 2.4 User Manual.” Retrieved January,2008,from http://nusmv.irst.itc.it/.
Owre S.,Rushby J.M.,et al.(1994).A Tutorial on Using PVS for Hardware Verification[C].Conference on Theorem Provers in Circuit Design (TPCD1994),FZI Publication,Universif'at Karlsruhe.
Paruthiy V.,Mansouri N.,et al.(1998).Automatic Data Path Abstraction for Verification of Large Scale Designs[C].International Conference on Computer Design (ICCD1998).
Patterson D.A.and Hennessy J.L.(1998).Computer Organization & Design:The Hardware/Software Interface,Morgan Kaufmann Publishers,Inc.
Pees S.,Hoffmann A.,et al.(1999).LISA:Machine Description Language for Cycle-accurate Models of Programmable DSP ArchitecturesfC].Design Automation Conference (DAC1999),New Orleans.
Peng Z.and Kuchcinski K.(1994).Automated Transformation of Algorithms into Register-Transfer Level Implementations[J].IEEE Trans,on CAD 13(2).
Peterson J.(1981).Petri Net Theory and the Modeling of Systems,Englewood Cliffs,NJ:Prentice-Hall.
Pnueli A.(1984).In Transition from Global to Modular Temporal Reasoning about Programs.Logics and Models of Concurrent Systems,Springer-Verlag New York,Inc.13:123-144.
Pnueli A.and Arons T.(2003).TLPVS:A PVS-based LTL Verification System.Verification:Theory and Practice:598-625.
Praet J.V.,Lanneer D.,et al.(1996).A Graph based Processor Model for Retargetable Code Generation[C].European Conference on Design and Test (ED&TC1996).
Rajesh V.and Moona R.(1999).Processor Modeling for Hardware Software Codesign[C].International Conference on VLSI Design 1999
Ramchandani C.(1974).Analysis of Asynchronous Concurrent Systems by Timed Petri Nets,Massachusetts Institute of Technology Cambridge,MA,USA
Rashinkar P.,Paterson P.,et al.(2000).System-on-a-Chip Verification Methodology and Techniques,Kluwer Academic Publishers.
Ratzer A.V,Wells L.,et al.(2003).CPN Tools for editing,simulating,and analysing Coloured Petri Nets[C].International Conference on Application and Theory of Petri Nets (ICATPN2003).
Ray S.and Hunt W.A.(2004).Deductive Verification of Pipelined Machines Using First-order Quantification[C].Computer Aided Verification (CAV2004),Boston,MA.
Razouk R.R.(1988).The Use of Petri Nets for Modeling Pipelined Processors[C].Design Automation Conference (DAC1988),Anaheim,CA,USA.
Ribeiro O.R.,Fernandes J.M.,et al.(2005).Model Checking Embedded Systems with PROMELA[C].International Conference and Workshops on the Engineering of Computer-Based Systems (ECBS2005).
Saghir M.A.R.,Chow P.,et al.(1994).Application-Driven Design of DSP Architectures and Compilers[C].International Conference on Acoustics,Speech,and Signal Processing (ICASSP1994).
Sato J.,lmai M.,et al.(1991).An Integrated Design Environment for Application Specific Integrated Processor[C].International Conference on Computer Design(ICCD1991),Cambridge,MA,USA.
Sawada J.and Hunt W.A.(1997).Trace Table based Approach for Pipelined Microprocessor Verification[C].Computer Aided Verification(CAV1997),Haifa.
Sgroi M.,Lavagno L.,et al.(1999).Synthesis of Embedded Software Using Free-Choice Petri Nets[C].Design Automation Conference(DAC1999).
Shrivastava A.,Earlie E.,et al.(2005).PBExplore:A Framework for Compiler-in-the-Loop Exploration of Partial Bypassing in Embedded Processors[C].Design,Automation and Test in Europe(DATE2005).
Shu J.,Wilson T.C.,et al.(1996).Instruction-Set Matching and GA-based Selection for Embedded-Processor Code Generation[C].International Conference on Very Large Scale Integration(VLSI1996).
Skakkebaek J.U.,Jones R.B.,et al.(1998).Formal Verification of Out-of-order Execution using Incremental Flushing[C].Computer Aided Verification(CAV1998).
Stoy E.(1995).A Petri Net Based Unified Representation for Hardware/Software Co-Design[D]:[Dept.of Computer and Information Science,Link(o|¨)ping University,Link(o|¨)ping,Sweden.
Stoy E.and Peng Z.(1994).An Integrated Modelling Technique for Hardware/Software Systems[C].International Symposium on Circuits and Systems(ISCAS1994).
Suresh D.C.,Najjar W.A.,et al.(2003).Profiling Tools for Hardware/Software Partitioning of Embedded Applications[C].ACM SIGPLAN Conference on Language,Compiler,and Tool for Embedded Systems2003 San Diego,California,USA
Tahar S.and Kumar R.(1998).A Practical Methodology for the Formal Verification of RISC Processors[J].Formal Methods in System Design 13(2):159-225
Thiry O.and Claesen L.(1996).A Formal Verification Technique for Embedded Software[C].International Conference on Computer Design(ICCD1996),Austin,Texas,U.S.A.
Varea M.,Al-Hashimi B.M.,et al.(2002).Symbolic Model Checking of Dual Transition Petri Nets[C],International Workshop on Hardware/Software Codesign(CODES/CASHE2002),Colorado,USA.
Wasaki K.,Harai T.,et al.(2007).Controller Design and Verification for A Pipeline Image Processor based on An Extended Petri net[C].Euromicro Conference on Digital System Design Architectures,Methods and Tools(DSD2007).
Wilson T.,Grewal G.,et al.(1994).An Integrated Approach to Retargetable Code Generation[C].International Symposium on High-Level Synthesis 1994.
Winkelmann K.,Trylus H.-J.,et al.(2004).Cost-Efficient Block Verification for a UMTS Up-Link Chip-Rate Coprocessor[C].Design,Automation and Test in Europe(DATE2004),Paris,France.
Yuan C.(1998).Principle of Petri Net,Electronics Industry Press.
Zhu Q.,Shrivastava A.,et al.(2007).Functional and Timing Validation of Partially Bypassed Processors[C].Design,Automation and Test in Europe(DATE2007).
王志刚(2006).可重定向的专用指令集处理器(ASIP)仿真评估方法研究[D]:[博士].合肥,中国科学技术大学.
仲力(2007).ASIP体系结构描述、仿真和形式化验证方法研究[D]:[硕士].合肥,中国科学技术 大学.
朱资(2006).基于Petri网的ASIP体系结构形式化建模和验证[D]:[硕士].合肥,中国科学技术大学.
杜日富,骆佑祯,et al.(2006).使用派翠網驗證CPU内部結耩之流程[J].圣约翰学报第二十三期23:127-145.
林闯(1999).随机Petri网和系统性能评价,清华大学出版社.
刘士喜,方贤文,et al.(2005).基于Petri网的同步DRAM控制器的建模与分析[J].系统仿真学报17:204-206.
张晨曦,王志英,et al.(2000).计算机体系结构,高等教育出版社.
杨君(2006).专用指令集处理器(ASIP)体系结构设计研究[D]:[博士].合肥,中国科学技术大学.
蒋屹新,林闯,et al.(2004).基于Petri网的模型检测研究[J].软件学报15(9):1265-1276.
蒋昌俊(2002).Petri网的行为理论及其应用,高等教育出版社.
韩俊刚and杜慧敏(2001).数字硬件的形式化验证,北京大学出版社:64-140.
Arons T.(2004).Verification of an Advanced MIPS-Type Out-of-Order Execution Algorithm[C].Computer Aided Verification (CAV2004),Springer-Verlag Berlin Heidelberg 2004.
Arons T.and Pnueli A.(1999).Verifying Tomasulo's Algorithm by Refinement[C].International Conference on VLSI Design 1999.
Binh N.N.,Imai M.,et al.(1996).A New HW/SW Partitioning Algorithm for Synthesizing the Highest Performance Pipelined ASIPs with Multiple Identical FUs[C].European Design Automation Conference (EURODAC1996),Geneva,Switzerland.
Barrett C,Dill D.L.,et al.(1996).Validity Checking for Combinations of Theories with Equality [C].International Conference on Formal Methods in Computer-Aided Design (FMCAD1996),Stanford,CA,USA,Springer-Verlag.
Bashford S.,Bieker U.,et al.(1994).The MIMOLA Language Version 4.1,University of Dortmund.
Benders L.P.M.and Stevens M.P.J.(1992).Petri Net Modelling in Embedded System Design[C].European Computer Conference (CompEuro1992).
Burch J.,Clarke E.M.,et al.(1990).Sequential Circuit Verification using Symbolic Model Checking[C],Design Automation Conference (DAC1990),Los Alamitos.
Burch J.and Dill D.(1994).Automatic Verification of Pipelined Microprocessor Control[C].Computer Aided Verification (CAV1994),Springer-Verlag.
Burch J.R.,Clarke E.M.,et al.(1991).Symbolic Model Checking with Partitioned Transition Relations[C].International Conference on Very Large Scale Integration (VLSI1991).
Burch J.R.,Clarke E.M.,et al.(1994).Symbolic Model Checking for Sequential Circuit Verification[J].IEEE Transactions on CAD of Integrated Circuits and Systems 13:401-424.
Burch J.R.,Clarke E.M.,et al.(1998).Symbolic Model Checking:1020 States and Beyond[J].Information and Computation 2:141-170.
Chattopadhyay A.,Sinha A.,et al.(2006).Integrated Verification Approach during ADL-Driven Processor Design[C].International Workshop on Rapid System Prototyping (RSP2006).
Choi H.,Park I.-C,et al.(1998).Synthesis of Application Specific Instructions for Embedded DSP Software[C].International Conference on Computer-Aided Design (ICCAD1998).Digest of Technical Papers.
Cimatti A.,Clarke E.,et al.(1999).NuSMV:A New Symbolic Model Verifier[C].Computer Aided Verification (CAV1999),Trento,Italy,Springer.
Cimatti A.,Clarke E.,et al.(2000).NuSMV:A New Symbolic Model Checker[J].International Journal on Software Tools for Technology Transfer (STTT2000)2(4).
Clarke E.M.,Emerson E.A.,et al.(1986).Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications[J].ACM Transactions on Programming Languages and Systems 8:244-263.
Clarke E.M.and Wing J.M.(1996).Formal Methods:State of the Art and Future Directions[J].ACM Computing Surveys 28(4):626-643.
Cleavel R.,Parrow J.,et al.(1993).The Concurrency Workbench:a Semantics-based Verification Tool for the Verification of Concurrent Systems[J].ACM Transactions on Programming Languages and Systems 5(1):36-72.
Cortes L.A.,Eles P.,et al.(2000).Verification of Embedded Systems Using a Petri Net Based Representation[C].International Symposium on System Synthesis (ISSS2000).
Cyrluk D.(1993).Microprocessor Verification in PVS:A Methodology and Simple Example,SRI Computer Science Laboratory.
Damm W.and Pnueli A.(1997).Verifying out-of-order executions[C].D.Probst (Ed.),CHARME'97,Chapman & Hall,London.
Fauth A.,Praet J.V.,et al.(1995).Describing Instruction Set Processors using nML[C].European Conference on Design and Test (ED&TC1995).
Gao Y.,Li X.,et al.(2008).Validation of ASIP Architecture Description[C].International Symposium on Embedded Computing (SEC2008),BEIJING,CHINA.
Garcez E.H.A.and Rosenstiel W.(1998).CVF-Coverification Framework[C].Brazilian Symposium on Integrated Circuit Design.
Gerth R.,Peled D.,et al.(1995).Simple on-the-fly Automatic Verification of Linear Temporal Logic[C].Protocol Specification Testing and Verification (PSTV1995),Warsaw.
Ghazal N.,Newton R.,et al.(2000).Retargetable Estimation Scheme for DSP Architecture Selection[C].Conference on Asia South Pacific Design Automation (ASP-DAC2000).
Gloria A.D.and Faraboschi P.(1990).An Evaluation System for Application Specific Architectures[C].Annual Workshop and Symposium on Microprogramming and Microarchitecture.Micro 23.
Godefroid P.(1997).VeriSoft:A Tool for the Automatic Analysis of Concurrent Reactive Software[C].Computer Aided Verification (CAV1997),Berlin:Springer-Verlag.
Gong J.,Gajski D.D.,et al.(1995).Performance Evaluation for Application-Specific Architectures[J].IEEE Transactions on VLSI Systems 3(4):483-490.
Gordon M.J.and EMelham T.(1993).Introduction to HOL:A Theorem Proving Environment for Higher-order Logic.Cambridge,UK,Cambridge University Press.
Gschwind M.(1999).Instruction Set Selection for ASIP Design[C].International Workshop on Hardware/Software Codesign (CODES 1999),Rome Italy.
Gu Z.and Shin K.G (2003).An Integrated Approach to Modeling and Analysis of Embedded Real-time Systems based on Timed Petri Nets[C],International Conference on Distributed Computing Systems (ICDCS2003).
Gupta T.V.K.,Sharma P.,et al.(2000).Processor Evaluation in an Embedded Systems Design Environment[C].International Conference on VLSI Design 2000
Gyllenhaal J.C.(1994).A Machine Description Language for Compilation[D]:[Master].Dept.of ECE,UIUC.
Hack M.(1976a).Decidability Questions for Petri Nets[D]:[Ph.D].Cambridge,MA,USA Massachusetts Institute of Technology
Hack M.(1976b).Petri Net Languages.Cambridge,Massachusetts Institute of Technology.
Hadjiyiannis G.,Hanono S.,et al.(1996).ISDL:An Instruction Set Description Language for Retargetability[C].Design Automation Conference (DAC1996).
Halambi A.,Grun P.,et al.(1999).EXPRESSION:A Language for Architecture Eexploration through Compiler/Simulator Retargetability[C].Design,Automation and Test in Europe (DATE1999).
Hanono S.and Devadas S.(1998).Instruction Selection,Resource Allocation,and Scheduling in the AVIV Retargetable Code Generator[C].Design Automation Conference (DAC1998).
Harris D.,Stokes D.,et al.(2000).Executing An RTOS On Simulated Hardware Using Co-Verification[C].Embedded Systems Conference (ESC2000).
Hatcher P.J.and Tuller J.W.(1988).Efficient Retargetable Compiler Code Generation[C].International Conference on Computer Languages 1998,Miami Beach,FL,USA.
Hennessy J.L.and Patterson D.A.(2007).Computer Architecture:A Quantitative Approach,Elsevier.
Holzmann G.J.(1991).Design and Validation of Computer Protocols.New Jersey,Prentice Hall.
Holzmann G.J.(1997).The Model Checker SPIN[J].IEEE Transactions on Software Engineering 23(5):279-295.
Hosabettu R.,Srivas M.,et al.(1999).Proof of Correctness of a Processor with Reorder Buffer using the Completion Functions Approach[C].Computer Aided Verification (CAV1999),Trento,Italy.
Huang I.-J.and Despain A,M.(1995).Synthesis of Application Specific Instruction Sets[J].IEEE Transactions on CAD of Integrated Circuits and Systems 14(6):663-675.
Intel.(2001).“Intel XScale Microarchitecture Programmers Reference.” Retrieved April,2009,from http://vvww.intel.com/design/intelxscale/273436.htm.
Jacobi C.(2002).Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving[C].Computer Aided Verification (CAV2002),LNCS 2404.
Jacobi C.and Kroening D.(2000).Proving the Correctness of a Complete Microprocessor[C].GI Jahrestagung 2000,Springer.
Jain M.K.,Balakrishnan M.,et al.(2001).ASIP Design Methodologies:Survey and Issues[C].International Conference on VLSI Design 2001 Bangalore,India.
Jensen K.(1983).High-level Petri nets:Applications and Theory of Petri net,Informatik Fachberichte:166-180.
Jensen K.(1992).Coloured Petri Nets.Berlin,Springer-Verlag.
Jhaia R.and McMillan K.L.(2001).Microarchitecture Verification by Compositional Model Checking[C].Computer Aided Verification (CAV2001),LNCS 2102.
Karlsson D.,Eles P.,et al.(2006).Formal Verification of Systemc Designs using a Petri-net based Representation[C].Design,Automation and Test in Europe (DATE2006),Munich,Germany
Kaufmann M.and Russinoff D.(2000).Verification of Pipeline Circuits.ACL2 Workshop 2000.Austin,Texas.
Kienhuis B.,Deprettere E.,et al.(1998).The Construction of a Retargetable Simulator for an Architecture TemplatefC].International Workshop on Hardware/Software Codesign (CODES/CASHE1998).
Kin J.,Lee C,et al.(1999).Power Efficient Mediaprocessors:Design Space Exploration[C].Design Automation Conference (DAC1999).
Klein R.(2003).Hardware/Software Co-Verification[C].Embedded Systems Conference (ESC2003).
Koo H.-M.and Mishra P.(2008).Specification-based Compaction of Directed Tests for Functional Validation of Pipelined Processors[C].International Workshop on Hardware/Software Codesign (CODES2008),Atlanta,Georgia,USA.
Koo H.-M.and Mishra P.(2009).Functional Test Generation using Design and Property Decomposition Techniques [J].ACM Transactions on Embedded Computing Systems.
Kreuzer W.,Gotschlich M.,et al.(1996).A Retargetable Optimizing Code Generator for Digital Signal Processors[C].International Symposium on Circuits and Systems (ISCAS1996).
Lahiri S.K.and Bryant R.E.(2003).Deductive Verification of Advanced Out-of-Order Microprocessors[C].Computer Aided Verification (CAV2003),Springer-Verlag Berlin Heidelberg 2003.
Lam W.K.(2005).Hardware Design Verification:Simulation and Formal Method-based Approaches.
Leupers R.and Marwedel P.(1996).Instruction Selection for Embedded DSPs with Complex InstructionsfC].European Design Automation Conference (EURODAC1996),Geneva,Switzerland.
Leupers R.and Marwedel P.(1997).Retargetable Generation of Code Selectors from HDL Processor Models[C].European Conference on Design and Test (ED&TC 1997).
Levitt J.and Olukotun K.(1996).A Scalable Formal Verification Methodology for Pipelined Microprocessors[C].Design Automation Conference (DAC1996),Las Vegas NV.
Levitt J.and Olukotun K.(1997).Verifying Correct pipeline Implementation for Microprocessors[C].International Conference on Computer-Aided Design (ICCAD 1997).
Liem C,May T.,et al.(1994).Instruction-Set Matching and Selection for DSP and ASIP Code GenerationfC].European Design Automation Conference (EURODAC1994).
LIN Y.-N.,LIN Y.-D.,et al.(2008).Modeling and Analysis of Core-centric Network Processors[J].ACM Transactions on Embedded Computing Systems,Article 41 7(4).
Loitz S.,Wedler M.,et al.(2008).Proving Functional Correctness of Weakly Programmable IPs-A Case Study with Formal Property Checking[C].Symposium on Application Specific Processors(SASP2008).
Lu L.,Li X.,et al.(2002).XM-ADL,an Extensible Markup Architecture Description Language[C].Annual IEEE International ASIC/SOC Conference 2002,New York,USA.
McLellan E.(1993).The Alpha AXP Architecture and 21064 processor[J].IEEE Micro.
McMillan K.L.(1992).Symbolic Model Checking:an Approach to the State Explosion Problem,Camegie-Melon University,Department of Computer Science.
McMillan K.L.(1993).Symbolic Model Checking.Boston,Massachusetts,Kluwer Academic Publishers.
Mcmillan K.L.(1998).Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking[C].Computer Aided Verification (CAV1998).
Mishra P.and Dutt N.(2005).Functional Coverage Driven Test Generation for Validation of Pipelined Processors[C].Design,Automation and Test in Europe (DATE2005),Munich,Germany.
Mishra P.and Dutt N.(2008).Specification-driven Directed Test Generation for Validation of Pipelined Processors[J].ACM Transactions on Design Automation of Electronic Systems 13(2):36.
Mishra P.,Dutt N.,et al.(2001).Architecture Description Language driven Validation of Processor,
Memory,and Co-processor Pipelines,California,Irvine:Dept.of Information and Computer Sience,UCI.
Mishra P.,Tomiyama H.,et al.(2002).Automatic Verification of In-Order Execution in Microprocessors with Fragmented Pipelines and Multicycle Functional Units[C].Design,Automation and Test in Europe (DATE2002),Paris,France.
Mishra P.,Tomiyama H.,et al.(2004).Automatic Modeling and Validation of Pipeline Specifications driven by an Architecture Description Language[J].ACM Transactions on Embedded Computing Systems:114-139.
Moona R.(2000).Processor Models for Retargetable Tools[C].International Workshop on Rapid System Prototyping (RSP 2000).
Murata T.(1989).Petri Nets:Analysis and Applications[C].Proc.IEEE.NuSMV.(2008).“NuSMV 2.4 User Manual.” Retrieved January,2008,from http://nusmv.irst.itc.it/.
Owre S.,Rushby J.M.,et al.(1994).A Tutorial on Using PVS for Hardware Verification[C].Conference on Theorem Provers in Circuit Design (TPCD1994),FZI Publication,Universif'at Karlsruhe.
Paruthiy V.,Mansouri N.,et al.(1998).Automatic Data Path Abstraction for Verification of Large Scale Designs[C].International Conference on Computer Design (ICCD1998).
Patterson D.A.and Hennessy J.L.(1998).Computer Organization & Design:The Hardware/Software Interface,Morgan Kaufmann Publishers,Inc.
Pees S.,Hoffmann A.,et al.(1999).LISA:Machine Description Language for Cycle-accurate Models of Programmable DSP ArchitecturesfC].Design Automation Conference (DAC1999),New Orleans.
Peng Z.and Kuchcinski K.(1994).Automated Transformation of Algorithms into Register-Transfer Level Implementations[J].IEEE Trans,on CAD 13(2).
Peterson J.(1981).Petri Net Theory and the Modeling of Systems,Englewood Cliffs,NJ:Prentice-Hall.
Pnueli A.(1984).In Transition from Global to Modular Temporal Reasoning about Programs.Logics and Models of Concurrent Systems,Springer-Verlag New York,Inc.13:123-144.
Pnueli A.and Arons T.(2003).TLPVS:A PVS-based LTL Verification System.Verification:Theory and Practice:598-625.
Praet J.V.,Lanneer D.,et al.(1996).A Graph based Processor Model for Retargetable Code Generation[C].European Conference on Design and Test (ED&TC1996).
Rajesh V.and Moona R.(1999).Processor Modeling for Hardware Software Codesign[C].International Conference on VLSI Design 1999
Ramchandani C.(1974).Analysis of Asynchronous Concurrent Systems by Timed Petri Nets,Massachusetts Institute of Technology Cambridge,MA,USA
Rashinkar P.,Paterson P.,et al.(2000).System-on-a-Chip Verification Methodology and Techniques,Kluwer Academic Publishers.
Ratzer A.V,Wells L.,et al.(2003).CPN Tools for editing,simulating,and analysing Coloured Petri Nets[C].International Conference on Application and Theory of Petri Nets (ICATPN2003).
Ray S.and Hunt W.A.(2004).Deductive Verification of Pipelined Machines Using First-order Quantification[C].Computer Aided Verification (CAV2004),Boston,MA.
Razouk R.R.(1988).The Use of Petri Nets for Modeling Pipelined Processors[C].Design Automation Conference (DAC1988),Anaheim,CA,USA.
Ribeiro O.R.,Fernandes J.M.,et al.(2005).Model Checking Embedded Systems with PROMELA[C].International Conference and Workshops on the Engineering of Computer-Based Systems (ECBS2005).
Saghir M.A.R.,Chow P.,et al.(1994).Application-Driven Design of DSP Architectures and Compilers[C].International Conference on Acoustics,Speech,and Signal Processing (ICASSP1994).
Sato J.,lmai M.,et al.(1991).An Integrated Design Environment for Application Specific Integrated Processor[C].International Conference on Computer Design(ICCD1991),Cambridge,MA,USA.
Sawada J.and Hunt W.A.(1997).Trace Table based Approach for Pipelined Microprocessor Verification[C].Computer Aided Verification(CAV1997),Haifa.
Sgroi M.,Lavagno L.,et al.(1999).Synthesis of Embedded Software Using Free-Choice Petri Nets[C].Design Automation Conference(DAC1999).
Shrivastava A.,Earlie E.,et al.(2005).PBExplore:A Framework for Compiler-in-the-Loop Exploration of Partial Bypassing in Embedded Processors[C].Design,Automation and Test in Europe(DATE2005).
Shu J.,Wilson T.C.,et al.(1996).Instruction-Set Matching and GA-based Selection for Embedded-Processor Code Generation[C].International Conference on Very Large Scale Integration(VLSI1996).
Skakkebaek J.U.,Jones R.B.,et al.(1998).Formal Verification of Out-of-order Execution using Incremental Flushing[C].Computer Aided Verification(CAV1998).
Stoy E.(1995).A Petri Net Based Unified Representation for Hardware/Software Co-Design[D]:[Dept.of Computer and Information Science,Link(o|¨)ping University,Link(o|¨)ping,Sweden.
Stoy E.and Peng Z.(1994).An Integrated Modelling Technique for Hardware/Software Systems[C].International Symposium on Circuits and Systems(ISCAS1994).
Suresh D.C.,Najjar W.A.,et al.(2003).Profiling Tools for Hardware/Software Partitioning of Embedded Applications[C].ACM SIGPLAN Conference on Language,Compiler,and Tool for Embedded Systems2003 San Diego,California,USA
Tahar S.and Kumar R.(1998).A Practical Methodology for the Formal Verification of RISC Processors[J].Formal Methods in System Design 13(2):159-225
Thiry O.and Claesen L.(1996).A Formal Verification Technique for Embedded Software[C].International Conference on Computer Design(ICCD1996),Austin,Texas,U.S.A.
Varea M.,Al-Hashimi B.M.,et al.(2002).Symbolic Model Checking of Dual Transition Petri Nets[C],International Workshop on Hardware/Software Codesign(CODES/CASHE2002),Colorado,USA.
Wasaki K.,Harai T.,et al.(2007).Controller Design and Verification for A Pipeline Image Processor based on An Extended Petri net[C].Euromicro Conference on Digital System Design Architectures,Methods and Tools(DSD2007).
Wilson T.,Grewal G.,et al.(1994).An Integrated Approach to Retargetable Code Generation[C].International Symposium on High-Level Synthesis 1994.
Winkelmann K.,Trylus H.-J.,et al.(2004).Cost-Efficient Block Verification for a UMTS Up-Link Chip-Rate Coprocessor[C].Design,Automation and Test in Europe(DATE2004),Paris,France.
Yuan C.(1998).Principle of Petri Net,Electronics Industry Press.
Zhu Q.,Shrivastava A.,et al.(2007).Functional and Timing Validation of Partially Bypassed Processors[C].Design,Automation and Test in Europe(DATE2007).
王志刚(2006).可重定向的专用指令集处理器(ASIP)仿真评估方法研究[D]:[博士].合肥,中国科学技术大学.
仲力(2007).ASIP体系结构描述、仿真和形式化验证方法研究[D]:[硕士].合肥,中国科学技术 大学.
朱资(2006).基于Petri网的ASIP体系结构形式化建模和验证[D]:[硕士].合肥,中国科学技术大学.
杜日富,骆佑祯,et al.(2006).使用派翠網驗證CPU内部結耩之流程[J].圣约翰学报第二十三期23:127-145.
林闯(1999).随机Petri网和系统性能评价,清华大学出版社.
刘士喜,方贤文,et al.(2005).基于Petri网的同步DRAM控制器的建模与分析[J].系统仿真学报17:204-206.
张晨曦,王志英,et al.(2000).计算机体系结构,高等教育出版社.
杨君(2006).专用指令集处理器(ASIP)体系结构设计研究[D]:[博士].合肥,中国科学技术大学.
蒋屹新,林闯,et al.(2004).基于Petri网的模型检测研究[J].软件学报15(9):1265-1276.
蒋昌俊(2002).Petri网的行为理论及其应用,高等教育出版社.
韩俊刚and杜慧敏(2001).数字硬件的形式化验证,北京大学出版社:64-140.