基于约束的核查

Electronic designs have been growing rapidly in both device count and functionality.
This growth has been enabled by deep sub-micron fabrication technology,
and fueled by expanding consumer electronics, communications, and computing
markets. A major impact on the profitability of electronic designs is the
increasing productivity gap. That is, what can be designed is lagging behind
what the silicon is capable of delivering.
The main cause of this productivity gap is the cost of design verification.
Verification complexity grows faster than the design complexity, which in turn
grows exponentially, as Moore’s Law has successfully predicted. This leads to
the verification crisis, a phenomenon that has become ever so familiar in today’s
Electronic Design Automation (EDA) landscape.
There are several remedies, each coming from different aspects of the design
and verification process. The first is the movement to higher levels of abstraction,
especially the emerging Electronic System Level (ESL) model. The key
enablers include languages that capture system level behavior and facilitate
testbench automation for high level verification.
The second are the methodology changes, exemplified by assertion-based
verification, and testbench automation highlighted by constrained random simulation.
Both can find specialized constructs in, and are facilitated by, the ESL
modeling languages.
The third is the advance of technology at the foundation of all the changes.
Constrained random simulation, with robust constraint solving capability, is
key to any practical testbench automation tool. The same fundamental solving
techniques are also shared by formal verification tools in assertion-based
verification. The formal semantics for assertions, now entrenched in the ESL
languages, connect interface constraints used in constrained random simulation,
and properties monitored in both simulation and formal verification.