Abstract: Functional Verification is the most time consuming activity in the chip design cycle - the common figure is 70%. With systems on a single chip reaching 10 billion transistors, the challenge of manufacturing a fully functional component becomes bigger.  Are the tools that we use today, good enough for the present verification challenges?  Are they being used effectively? What are ABV (Assertion-Based Verification), CDV (Coverage Driven Verification) SFV (Semi Formal Verification) and many other verification related TLAs (Three Letter Abbreviations)? What are the key areas that will lead to more reliable and more effective verification? In this tutorial we will present the functional verification fundamentals (for simulation-based and for formal), discuss present verification methodologies (advantages and pitfalls) and will address the above questions.

Bio: Yuval Caspi received a B.A. Cum laude in Computer Science from the Technion in 1987, M.Sc and PhD in Computer Science from the University of Texas at Dallas in 1989 and 1992 respectively.
He joined Intel Haifa in 1992, were he was first exposed to the area of Hardware functional verification. These years marked a turning-point in verification methodologies for Intel, after the Floating Point Divide (FDIV) bug in the Pentium. Intel Haifa laid the foundations, throughout the company, for Coverage Driven Verification (CDV) and Formal Verification, methodologies that have become wide spread only in the last few years. Dr. Caspi was also one of the first adopters of the Specman tool back in 1996, helping to extend its features' set, too. For the last decade, he is working as a consultant and a freelancer for various companies and many projects. Dr. Caspi taught courses on simulation-based verification at the Technion and on formal verification at the Open University.

Abstract: This tutorial will provide an overview of SystemVerilog Assertions (SVA) and explain the basics of formal verification. The following topics will be covered:

• Linear time formal verification model
• Assertions, assumptions and cover statements
• Sequences and properties
• Sequence methods
• Safety and liveness
• Clocks and resets
• Strong and weak operators
• Checkers
• Free and rigid variables
• Local variables
• Recursive properties
• Efficiency tips
• Potential SVA future directions and challenge

Bio: Dmitry Korchemny is a senior staff engineer at Intel working on functional verification tool development. He received his M.Sc. from Moscow Institute of Radio-engineering Electronics and Automation. Dmitry joined Intel in 1993. Dmitry is actively involved in the standardization of SystemVerilog Assertions. He is a chair of the Assertions Committee of IEEE P1800 SystemVerilog Working Group.

Abstract: Interconnect verification presents verification teams with many challenges, and with the introduction of cache coherent interconnects, these challenges have dramatically intensified. SoCs today are built from many IP blocks and support multiple protocols (some of which may not be standard). The ability to track data flows, ensure data integrity and cache coherency in the system becomes one of the critical verification tasks that needs to be addressed. Going beyond functional verification, verification teams need to ensure that the performance requirements defined by system architects, like minimum latency and guaranteed bandwidth, are met.

Cadence Interconnect Validator verifies the interconnect fabrics that connect IP blocks and subsystems within an SoC. Whereas a principal aim of verification IP (VIP) is to verify that IP blocks follow a given communication protocol, Interconnect Validator verifies the correctness and completeness of data traffic across multiple ports and various protocols, collecting the metrics required to analyze your performance results. Because it automates a difficult and time-consuming task, Interconnect Validator greatly increases verification productivity at all integration levels, from block to subsystem to SoC. During this session we will share the most up-to-date experience from customers designing and verifying challenges and the best practices solution to address these challenges.

Bio: TBD

Abstract: The tutorial will survey key technologies in modern SAT and CSP solving, with an emphasis on producing minimal resolution proofs of unsatisfiability. Small proofs (minimal or not) play a crucial role in a number of applications in formal verification and Mathematical programming. In several of these the objective is to minimize the number of 'high-level' constraints (rather than the number of CNF clauses) that constitute a proof. The tutorial will survey these applications and describe how machine-checkable proofs can also be generated by a CSP solver via a representation called 'signed clauses'.

Bio: Prof. Ofer Strichman is active in the formal verification and SAT communities for 15 years. He has published over 80 peer-reviewed articles, and two books about decision procedures for first-order theories.

Abstract: One of the main challenges of a System Engineer is the Verification and Validation (V&V) process of large systems. On the one hand, these systems are becoming more complex, and on the other hand they are required to follow shorter development schedules. This presentation deals with harnessing the System Simulation as a tool to conquer this challenge. This process allows for a more efficient and comprehensive V&V process and shorter integration times.

Bio: Rachel Kenigsbuch finished her PhD in Mechanical Engineering at the Technion, Haifa in the year 2000. From that time she has been working in Rafael's Missiles Division.Rachel has worked in flight algorithms' development and accompanied the Systems' Engineering of many projects. In the last three years, Rachel leads the group in charge of development of System Simulations in Rafael's Missiles Division.