{"showBreadcrumbs":true,"breadcrumbs":[{"title":"Siemens EDA Software","path":"/en-US/"},{"title":"IC Tool Portfolio","path":"/en-US/ic"},{"title":"Catapult High-Level Synthesis","path":"/en-US/ic/catapult-high-level-synthesis"},{"title":"High-Level Verification","path":"/en-US/ic/catapult-high-level-synthesis/hls-verification"},{"title":"SLEC","path":""}],"tagline":"Overview","title":"C++/SystemC/RTL Formal","description":"Formally verify the correctness of hand-written or Catapult-generated RTL vs High-Level models using Sequential Logic Equivalence Checking. Even with differences in language, timing, and interfaces, SLEC-System verifies manual RTL with SLEC-HLS proving C++ vs Catapult generated RTL.","pricingCurrency":"US$","image":{"url":"https://images.sw.siemens-cdn.com/siemens-disw-assets/public/7bYm5D0BUOcEc66s9yejQT/en-US/slec-system-flow-promo-640x480.jpg?w=640","alt":"slec system flow promo\n\n","linkData":"{\"name\":\"slec-system-flow-promo-640x480.jpg\",\"id\":\"7bYm5D0BUOcEc66s9yejQT\",\"contentType\":\"image/jpeg\"}"},"primaryButton":{"text":"Read Fact Sheet","env":"master","resource":{"ids":["1k67KCAvICWaDj7NENUIcD"],"mode":"selected","query":{"q":"SLEC System","sorts":[{"field":"publishedDate","order":"desc"}],"filters":[{"field":"collection","values":["resource"],"operator":"OR"}],"postFilters":[],"verboseLocalization":true},"idsQuery":{"size":1,"filters":[{"field":"collection","values":["resource"],"operator":"OR"},{"field":"id","values":["1k67KCAvICWaDj7NENUIcD"],"operator":"OR"}],"verboseLocalization":true}}},"secondaryButton":{"text":"Read White Paper","env":"master","resource":{"ids":["3reR7fz4DH3YQxIEYy6cKy"],"mode":"selected","query":{"q":"Renesas","sorts":[{"field":"publishedDate","order":"desc"}],"filters":[{"field":"collection","values":["resource"],"operator":"OR"}],"postFilters":[{"field":"resourceType","values":[],"operator":"OR"}],"verboseLocalization":true},"idsQuery":{"size":1,"filters":[{"field":"collection","values":["resource"],"operator":"OR"},{"field":"id","values":["3reR7fz4DH3YQxIEYy6cKy"],"operator":"OR"}],"verboseLocalization":true}},"leftIcon":false}}
  1. Home
  2. Siemens EDA Software
  3. IC Tool Portfolio
  4. Catapult High-Level Synthesis
  5. High-Level Verification
  6. SLEC
Overview

C++/SystemC/RTL Formal

Formally verify the correctness of hand-written or Catapult-generated RTL vs High-Level models using Sequential Logic Equivalence Checking. Even with differences in language, timing, and interfaces, SLEC-System verifies manual RTL with SLEC-HLS proving C++ vs Catapult generated RTL.

slec system flow promo
KEY FEATURES

Formal Verification of C++/SystemC/RTL

When designers move high-level design descriptions into RTL, or make power optimizations to RTL, they need to know if the result is functionally equivalent to the original, possibly high-level description. SLEC delivers solutions for manual, HLS, and power optimization RTL verification.

{"items":[{"title":"Leading Formal Equivalency Checking","subtitle":"SLEC SOLUTIONS","description":"<p>Paired with a range of best-in-class engines, this powerful</br>verification approach enables bug hunting, bounded-check, and full-proof strategies. SLEC is designed to complement typical simulation-based verification, and it is integrated with debug tools like Siemens EDA Visualizer for understanding</br>falsifications.</p>","image":"https://images.sw.siemens-cdn.com/siemens-disw-assets/public/1O15JTN5ZK565Vc9hbU4za/en-US/slec-system–comprehensive-formal-verification-flow-promo-640x480.jpg?w=640&q=60","imageAlt":"slec system comprehensive formal verification flow promo","imageTitle":"slec system comprehensive formal verification flow promo","rightIcon":"fal fa-long-arrow-right fa-lg"},{"title":"Manual Formal Equivalence Checking","subtitle":"SLEC-SYSTEM","description":"<p>For the toughest manual formal verification challenges involving complex implementations in hand-coded RTL. SLEC-System delivers capabilities enabling formal proof of design blocks as challenging as double precision floating point multiplication, mult-add and other problems that simply cannot be exhaustively simulated in RTL.</p>","image":"https://images.sw.siemens-cdn.com/siemens-disw-assets/public/5n4YjpmKaJ4qYwToY3G7vD/en-US/slec-system-manual-promo-640x480.jpg?w=640&q=60","imageAlt":"slec system manual promo","imageTitle":"slec system manual promo","rightIcon":"fal fa-long-arrow-right fa-lg"},{"title":"Automatic Formal Equivalence for Catapult HLS RTL","subtitle":"SLEC-HLS","description":"<p>An external testbench or SCVerify RTL simulation can provide good functional verification confidence. SLEC-HLS enhances confidence by verifying that Catapult high-level synthesis RTL has exact functional equivalency to the source C++ without requiring exhaustive simulation. Mismatches are formally proven and flagged with counter-examples.</p>","image":"https://images.sw.siemens-cdn.com/siemens-disw-assets/public/6iZVEVlWPFKmTw2YZim7VC/en-US/slec-hls-promo-640x480.jpg?w=640&q=60","imageAlt":"slec hls promo","imageTitle":"slec hls promo","rightIcon":"fal fa-long-arrow-right fa-lg"},{"title":"RTL Power Optimization Formal Verification","subtitle":"SLEC-PRO","description":"<p>When making optimizations automatically for Power, PowerPro Optimizer users now benefit from an automated setup for SLEC that proves the sequential equivalence between the original and optimized RTL. SLEC-Pro can also be leveraged in conjunction with RTL optimized as part of the Catapult HLS Low Power flow.</p>","image":"https://images.sw.siemens-cdn.com/siemens-disw-assets/public/1NF3B9lqpiAzcyi6Bi1v1L/en-US/slec-pro-promo-640x480.jpg?w=640&q=60","imageAlt":"slec pro promo","imageTitle":"slec pro promo","rightIcon":"fal fa-long-arrow-right fa-lg"}],"env":"master"}

SLEC SOLUTIONS

Leading Formal Equivalency Checking

<p>Paired with a range of best-in-class engines, this powerful</br>verification approach enables bug hunting, bounded-check, and full-proof strategies. SLEC is designed to complement typical simulation-based verification, and it is integrated with debug tools like Siemens EDA Visualizer for understanding</br>falsifications.</p>

slec system comprehensive formal verification flow promo

SLEC-SYSTEM

Manual Formal Equivalence Checking

<p>For the toughest manual formal verification challenges involving complex implementations in hand-coded RTL. SLEC-System delivers capabilities enabling formal proof of design blocks as challenging as double precision floating point multiplication, mult-add and other problems that simply cannot be exhaustively simulated in RTL.</p>

slec system manual promo

SLEC-HLS

Automatic Formal Equivalence for Catapult HLS RTL

<p>An external testbench or SCVerify RTL simulation can provide good functional verification confidence. SLEC-HLS enhances confidence by verifying that Catapult high-level synthesis RTL has exact functional equivalency to the source C++ without requiring exhaustive simulation. Mismatches are formally proven and flagged with counter-examples.</p>

slec hls promo

SLEC-PRO

RTL Power Optimization Formal Verification

<p>When making optimizations automatically for Power, PowerPro Optimizer users now benefit from an automated setup for SLEC that proves the sequential equivalence between the original and optimized RTL. SLEC-Pro can also be leveraged in conjunction with RTL optimized as part of the Catapult HLS Low Power flow.</p>

slec pro promo

Ready to have a conversation about SLEC System?

Any questions you may have, we have answers.

Email us

image of arrows

Join the IC Design Community

Join the discussion on new topics, features, content, and technical experts.

Access Community
two squares on top of each other

Catapult Support

Access detailed documentation, on-demand training resources and more.

Catapult Support Center

EDA Consulting

Helping you achieve maximum business impact by addressing your complex technology and enterprise challenges with a unique blend of development experience, design knowledge, and methodology expertise.

Consulting Services