"Using Solidify, the unit-level verification of a wireless networking product is drastically reduced to half. Solidify surprisingly uncovered several architecture corner case bugs that could have turned into potential system bugs. Design properties are easy to create and maintain, and Solidify provides quick feedback when properties fail. "
"Solidify uses a Verilog like property language, making it is easy for designers to understand and write properties. We are developing a methodology to write effective properties and will broadly adopt this methodology for our MCU products in various applications. We aim to eliminate time-consuming vector based logic simulation for many design blocks, using Solidify to achieve high quality verification in a short time."
"ARM uses many different validation techniques, including formal verification, to ensure high quality CPU cores. The exhaustive nature of formal verification makes it ideal for verifying every possible corner case � essential for configurable IP that's used by many customers in a variety of environments. We've recently had success with the Solidify property checker from Averant, using its Verilog-like property language to find and fix bugs in CPU blocks and interfaces. It can also extract a few standard properties directly from the RTL, allowing certain bugs to be found quickly and efficiently."
"Telecommunication IC designs are more complex in functionality and larger in density. Using simulation methodology and test vectors to verify these designs have become time consuming, ineffective, and incomplete. Hitachi, Ltd., Telecommunication Systems Division ("Hitachi TSD") has been searching for a verification solution that required no test vector and capable of verifying a large verification space in fraction of time. However, traditional verification methodologies that required no test vectors were not suitable for real designs as it lacked adequate design capacity and ease-of-use. Averant static functional verification tool, Solidify was a new alternative and it was evaluated at Hitachi TSD when it was first introduced in Japan. Solidify is easy to use and the properties are simple to write. Solidify exhaustively verifies real design behaviors equivalent of running millions of test vectors in simulation and it automatically exposes difficult and corner case bugs. Hitachi TSD has adopted Solidify on several design flows and applied it on many design areas. Solidify is effective to shorten the verification time and it improves quality of the designs at Hitachi TSD."
"Its very easy to start writing properties. The property language is in a very Verilog / C type of syntax, and its very easy to learn that. I got this piece of code, a PCI arbiter, that I hadn't seen before. I wrote some properties just to make sure that it did indeed do what an arbiter does. The first property I wrote, which is 'you are not going to arbitrate to more than one agent at any given time', failed! It took me seconds to write the property. But to simulate an arbiter, obviously is not the easiest thing to do. We would not have caught this bug because it was from an illegal state. But we would have never tested for the illegal state in the first place."
"Compaq has adopted a new methodology called static functional verification to attack difficult problems that demand significant design process bandwidth and are costly. Static functional verification allows a designer to completely verify the operation of a design without having to establish a verification testbench or develop simulation vector patterns. Instead, static functional verification uses a set of properties that describe the behavior of the design to prove proper functionality using formal verification techniques."
"We are using Solidify's new static approach as a way to reduce the time it takes us to verify our blocks. Solidify is part of our overall VLSI verification program to check corner cases and find difficult bugs in less time and with less effort."
"Solidify delivers the next generation capability in functional verification. Solidify's exhaustive verification algorithms eliminate the unnecessary and complex simulation cost at the block-level, and hence greatly reduce system-level testing time. It is an ideal tool for design and verification engineers to quickly verify blocks early in the design cycle and it automatically exposes corner cases and forbidden behaviors. Solidify's property set is simple, extendable, and familiar to HDL designers. It also provides a verification and debug environment that requires no change to the design flow."
"We determined it is crucially important to accelerate functional verification to keep our aggressive projects on schedule. We expect that by using Solidify we will not only shorten our verification schedules, but also improve our quality of results. Rising levels of integration significantly increases the likelihood a bug hiding in a block may not be found. These bugs are difficult to find and costly to fix at the chip-level. The use of Solidify's static verification, at the block-level before integration, will enable us to find corner cases that were previously too difficult or too time-consuming to reach. "The problem with control-like corner cases is that its often quite difficult to enumerate them. You have multiple interfaces with multiple behaviors. Its hard to create them often in the test bench logic. Solidify gives us the opportunity to look across a universe of conditions statically, and cover these corner cases without explicitly thinking of them. This is the behavior I am looking for. Does this block adhere to that behavior? "We don't get a lot of actual design re-use [at NVIDIA]. The bulk of our design gets redesigned each generation, because that's our value-added. What is interesting and which is high leverage for me is reuse of the testing environment, the verification environment. That's tremendous reuse. So we found just tremendous leverage in the fact that we don't have to keep rewriting everything, all the time. Solidify helps us to verify our designs, get them to market quicker. We look forward to great things from it."
"Solidify verifies RTL versus abstract properties, unlike netlist-to-netlist verifiers like Formality. The properties are easier to create than a Specman or Verilog testbench. When Solidify finds problems, the counter-example vectors it produces are nicely pruned, and they pointed me right at the problem areas. it's been very comforting to know that the circuit passes in Solidify. We're now verifying blocks with some nice interesting pipelines and more complicated temporal behavior. It's really very nice to be able to prove that module X will generate exactly the "right thing" three cycles from now, especially when module X has a few thousand bits of inputs and a fair amount of internal state."
"Formal verification's main strength is that unlike simulation, it does not depend on the probability of reaching any given scenario. If the scenario can occur, however infrequently, formal verification will find it. This makes the difference for complex systems where the number of degrees of freedom makes it impossible to design a simulation environment which will not miss certain combinations. In fact, we have found a number of just such bugs in designs we had thought were exhaustively simulated, by using Solidify."
"Solidify, I would say, is 'the' state of the art in terms of formal verification. If we look ten years ago, in terms of the challenges, it has actually stepped up and solved those challenges, in terms of the size of the practical application, in terms of ease-of-use, and in terms of identifying which areas to apply formal verification to. It is really a major step forward."