草榴社区 Cloud
Cloud native EDA tools & pre-optimized hardware platforms
Request a Free Trial →
ASIP eUpdate February 2024
ASIP Designer
草榴社区’ 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:
Technology Feature I: Advanced Verification Add-On / Formal Verification Support
Overview
With ASIP Designer? V-2023.12, we introduce a new product “ASIP Designer Advanced Verification Add-On”, which includes:
- Formal ISA verification support (new feature)
- Automatic test program generation for hazard rules (new feature)
- Extra license for random instruction sequence generator “RISK” (existing feature)
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 ISA Verification Support
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:
- Assertions: conditions that must be true under all circumstances. The formal solver is challenged to find a counterexample.
- Cover Points: specific states that must be covered and reachable. The formal solver is challenged to find an example.
- Assumptions: additional constraints to inputs and signals can be provided to limit the search range for the formal solver.
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 草榴社区 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:
- A reference model in SystemVerilog describing the functional behavior;
- Assertions describing the expected correct results and the fact that the instruction must be completed within a given number of clock cycles;
- Assumptions describing certain characteristics of the compiler-generated code, to prevent false negatives.
The SystemVerilog testbench is then imported into 草榴社区’ VC Formal tool to perform the actual formal solving. Complementarily, the same testbench can be run in an RTL simulation, for example with 草榴社区’ 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
Automatic Test Program Generation for Hazard Rules
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.
Technology Feature II: Reverse Debugging
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:
- In Tracing Mode, the ISS traces instructions and write accesses to selected storages. This data is stored internally while the simulation is executed.
- In Replay Mode, the ISS iterates over the stored trace and reconstructs previous states based on the traced values.
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.
What’s New: ASIP Designer V-2023.12 Release
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
Example Processor Models
In the 2023.12 release the following updates have been made to the library of example processor models:
- The “Trv” model family (RISC-V processors) has been updated:
- The following instruction extensions have been added to all 32-bit variants:
- Zba: improved generation of addresses that index into arrays of basic types
- Zbb: basic bit manipulation
- Zbs: single-bit instructions (clear, extract, invert, set)
- Update of the C++ Standard Library to Libcxx-16
- The following instruction extensions have been added to all 32-bit variants:
- Formal verification has been set up for the TLX processor model.
- A new processor model, “smarT” has been added, which is an accelerator for convolutional neural networks with medium throughput. The key features are:
- Dual convolution unit with 16 8-bit multipliers each,
- 128-bit memory interface with vector-based vector addressing,
- DMA between small local memory and external memory.
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.
Processor Modeling
- Support for parameterized chess_view rules to model record component access on a record alias register file.
C/C++ Compiler
- Chess-specific restrict pointer qualifiers expressing the absence of loop-carried dependencies.
- Deep duplication of expressions based on complex-spillable operands.
- Improvements to the LLVM compilation flow:
- The limitation on the maximum number of processor-specific types has been removed.
- Direct support for sign-extend intrinsics, avoiding that LLVM lowers a sign extension to a shift-left/shift-right combination.
- The LLVM front-end switches to the most recent LLVM version 17.0.
ChessDE GUI, Instruction-Set Simulation and Debugging
- The ChessDE editor now allows to display the same file in two tabs.
- The language server support, which has been introduced to the ChessDE editor in Release 2022.12, has been further enhanced and extended with additional functionality.
- Clickable references from generated HDL files to nML and PDG sources.
- Reverse debugging support. See “Technology Feature II: Reverse Debugging” above
- Direct Memory Interface (DMI) cache in SystemC simulations.
RTL Generation, Verification, and Synthesis Support
- New Advanced Verification Add-On product, including Formal Verification support. See “Technology Feature I: Advanced Verification Add-on / Formal Verification Support” above
- Support for architectural clock gating of separate register contexts.
Additional Resources
Video
Intro to ASIP Designer
The efficient way to design, implement, program and verify your custom processor.
Training
ASIP Designer Online Training
Deep dive into the concepts, languages, and files used to capture a processor design.
Request Access
New Videos
ASIP Designer Tutorial Videos
Learn from experts: Demo videos of ASIP Designer methodology and use cases
Register Now