• Video: Verifying Datapath for an AMD Processor, Ankit Saxena, Oski

  • Video:Formal Verification for Networking Blocks, Vigyan Singhal, Oski

  • Video: DAC 2015 Verification Academy - Starting Formal Right from Formal Test Planning

  • Video: How to Know When a Formal Testbench is Complete

    Decoding Formal Video Tutorial Series: How to Know When a Formal Testbench is Complete This is an important problem because if you have decided to replace simulation with formal verification on a block you are working on, you want to know when to sign off with the work you have done. Three factors determine whether or not you are done with your formal testbench: constraints, checkers, complexity.
  • Video: How to Achieve Early Formal Convergence with Oski Abstraction Models

    Decoding Formal Video Tutorial Series: How to Achieve Early Formal Convergence with Abstraction Models
    The state space for formal is huge. If you have a design with 300 flops, that is already more states than there are atoms in the universe. So the state space is growing exponentially. Formal tools are limited by design size and where the proofs stop converging. Abstraction models can transform the search space for a formal verification run, and bring states which are distant close to the search state, allowing the proofs to converge much faster.
  • Video: How to Formally Verify - and Reuse - Highly Configurable IP Designs

    Decoding Formal Video Tutorial Series: How to Formally Verify and Reuse Highly Configurable IP
    Many designs these days support all sorts of IPs, and we want to verify these designs. However with tight schedules, we don't have the luxury of building from scratch, so the best thing to do is re-use IPs from 3rd parties or internal designs. We are still responsible for IP from 3rd parties. The designs are very configurable and the IPs themselves are highly configurable. The problem is that there are billions of different configurations. The beauty of formal verification is that you can try all of these different configurations together by making them a symbolic constant. Verifying IP especially highly configurable IP becomes extremely valuable if you do it with formal because you get a level of coverage that is almost impossible to get with simulation.