Linking is the process of converting one or more RTL-specified designs into a database of information suitable for formal analysis. Linking involves several steps including:
Each of these steps is detailed in the following sections:
Design elaboration
Design elaboration entails resolving instantiated component names, verifying hierarchical connections, setting parameter values and propagating them through the hierarchy. During elaboration, if components cannot be found in the current Design nor in any specified library, a warning is issued, but elaboration will not abort. Missing hierarchical components can affect analysis results, so care should be taken to ensure all components needed for any planned analyses are included in the Design or a Library.
Schematic generation
After completion of elaboration, a schematic representation of the design is generated. The schematic is not a gate-level schematic but rather a function-level schematic. Schematic functions include muxes, adders, subtractors, signal rippers, signal combiners, and gate primitives such and And's, Or's, etc.
Logic gate generation and reduction
The schematic representation is then converted to a logic gate representation. Logic reduction also occurs at this time in essence resulting in a first-stage synthesis of the design (i.e. conversion of RTL to generic gates).
BDD database creation
The gate-level logic is then converted to a BDD (Boolean Decision Diagram) database. The BDD representation of the design is used for many of the logic analysis functions of X-Amin including equivalency checking, truth table generation, and temporal proofs. The BDD representation of a signal can be displayed in a BDD Plot Diagram.