Verification Overview
Mplicity has developed a comprehensive verification approach predicated on accepted Functional, Behavioral, and Formal verification methodologies to ensure that its CoreUpGrade process and automatic tools will not introduce any functional faults.
Mplicity’s verification approach allows developers the flexibility to:
- Perform solely Functional Verification on an extension of the original design to verify the design. This is accomplished by running dynamic simulations (at the RTL or at gate level Netlist/EDIF) with or without timing constraints to confirm that each of the Virtual-Multi-Logic-Blocks has the identical test vector results as the original design.
- Create a Behavioral Model in order to simplify the debug, functional test verification and overall system simulation. The behavioral model is verified in the same process as the original design and becomes the “Golden Model" (GM). The GM will then be used in a Formal Verification process to verify the enhanced CoreUpGrade design.
- The Formal Verification methodology is used to perform equivalence checking (Formal EC) between the GM behavioral functionality and the CoreUpGrade Netlist/EDIF results to ensure the correctness of the CoreUpGrade Flow.
Mplicity’s verification approach assures both the correctness and functionality of the CoreUpGrade process. The diagrams below illustrates the CoreUpGrade design flow as well as the aforementioned verification phases.
Functional Verification
Mplicity’s Functional Verification Methodology is used to validate the enhanced CoreUpGrade design and is applicable for both RTL level and Gate level verification and simulations. The objective being to successfully run all of the design tests executed on the original design test bench on each of the new Virtual-Multi-Logic-Blocks (VMLB).
In doing so, it is possible to compare each cycle, all the inputs and the machine state registers of the GM with one VMLB while all other VMLB hold X’s. This procedure is repeated for each of the available VMLB to verify that no inter-core dependency problems exist.
The following diagram demonstrates the basic concept of Mplicity’s functional tests methodology:

Behavioral Model
Mplicity also allows the RTL to be used to automatically create an RTL Behavioral Model that enables early simulation and integration of the entire system. The enhanced RTL generated by the Genghis-Khan tool has the equivalent logical functionality as the enhanced CoreUpGrade Netlist/EDIF produced by the Hannibal tool and is applicable for both RTL and Gate Level flows.
Formal Verification
Mplicity’s CoreUpGrade Formal Verification Methodology utilizes off-the-shelf EDA tools and by developing a close working relationship with the leading formal verification EDA vendors Mplicity is able to provide a smooth formal verification flow for CoreUpGrade. As in the case with Synopsys, Synopsys collaborated with Mplicity to ensure that the multi-core verification flow records the retiming and other data so that designers can validate all aspects of their multi-core design implementation flow.
RTL Flow Verification

Gate Level flow verification

|