Published on January 17th, 2008

Verification – the Next Step for ESL

What if we write a high level collection of models and – when the collection "works" in its native software environment – compile it with some whiz-trick-tool that produces stellar RTL that is guaranteed to work whether simulated or not?
Chad SpackmanESL (electronic system level) looked, for a while, as if it would be defined as a design environment featuring SystemC as the design language. System-on-chip (SoC) development would take place by modeling both the design and the surrounding environment at the transaction level. Transaction level models (TLMs) would allow major design blocks and surrounding environments to be behaviorally coded, cycle accurately, and then analyzed in a conventional simulator. Such modeling also would facilitate architectural exploration and design tradeoffs.

And yet, SystemC appears to have become, largely, a test environment language. Why?

The answer to this conundrum is because the steps required to take a design from working TLM to working register transfer level (RTL) turn out to be hard. Coding SystemC in synthesizable form is so tedious that learning a new language – versus using Verilog or VHDL – is simply not worth the effort. TLM synthesis could change the current course for SystemC, but TLM synthesis has yet to be realized. Thus, SystemC is relegated to a test language.

SystemVerilog is perhaps a contender for the ESL design language. It's Verilog with C extensions, which is less ambitious than behavioral synthesis and not a stretch for teams that are Verilog-RTL-centric. The solutions that exist add further, proprietary, extensions to the language, complete with custom synthesis and simulators.

Various C and C++ based ESL efforts are available, some accepting un-timed input, some not. Most list a range of exclusions on the input language to support synthesis. These exclusions are often severe enough to make designers wonder, "Why am I using a high level language if there is a bunch of it I'm not allowed to use?"

By all appearances, contemporary ESL exclusively targets the front end of the design process. The goals are modeling, design exploration, and better design description. The intended outcome is RTL that rivals handwritten RTL and that can also be functionally proven in simulation.

All of which misses what should be a major objective and benefit of moving up in levels of input language abstraction. Design teams have found ways to solve difficult design entry problems – abstract description, in itself, is a nicety for all but the most complex of SoC designs. However, verification is where the re-spin and market window battle is won or lost. What can be done about that and shouldn't that be a primary target of ESL?

My ideal for ESL is simple. Write a high level collection of models and – when the collection "works" in its native software environment – compile it with some whiz-trick-tool that produces stellar RTL that is guaranteed to work whether simulated or not. Doesn't that accomplish everything currently defined as ESL, with the huge addition of verification, which seems completely off the industry radar?

This goal is achievable. Language choice is only somewhat important; it must support complex data types that can be used to describe memory and hardware. Pointers can provide a very powerful means of implementing memory access. Hardware concurrency of any degree is supportable, as long as some form of threads operation is present.

As illustration, consider an overly simplistic ANSI C-to-RTL compiler. The designer must insert clocks (thread yields) for the resulting RTL to obey C semantics. Functions that will become state machines are declared as threads. Variables become flip-flops, or memory, as specified by the designer. Data-paths and queuing are explicitly coded. The compiler turns threads into state machines and turns specific functions into externally visible ports with handshakes. Array references and pointer dereferences become memory reads and writes where appropriate. A lightweight scheduler ensures hardware behavior. The C can be compiled with gcc and a pthreads library and it goes like a rocket natively, allowing rigorous proof. Then the C–to-RTL compiler is deployed, and the resulting RTL could be shown to be formally equivalent to the C we started with. We can simulate if we choose, but formal verification is the standard which links the functionally-proven software representation to the final result.

Although such a process addresses the simulation bottleneck, the flow outlined above is too explicit and detailed to code. The compiler needs to become somewhat smarter. The next step might be to have it perform clock insertion, but this presents a problem. If clocking is no longer in the C source, it is no longer meaningful to prove functionality natively. Formal equivalence from the un-clocked software domain to the clocked hardware domain is equally meaningless. Another simple solution: Have the compiler spit out the clocked version of the C as well as the RTL. We test the clocked version natively this time and again prove formal equivalence with the RTL.

If the design tool produces cycle-accurate ANSI C, as well as RTL, there is no limit with respect to compiler intelligence. Resource sharing, parallelism, datapath widths, even power considerations can be performed by the compiler. Verification takes place in a native software environment, with formal equivalence closing the loop, and simulation takes a back seat in device verification.

ESL must provide for exploration and abstract design entry, but verification must be intrinsic to the process for ESL to take hold.
Chad Spackman, founder and CTO of CebaTech Inc., has 15 years of semiconductor design and holds five patents in the field. Chad's achievements include over a dozen analog designs for various foundries, six large-scale communications ASIC designs in the communications sector, and a complete TCP/IP TOE engine now licensed to a major semiconductor company. Chad holds a B.SC in physics and Bachelor and Master's degrees in engineering from the University of Pennsylvania and Penn State University, respectively.

Tech Videos

©2018 Extension Media. All Rights Reserved. PRIVACY POLICY | TERMS AND CONDITIONS

Extension Media websites place cookies on your device to give you the best user experience. By using our websites, you agree to placement of these cookies and to our Privacy Policy. Please click here to accept.