Verification Needed to Take High-Level Synthesis Mainstream

This blog focuses mostly on verification, but from time to time we like to take a look at other aspects of the EDA industry. Today we’d like to discuss high-level synthesis (HLS), its progress and status, and what’s keeping it from being  a mainstream technology used for every chip design. It turns out that this topic has a lot to do with verification, so we’re not straying too far from our primary focus.

To start, let’s define what we mean by HLS in contrast to the mainstream technology of logic synthesis. Generating gates from a hardware description language (HDL) moved from a research problem to viable products around 1988. The ultimate winner among several promising companies was Synopsys, in part because they chose a register-transfer level (RTL) subset of the popular Verilog HDL as their input format. Their tools generated a gate-level netlist using the cells available in an ASIC vendor’s library.

This approach took off quickly with leading-edge companies designing some of the largest chips, since the gate counts had exceeded what manual effort could handle. However, by most reckonings it took another four or five years before logic synthesis was a mainstream technology adopted by most chip design teams. Certainly common EDA tool attributes such as speed, capacity, and ease of use all improved during this period, increasing the benefits of logic synthesis to the point where even teams reluctant to adopt an HDL felt compelled to do so.

But there were also three key developments in the industry overall. The first is simply that more and more chips grew beyond the point at which manual gate-level design was practical. Second, ASIC vendors fully embraced the automated flow, providing better models for cells and wires so that logic synthesis tools could generate netlists meeting timing requirements and better estimate die size. Many ASIC vendors also started allowing sign-off in commercial HDL/gate-level simulators, simplifying the flow even further.

Perhaps the biggest single factor in taking logic verification mainstream was the availability of formal equivalence checkers. These checkers read in two representations of design and used formal algorithms to compare them. For example, a checker can read in the input RTL and the output netlist from logic synthesis and formally prove that they are functionally equivalent. A synthesis tool can have bugs, just like any other piece of software, so equivalence checking serves as a double-check that the RTL has been properly transformed into gates.

Many mainstream logic designers were suspicious of logic synthesis, and worried about what would happen if the netlist contained errors. Trying to check the gates by re-running the complete RTL test suite was time-consuming and provided no guarantee that differences would be detected. Formal equivalence checking changed all that. If different EDA vendors provided the synthesis and checking tools, or if the same vendor maintained separate teams who didn’t share code, then the mainstream designer was finally comfortable with logic synthesis.

HLS should really be just the next step in this process, moving up to a higher level of abstraction for the input hardware description. HLS tools typically take untimed or partially timed C/C++/SystemC algorithmic models that do not define every clock stage the way that RTL does. The synthesis process is then free to choose radically different implementations to meet the design parameters, locating cycle boundaries wherever convenient. The input and output of HLS are much further apart in abstraction than the input and output of logic synthesis.

Despite availability of  several solid commercial solutions, HLS cannot be called mainstream today. Given that it is the obvious next step from logic synthesis, many of the same inhibitors and enablers apply. Speed, capacity, and ease of use have all increased. Many chip designs are growing to the point where the RTL description is huge and higher abstraction would be a clear benefit. ASIC vendor support is not a big  issue, since HLS tools either generate RTL for logic synthesis tools or are tightly integrated into the traditional logic synthesis flow.

Equivalence checking remains the sticking point. Logic synthesis makes few changes to the design state or cycle boundaries, and so combinational equivalence checking generally suffice. This breaks down the problem to formally comparing the logic between state elements such as flip-flops and registers. HLS requires sequential equivalence checking, in which the entire multi-cycle design from inputs to outputs must be formally compared.

The problem is even harder than that, given the many micro-architectural decisions made during HLS. The designer may not want the HLS tool giving hints to the equivalence checker, but without such a link a comparison many be impossible. There are sequential equivalence checkers available in the market, but none offers a complete, automated solution. Many chip developers will not adopt HLS until and unless such a solution is available. Since an equivalence checker is a verification tool, it’s fair to say that “verification is needed to take high-level synthesis mainstream.”

Given the limitations of equivalence checking, HLS users for the foreseeable future will have to re-run some of their high-level tests on the RTL model to try to detect any inconsistencies. This is where Breker can help. We generate test cases that do an excellent job of stressing your design. Further, these test cases are fully portable from high-level simulation environments such as virtual platforms to traditional RTL simulation. No rework at all is needed to re-run the test cases. We can’t offer a formal guarantee but at least we can stress-test both versions of your design.

Tom Anderson

The truth is out there … sometimes it’s in a blog.

Tags: Breker, coverage, EDA, equivalence checking, ESL, formal analysis, functional verification, HDL, high-level synthesis, HLS, portable stimulus, reuse, RTL, scenario model, Verilog

This entry was posted on Tuesday, December 2nd, 2014 at 6:56 pm. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.