Cloud native EDA tools & pre-optimized hardware platforms
Synopsys¡¯ solution to efficiently design and implement your own application-specific instruction-set processor (ASIP) when you can¡¯t find suitable processor IP, or when hardware implementations require more flexibility.
This bi-annual newsletter provides you with easy access to ASIP-related resources. This issue includes the following topics:
With ASIP Designer? V-2023.12, we introduce a new product ¡°ASIP Designer Advanced Verification Add-On¡±, which includes:
The following sections give a brief explanation of the new features introduced with the Advanced Verification Add-On product. This product requires a separate license.
Formal verification is a powerful method to work towards a bug-free design, complementary to traditional simulation. In contrast to simulation, formal verification exhaustively explores the complete design space and results in a mathematical proof or disproof that the implementation exhibits expected behavior. While simulation uses stimuli to verify a certain testcase, formal verification works from a mathematical description of expected behavior, and the formal tool explores all legal scenarios.
To guarantee the correctness of an instruction, even one as simple as an add instruction, many scenarios must be considered. There may be interfering hazards, the processor may be in different modes (normal issue, on-chip debugging, interrupt, power down, ¡), or in VLIW architectures there may be interfering parallel instructions.
In formal verification, there is no need to specify or enumerate scenarios where execution of an instruction can go wrong. It is needed only to express the behavior in a formal way. The processor model, representing a finite state machine, is checked against temporal properties. These properties can be expressed in the SystemVerilog language and include:
ASIP Designer supports formal verification by taking advantage of the information that is inherent in the nML processor model, and automatically generating a SystemVerilog testbench that can be evaluated in the Synopsys VC Formal? tool, as depicted in Figure 1.
Figure 1: Automatically generated SystemVerilog components and flow into VC Formal and VCS
For each nML rule, the Go RTL Generator of ASIP Designer generates:
The SystemVerilog testbench is then imported into Synopsys¡¯ VC Formal tool to perform the actual formal solving. Complementarily, the same testbench can be run in an RTL simulation, for example with Synopsys¡¯ VCS?, to verify the assumptions. The generated assertions are easy to review, and the user can add extra assertions.
The generated testbench for formal checking works according to the principle as depicted in Figure 2
Figure 2: Convergence strategy using reference model and intermediate CPU
In addition to the reference model, the SystemVerilog testbench contains two instances of the ASIP RTL implementation, which is the design-under-test, named CPU 1 and CPU 2 with separately stored results. CPU 1 is fed with instructions in isolation only, while CPU 2 has an unconstrained pipeline. First, CPU 1 is checked against the reference model, then CPU 2 is checked against CPU 1, which helps achieve a faster convergence of the formal solver.
Figure 3 shows a screenshot of the corresponding project running in VC Formal. As with RTL synthesis and simulation tools, ASIP Designer automatically generates the necessary script infrastructure for a seamless flow into VC Formal.
Figure 3: ASIP model checking using VC Formal
The Advanced Verification Add-On contains a utility to automate C test program generation for hazards. The hazard decoder is a challenging module to reach RTL source coverage closure. The new utility automates the generation of tests that trigger all hazard rules for this purpose, building upon the existing infrastructure of automatically generated one-liner tests and the existing hazard reporting functionality of the disassembler.
ASIP Designer and ASIP Programmer? V-2023.12 now support reverse debugging. Reverse debugging in the ChessDE GUI allows users simulating an application to step back in simulation time and inspect a previous state of the processor. To achieve this, we distinguish two separate operation modes of the simulation:
Figure 4 shows a screenshot of the ChessDE GUI with reverse debugging support.
Figure 4: ChessDE GUI with Reverse Debugging
In a running simulation, tracing mode can be started any time by pressing a dedicated ¡°Record¡± button. Instructions and selected write events are now copied into a sliding history window that stores the data cycle by cycle into a circular buffer. Within the sliding history window, the debugger now allows reverse stepping and reverse continue, functionality that is accessible via dedicated buttons newly added to the debug control panel. Reverse debugging is fully user configurable, including the size of the history window and the selection of resources to be traced.
Since the last edition of this newsletter, we have launched a new feature release of ASIP Designer in December 2023, providing various enhancements and extensions. The following is an extract, sorted by categories (customers can refer to the official Release Notes for a comprehensive list).
Click on each tab for additional information about that new feature
In the 2023.12 release the following updates have been made to the library of example processor models:
smarT is based on the RISC-V Trv32p5x model. The example also contains a prototype version of the TensorFlow Lite for Microcontrollers (TFLM) runtime mapped on and optimized for the smarT processor.
The smarT example has not yet been distributed with ASIP Designer V-2023.12, but it is already available on demand. It will be distributed with the V-2023.12-SP1 service pack release scheduled for March 11, 2024.