HECTOR is the next-generation of formal technology—a block-level consistency checker built to deliver high-performance checks between independently developed models and exhaustive verification of successive design refinements all without testbenches, assertions, or coverage.
HECTOR is designed to help find bugs and reduce RTL bring-up time, verify algorithmic consistency through design changes without running simulation, and increase functional signoff certainty by verifying transaction equivalence between high-level models and RTL implementations. Its patented compilers improve capacity by generating word-level RTL and Formal C/SystemC models. The powerful formal algorithms it provides find proofs in minutes or hours, not days, and its unique multiple leaf-level solvers solve complex logic. HECTOR uses hierarchical equivalence, automatic design partitioning, efficient and patented memory models, and multi-processor support to rapidly converge on proofs. HECTOR also supports multiple languages: Verilog, VHDL, SV, C, C++, and SystemC.*
Figure 1. HECTOR Overview
HECTOR is well suited to algorithm-intensive blocks including video processing, wireless media, cameras, encryption/decryption logic, transformations, GPUs, and floating point. HECTOR can be targeted at data-path dominated designs, and arithmetic blocks including floating point and, uniquely, bit-serial division. HECTOR is also unique in the formal space in that it can do consistency checks on complete blocks including control logic.
*Not all SystemC constructs are supported. Contact your applications engineer for language support options.
Figure 2. HECTOR Flow Diagram
When a bug is found and HECTOR provides a counter-example to help resolve the issue, two debug flows are supported. A raw counter-example can be dumped directly as VCD, or the design can be compiled and simulated with VCS®, and dumped to VPD or FSDB. Full DVE interactive capabilities can be used to debug the RTL, and multiple designs can be debugged side-by-side. HECTOR also provides a debugger (HDB) similar to GDB for C/C++ code. HDB can be used to debug counter-examples in C/C++ code. HDB can be used with graphical frontends like DDD. HDB internally operates on HECTOR's formal model. HDB provides more aggressive bounds violation checking, warns about accesses to non-initialized variables, and provides code annotation.
Figure 3. HECTOR RTL counter-example debug in DVE
Figure 4. HECTOR C++ counter-example debug in HDB
HECTOR Formal Block-Level Consistency Checker
HECTOR has been shown effective for commercial designs. HECTOR provides block-level consistency checks with no testbenches, assertions, or coverage required. HECTOR is used to speed design bring-up, verify design changes, and validate that implementations are equivalent to algorithmic specifications to aid in achieving tapeout criteria. HECTOR has been proven to be effective on arithmetic blocks including floating point, and used on video, audio, datapath, encryption, decryption, wireless, camera, GPU, and other designs. Please contact your account team to get more information.