jasper user manual

所需积分/C币:20 2018-03-13 09:34:18 7.24MB PDF
收藏 收藏

jasper user manual,可以用于静态验证assertion的覆盖是否完备.
Contents Preface 8 Who should read this book What's New in 2014.03 9 How This book Is organized 5 Related documentation ..52 Conventions Used in Jasper documents ...,,,,..53 Chapter 1 Jasper Gold Apps Overview n,,,,56 Jasper Gold Apps- Common Attributes ..,57 Generic GUI Components .57 Search Sort and filter Features 62 Starting a New Jasper Gold Apps Database 4 Loading an Existing Database ..65 Formal Property Verification App 66 Formal Property Verification App Flow 66 Formal Property Verification App GUI Orientation 66 X-Propagation Verification App 73 X-Propagation Verification App Flow 73 X-Propagation Verification App GUI Orientation ..,74 Connectivity Verification App .,80 Connectivity Verification App Flow ...80 Connectivity Verification App GUI Orientation 81 Architectural Modeling app 84 Architectural Modeling App Flow 85 Architectural Modeling App GUI Orientation 85 CSR Verification App 91 CSR Verification App Flow .....,.92 CSR Verification App GUI Orientation ,,,,,,,,.93 RTL Development App RTL Development App Phases .98 RTL Development App GUI Orientation 9 EXecutable Specification App 翻 104 Behavioral Property Synthesis App 109 Behavioral Property Synthesis App Flow 110 Behavioral Property Synthesis App GUl Orientation 110 Structural Property Synthesis App 117 Structural Property Synthesis App GUI Orientation 118 LoW Power Verification App .124 LoW Power Verification App Flow 124 Low Power Verification App GUI Orientation ......... 125 Sequential Equivalence Checking App 129 SEC App Flow 130 SEC App GUI Orientation 131 a 2014 Jasper Design Automation Confidentia Jasper Gold Apps User,'s Guide 2014.03 3 Security Path Verification App 135 SPV App Flow .,,,,,,.135 SPV App GUI Orientation .136 Coverage App ...,.139 Coverage App Flow 140 Coverage App GUI Orientation .14 Chapter 2: Specifying the Environment n,,,148 Analyzing the design .,,,,,149 Elaborating the design 152 Specifying the Global Clock 154 Specifying the Global Reset 155 Specifying Proof Settings 157 Specifying Basic Engine Settings 158 Specifying Advanced Engine Settings 16 Capturing and Reusing the Setup Configurati 165 Creating Multiple Sessions .,,,,,,166 Launching a New Session .167 Launching a New Session with an Elaborated Design 167 Saving and restoring your Work 168 Saving the Database .169 Saving an elaborated Design 169 Restoring the Database 170 Restoring an elaborated design ....170 Chapter 3: ProofGrid Manager 171 Proof Grid Manager Use modes 172 Using Proof Grid with Server Farms 172 Leveraging Engine L with Proof Grid Manager 172 Proof Grid Manager GUI Orientation 173 Working with the Engine Graph 177 Working with the Engine List .178 Chapter 4 Visualize n,,,,,181 Visualize window- GUl Orientation .182 Usability Tips 182 GUI Components .....183 Window docking features .193 Copy/Paste Operations 193 Visualize Work flows 194 Property visualization 195 RTL Exploration with Waveforms 197 Design-Space Tunneling ,,,,,,,,.,198 State-Space Tunneling 翻 199 a 2014 Jasper Design Automation Confidentia Jasper Gold Apps User's Guide 2014.03 4 Configuring a Visualize Waveform 202 Building Your Waveform ......203 Adding a Waveform Configuration ..205 Using Freeze When Building a Waveform .208 Local Task Context Operations for Waveforms .209 Reset Analysis 210 Chapter 5: Source browser ,213 Accessing the Stand-Alone Source Browser.......... 214 Source browser -GUl Orientation 214 GUI Components 214 Copy/Paste Operations 218 Chapter 6 Design Exploration Tools n,220 Before you begin 221 Jasper Gold Design Information Design Information GUl Orientation .,222 Working with the design Information Metrics Pane 223 Leveraging Design Information Metrics 225 Jasper Gold Design Space Coverage .226 Design Space Coverage Context .....,..227 Design Space Coverage Flow 227 Design Space Coverage GUI Orientation ..228 Jasper gold Complexity Manager 232 Complexity Manager GUl Orientation 233 Working with the Complexity Manager Tree Pane 237 Working with the complexity Manager-Information Pane 238 Appendix A: GUI Settings..,.,.. ,,,,,,,,,,,240 Setting Preferences 241 Resolving Unavailable Fonts Issues ..242 Window geometry Settings................. 243 Color Depth Configuration 243 Changing Default Configuration Settings .244 Changing Message Pane Preferences 244 Changing Font Color for Sourced Commands .246 Changing Property Table Filtering Behavior ..246 Changing GUI Background and Foreground Colors ..246 Copying Text in VNC Sessions .....247 Appendix B: Verification Status Indicators 249 Proof status Indicators .....,,250 o 2014 Jasper Design Automation Confidentia Jasper Gold Apps User,'s Guide 2014.03 5 Assumption Scoreboarding Indicators 253 Filtering and sorting 254 Appendix C: Why and relevant Loads 256 Why and relevant Loads gul basics ...257 Wh 257 Relevant loads 258 Why and relevant loads limitations 258 PSL and svA Support .258 Relevant Loads in Multiple cycles .....259 High Impedance() Assignments ....259 Appendix D: Connectivity Verification App Table Format. 260 Input Forn ○ tional Attributes 273 Appendix E: Architectural Modeling App Formats .... 276 Architectural Modeling app table Format .277 Murphi Program Support ..283 Accessing Murphi Language Support 283 Known limitations ...284 Appendix F: CSR Verification App Supporting Details... 285 Input 286 Instance Interface .286 Worksheet Format .......290 Access Types 296 Address Aliasing 296 Locking Support 297 Direct write and direct read si 298 Latencies Support 30 Modified write∨a|ue 303 Write value constraint 304 Bus Read Check and Bus Write Check for Different Access Type Semantics 306 Generating assumptions and Assertions 309 M asks 309 Masks Specified at the CSR Level .310 Simultaneous read /write 310 Register Maps 311 Secure and non -secure transactions .312 a 2014 Jasper Design Automation Confidentia Jasper Gold Apps User,'s Guide 2014.03 6 Remap States for JDA: SECURE and JDA: NON SECURE 312 Remap states for JDA: EXPRESSION 312 Address blocks 314 Reset signals 314 Windowed csrs 314 Appendix G: Jasper Property Macros for the BPS App 316 jasper_ stuck at(signal, values 318 jasper bits stuck at(signal, mask, values) ..319 jasper_ reachable_ states(signal, values 319 jasper unreachable states(signal, values) 320 jasper_ reachable transitions (signal, transitions 320 jasper_unreachable_transitions(signal, transitions 321 jasper reachable multi transitions(signal, multi transitions) 321 [jasper deadlock (signal, values) .322 jasper_ livelock(signal, values) ...322 jasper_ wraparound(signal, [before], [after]) ....,,323 jasper_overflow (signal, [before], [after]) .....323 jasper_ underflow (signal, [before], [afterD 324 jasper handshake ([-]req, [-lack, min, max, protocol type, parameter)325 jasper_past([-]signal, range) 326 jasper increment(signal) ........326 jasper decrement(signal) ..,,,327 jasper forbidden([-]signal1, [- signal2 [-]signal) ..327 jasper_ equal(signal_1,.[-]signal_n 328 Appendix H: Persistent Waivers with the SPS App..,. 329 Waiver Signatures and Examples Exporting Waivers .331 Importing Waivers .,,,,,.331 Tutorial 333 Appendix I: BPS App Progress Report 334 Using Progress Methodology in Verification Closure 335 Working with the BPS App Progress Report 335 Accessing the Progress Report ...335 eading the Progress Report 336 Exporting the Progress Report 337 Ensuring Database Compatibility 338 Appendix J Troubleshooting for External Applications . 340 a 2014 Jasper Design Automation Confidentia Jasper Gold Apps User,'s Guide 2014.03 7 Preface This manual is an introduction to Jasper Gold@ Apps, which provides verification solutions through a collection of apps, including Formal Property verification App, RtL Development App, Executable Specification App, X-Propagation Verification App Connectivity Verification App, and Architectural Modeling App. This preface includes the following sections: Who Should Read this book on page 9 What's New in 2014.03 on page 9 How This Book Is Organized on page 51 Related Documentation on page 52 Conventions Used in Jasper Documents on page 53 Jasper Design Automation, Inc. prohibits the use of our software in a way that does not comply with our written guidelines and documentation o 2014 Jasper Design Automation Confidential Who should read this book Who should read this book This user guide is intended for Soc design and verification engineers, including architectural model developers, designers, and verification engineers. Jasper Gold Apps supports a wide variety of verification needs with easy-to-access apps available from a common console What's New in 2014.03 The following list provides the highlights for this release, which includes the production- level release of the Coverage App and the sequential equivalence Checking App this release also includes the IPK upgrade with enhanced debugging, tighter integration with Jasper Gold Apps, and streamlined analysis and extraction. In addition, this release features use flow enhancements for the Low Power Verification App that emphasize the value of leveraging power-aware designs to reach your verification goals. Additional details are available in Table 1 and in the Incremental Training presentation, which is availableonFormalExpert(jasper-da.com/fe) NOTE: Jasper products no longer support Solaris Operating System Refer to table 1 for details about new and enhanced features and references to supporting documentation. Refer to the release notes in your build(doc directory )and on Formal expert for information about fixes for reported issues a Intelligent Proof Kit(IPK) Upgrade on page 11 Behavioral Property Synthesis(BPS) App on page 12 Connectivity verification on page 14 Coverage App on page 15 CSR Verification App on page 20 Low Power Verification App on page 24 Security Path Verification(SPV) App on page 27 Sequential Equivalence Checking App on page 28 X-Propagation Verification on page 31 Design Synthesis on page 33 Proofs and traces on page 36 User Interface on page 38 ■ Visualize on page40 o 2014 Jasper Design Automation Confidential Jasper Gold Apps User's Guide 2014.03 9 What s new in 2014.03 ■|P- XACT on page45 Miscellaneous on page 47 a 2014 Jasper Design Automation Confidential Jasper Gold Apps User's Guide 2014.03 10

试读 127P jasper user manual
立即下载 低至0.43元/次 身份认证VIP会员低至7折
关注 私信
jasper user manual 20积分/C币 立即下载
jasper user manual第1页
jasper user manual第2页
jasper user manual第3页
jasper user manual第4页
jasper user manual第5页
jasper user manual第6页
jasper user manual第7页
jasper user manual第8页
jasper user manual第9页
jasper user manual第10页
jasper user manual第11页
jasper user manual第12页
jasper user manual第13页
jasper user manual第14页
jasper user manual第15页
jasper user manual第16页
jasper user manual第17页
jasper user manual第18页
jasper user manual第19页
jasper user manual第20页

试读结束, 可继续阅读

20积分/C币 立即下载