Part of the  

Chip Design Magazine


About  |  Contact

Posts Tagged ‘formal verification’

Research Review November 12, 2013

Tuesday, November 12th, 2013

SmartLoc System Improves GPS Accuracy and Increases Battery Life

Researchers at the Illinois Institute of Technology have developed a system that can not only improve the accuracy of smartphone GPS systems in large city settings, but also extend their battery life.  While GPS accuracy in highly congested areas averages about 40 meters, the new system claims accuracies of 20 meters or better.

The new system uses a phone’s inertial tracking systems, (accelerometer), and compass to glean more detailed information about the users location between GPS location updates.  In addition to tracking the movement of the phone, the system builds a database of geographic features near a given GPS location.  For example, as a car travels over a humped bridge, the phones accelerometer produces a recognizable pattern of slightly increased and then slightly decreased downward acceleration.  The system can use this pattern to pinpoint the phones location on a nearby bridge that fits the pattern.  All geographic information is currently provided by Google Maps via the 4G network.  These network accesses use significantly less power than GPS functionality increasing battery life.  Using the SmartLoc system, as its called, it may even be possible to turn off GPS circuitry for periods of time resulting in even greater battery efficiency.

Selling Verification Internally
Paul McLellan chronicled ARM’s Laurent Arditi’s efforts to promote the use of formal verification techniques.  The advice given by Arditi can be applied to selling any new technology in-house.  Arditi advises engineers first,  not to oversell a technology by promising benefits that the system simply can’t deliver, and second to record metrics on the gains and costs of the technology meticulously over each project where the new technology is utilized.  By keeping expectations rational and being able to objectively report results, engineers can more easily influence executive decision makers to participate in their own success.

Arditi was specifically working on propagating successful formal verification techniques with ARM and reports that the aspects of a design to focus formal verification on are:

  • embedded assertions/properties are primarily written for simulation and so can be used for formal at no extra cost
  • X-propagation is low hanging fruit since simulation has issues with it and formal can do it with very few hand-written properties
  • complex clocking schemes are hard to verify with simulation but formal has found many corner case bugs and a major bug on the Cortex-A12
  • use Jasper ProofKits
  • reduce the cost of simulation. correlate formal coverage with simulation coverage, don’t try and do stuff like X-propagation in simulation, remove a big effort from simulation/humans
  • use simulation tricks (like reducing FIFO depths, changing arbitration) to reduce formal proof times too”

Verifying Security Aspects Of SoC Designs

Thursday, August 8th, 2013

This paper presents Jasper technology and methodology to verify the robustness of secure data access and the absence of functional paths touching secure areas of a design. Recently, we have seen an increasing demand in industrial hardware design to verify security information. Complex system-on-chips, such as those for cell phones, game consoles, and servers contain secure information. And it is likely that the presence of this information makes providers vulnerable to unauthorized access to secure data. The potential business loss, direct and indirect, is large, and verifying whether the secure information can be leaked is hard to achieve with conventional RTL validation methods. The security requirements are not easily expressible by regular SVA assertions; therefore, it is not practical to achieve validation with standard formal verification tools. Jasper’s Security Path Verification App (SPV) is part of a wide spectrum of apps we provide for design and verification domains. SPV provides a comprehensive solution to the security path verification problem. With SPV, it is convenient to specify the security paths and perform an exhaustive verification based on our special path sensitization technology, automatic connectivity abstraction, path divide-and-conquer search, and by leveraging the comprehensive core formal engines and usability features of the JasperGold platform. Jasper security path verification has been successfully used by various customers in the SoC domain, confirming the impact of Jasper’s solution and technology roadmap.

To download this white paper, click here.

Where Should I Use Formal Functional Verification?

Thursday, July 11th, 2013

With innovations in formal technologies and methodology, the benefits of formal functional verification apply in many more areas. Although a generic awareness of where formal functional verification applies is useful, understanding the “what” and the “why” leads to greater success. Clearly, if we understand the characteristics of areas with high formal applicability, we can identify not only which blocks are good candidates, but also what portions or functionalities of the blocks will give the greatest return on the time and effort invested. In recent years, we have come to realize that although we can apply formal to entire blocks, it can be more valuable to apply formal partially within blocks by choosing the functions that have the highest return. This paper will aid the reader in understanding where, why and how to apply formal for the highest return.

To download this white paper, click here.

Formal Verification Of Power-Aware Designs

Thursday, May 9th, 2013

Power reduction and management methods are now all-pervasive in system-on-chip (SoC) designs. They are used in SoCs targeted at power-critical applications ranging from mobile appliances with limited battery life to big-box electronics that consume large amounts of increasingly expensive power. Power reduction methods are now applied throughout the chip design flow from architectural design, through RTL implementation to physical design.

This white paper addresses the verification challenges posed by power-aware chip design, and how the JasperGold Low Power Verification App works with other JasperGold Apps to overcome those challenges. It covers:

  1. Power-aware verification challenges
  2. Power-aware verification requirements
  3. The limitations of traditional power-aware verification
  4. Meeting power-aware verification requirements with JasperGold Apps

Extension Media websites place cookies on your device to give you the best user experience. By using our websites, you agree to placement of these cookies and to our Privacy Policy. Please click here to accept.