Karmel Electronic Design Services                 

Karmel Electronic Design Services

ph: +972.54.320.9244

contact@karmeleds.com

  • Home
  • Charter
  • Management
  • ServicesClick to open the Services menu
    • Methodology and Deployment
    • Formal Verification
    • Assertion Libraries
  • Customers
  • Documents
  • Contact Us

Formal Verification Methodology and Deployment

The goal of Karmel EDS methodology and deployment services is to help your team get the most out of formal verification.  We have identified four stages of formal verification deployment.

Stage 0:  No deployment on real projects.  The team is interested in taking first steps towards adoption. 

Stage 1:  Limited local deployment with ambiguous results.  The team is interested in analyzing past experience and moving forward with formal. 

Stage 2: Limited deployment with good results.  The team is interested in extending deployment and in making formal an integral part of the design and verification flow.

Stage 3:  Formal verification is part of the flow.  The team may benefit from an external audit with the aim of learning about better ways of doing things and new areas to deploy formal at.   

Regardless of the stage your team is at, Karmel EDS has the knowledge and the experience to assist your team in moving forward with formal verification. We will make sure that your progress is not stalled due to uncertainties or wrong technical decisions.

We offer consultation and services in the following areas:

1.    Evaluation plan: Is formal verification suitable for your design flow and the type of logic you need to verify?  Which tools are best suited for the jobs you need done?  We will help you go through an evaluation process that will yield solid answers to these and other questions you might have. 

2.    Adoption plan:  You have decided to try formal on a real project.  Karmel EDS will help you plan and execute on this initial deployment.  We’ll decide together on the blocks to target and on the scope of the project, the people that should be involved and the methodology.  We’ll work with you through all the technical stages of the project.  

3.    Verification planning:  Like in other verification methodologies, verification plan is extremely important for formal verification.  This is where the blocks to target, the properties to be verified, the environmental assumptions to be used, the coverage events expected to be seen, the design modes that need to be tested, the initialization sequences that are required and the verification strategy to be used are all discussed and specified.  This is also where full proofs versus bounded proofs are discussed and where implications on your simulation environments are determined.

4.    Specification techniques:  Karmel EDS will work with you to ensure that your properties are correct, general, efficient and reusable.  Whether they are control logic or data path oriented, we will help you write properties that express exactly what you intend them to.  

5.    Handling size problems:  Not all assertions converge (pass or fail) in all formal verification projects.  We will guide you through a variety of approaches around this limitation. One class of approaches aim to assist the tools in converging on tough properties (e.g. abstractions or assume-guarantee).  Another class teaches how to extract significant verification value even from properties that do not converge. 

6.    Combining formal and simulation:  Formal verification should not be an isolated activity but an integral part of the design and verification flow.  In particular, the verification team needs to decide what is best verified by formal and what should be verified by simulation, eliminating unnecessary duplication of efforts whenever is possible and leveraging both activities towards common goals (e.g. quality and productivity of the verification process). 

7.    Formal verification audit:  There are multiple areas in the design and verification flow where formal can bring significant value.  Beginning at the architectural level and the first stages of RTL coding, through the verification process, and ending at post silicon debug.  Our audit services will examine with you your design and verification flow and propose ways to improve and/or extend your application of formal methodologies and tools. 

    Karmel Electronic Design Services

    Contact Us

    Copyright 2011 Karmel Electronic Design Services. All rights reserved.

    Karmel Electronic Design Services

    ph: +972.54.320.9244

    contact@karmeleds.com