Leading Formal Innovations

SoC design complexity demands fast and comprehensive verification methods to accelerate verification and debug, as well as shorten overall schedule and improve predictability. 

Leveraging the latest formal technologies and Machine Learning techniques, Synopsys VC Formal™ has the capacity, speed and flexibility to exhaustively verify some of the most complex SoC designs, find deep corner-case design bugs, and achieve formal signoff. Natively integrated with Synopsys VCS®, Verdi®, VC SpyGlass™, VC Z01X Fault Simulation and other Synopsys design and verification solutions, VC Formal continues to innovate to solve the toughest verification challenges in the industry.

Synopsys also offers Formal Verification Services specializing in enhancing productivity and reducing risk by working closely with domain experts in the deployment of verification methodology.

Key Benefits

Formal Applications

Learn About VC Formal Apps: Automated Extracted Properties (AEP)
Using formal verification to catch design bugs does not require formal expertise. Synopsys VC Formal AEP app is designed to help designers & verification engineers catch many kinds of design errors by automatically extracting properties in the design
Video Player is loading.
Current Time 0:00
Duration 0:00
Loaded: 0%
Stream Type LIVE
Remaining Time 0:00
 
1x
    • Chapters
    • descriptions off, selected
    • captions off, selected

        Automatic Extracted Properties (AEP)

        Automatic functional analysis for out of bound arrays, arithmetic overflow, X-assignments, simultaneous set/reset, full case, parallel case, multi driver/conflicting bus and floating bus checks without the need for dedicated simulation tests.

        Learn About VC Formal Apps: Formal Coverage Analysis (FCA)
        Synopsys VC Formal FCA performs formal unreachability analysis (UNR) to identify unreachable simulation coverage goals so users can either fix the design issues or exclude those coverage goals from the simulation coverage signoff criteria.
        Video Player is loading.
        Current Time 0:00
        Duration 0:00
        Loaded: 0%
        Stream Type LIVE
        Remaining Time 0:00
         
        1x
          • Chapters
          • descriptions off, selected
          • captions off, selected

              Formal Coverage Analyzer (FCA)

              Complementing simulation flows, VC formal provides proof that uncovered points in coverage goals are indeed unreachable, allowing them to be removed from further analysis—saving significant manual effort.

              Learn About VC Formal Apps: Formal X-Propagation Verification (FXP)
              Synopsys VC Formal FXP app finds X-propagation issues at the RTL stage using exhaustive formal analysis, saving time and effort from debugging RTL and gate-level simulation mismatch.
              Video Player is loading.
              Current Time 0:00
              Duration 0:00
              Loaded: 0%
              Stream Type LIVE
              Remaining Time 0:00
               
              1x
                • Chapters
                • descriptions off, selected
                • captions off, selected

                    Formal X-Propagation Verification (FXP)

                    Checks for unknown signal value (X) propagation through the design and allows tracing of the failed property to source of X in the Verdi schematic and waveform.

                    Learn About VC Formal Apps: Connectivity Checking (CC)
                    Synopsys VC Formal CC app verifies signal connectivity at the SoC level, such as SoC I/O, scan mode, register to debug bus, block pin muxing & demuxing, configurable interconnect, etc. to make sure signals are connected as intended.
                    Video Player is loading.
                    Current Time 0:00
                    Duration 0:00
                    Loaded: 0%
                    Stream Type LIVE
                    Remaining Time 0:00
                     
                    1x
                      • Chapters
                      • descriptions off, selected
                      • captions off, selected

                          Connectivity Checking (CC)

                          Verification of connectivity at the SoC level. Flexible input format ensures ease of integration. Powerful debugging, including value annotation, schematic viewing, source code browsing and analysis reporting speeds analysis. Automatic root-cause analysis of unconnected connectivity checks saves significant debug time.

                          Learn About VC Formal Apps: Formal Register Verification (FRV)
                          Synopsys VC Formal FRV app uses formal technology to exhaustively verify that the control status registers are implemented correctly using standard or proprietary bus protocols.
                          Video Player is loading.
                          Current Time 0:00
                          Duration 0:00
                          Loaded: 0%
                          Stream Type LIVE
                          Remaining Time 0:00
                           
                          1x
                            • Chapters
                            • descriptions off, selected
                            • captions off, selected

                                Formal Register Verification (FRV)

                                Helps to formally verify behavior of configuration registers for respective attributes like “read only”, “read/write” or “reset value” eliminating the need for directed simulation tests.

                                Learn About VC Formal Apps Sequential Equivalence Checking (branded)
                                Video Player is loading.
                                Current Time 0:00
                                Duration 0:00
                                Loaded: 0%
                                Stream Type LIVE
                                Remaining Time 0:00
                                 
                                1x
                                  • Chapters
                                  • descriptions off, selected
                                  • captions off, selected

                                      Sequential Equivalence Checking (SEQ)

                                      This allows comparison of designs, after register retiming, insertion of clock gating for power optimization or microarchitecture changes.

                                      VC Formal FPV App

                                      Formal Property Verification (FPV)

                                      Formal proof-based techniques to verify SystemVerilog Assertion (SVA) properties to ensure correct operation across all possible design activity even before the simulation environment is available. Advanced assertion visualization, property browsing, grouping and filtering allow simple concise access to results. Formal navigator enables debug and "what-if-analysis" with only the RTL design in the Unified Verdi GUI with/without assertions or Testbench.

                                      Learn About VC Formal Apps: Formal Security Verification (FSV)
                                      Synopsys VC Formal FSV app verifies the integrity of data flow in an SoC to make sure that there is no secure data leak to unauthorized destinations or sensitive data alternation due to influence from insecure sources.
                                      Video Player is loading.
                                      Current Time 0:00
                                      Duration 0:00
                                      Loaded: 0%
                                      Stream Type LIVE
                                      Remaining Time 0:00
                                       
                                      1x
                                        • Chapters
                                        • descriptions off, selected
                                        • captions off, selected

                                            Security Verification (FSV)

                                            Helps formally verify that secure data should not reach non-secure destinations and ensures data integrity, where non-secure data should not over-write (or reach) secure destinations.

                                            VC Formal FLP App

                                            Formal Low Power (FLP)

                                            Start Power Aware Verification at the block level with Formal Low Power (FLP). FLP allows complete verification of power controller, power aware connectivity checking with CC App, and power aware bug hunting with the FPV App.

                                            VC Formal FTA App

                                            Formal Testbench Analyzer (FTA)

                                            Testbench Quality Assurance provides the unique capability to assess the quality of formal environment. The native integration of Testbench Quality Assurance with VC Formal provides meaningful property coverage measurements as part of formal signoff and identifies any weaknesses such as missing or incorrect properties or constraints. The native integration delivers 5-10X faster performance compared to stand-alone fault injection methods.

                                            Learn About VC Formal Apps: Datapath Validation (DPV)
                                            Synopsys VC Formal DPV app performs transactional equivalence checking between C-to-C, C-to-RTL, and RTL-to-RTL to ensure mathematical functions are implemented correctly according to spec.
                                            Video Player is loading.
                                            Current Time 0:00
                                            Duration 0:00
                                            Loaded: 0%
                                            Stream Type LIVE
                                            Remaining Time 0:00
                                             
                                            1x
                                              • Chapters
                                              • descriptions off, selected
                                              • captions off, selected

                                                  Datapath Validation (DPV)

                                                  Integrated HECTOR™ technology within VC Formal and contains custom optimizations and engines for datapath verification (ALU, FPU, DSP etc.) using transaction level equivalence. This app leverages the Verdi graphical user interface for debug.

                                                  Learn About VC Formal Apps: Functional Safety (FuSa)
                                                  Synopsys VC Formal FuSa app accelerates functional safety verification by performing structural analysis, formal observability, controllability and detectability analysis to prune away safe faults, and accurately identify dangerous faults.
                                                  Video Player is loading.
                                                  Current Time 0:00
                                                  Duration 0:00
                                                  Loaded: 0%
                                                  Stream Type LIVE
                                                  Remaining Time 0:00
                                                   
                                                  1x
                                                    • Chapters
                                                    • descriptions off, selected
                                                    • captions off, selected

                                                        Functional Safety (FuSa)

                                                        Functional safety verification is an essential requirement for automotive SoC and IP designs. This App formally identifies and classifies faults based on observability or detectability criteria. Complementing fault simulation with Z01X™, the combined solution reduces the effort and time required to achieve the test coverage closure and meet functional safety objectives.

                                                        Resources

                                                        Quick Tasks

                                                        Support and Training

                                                        SolvNetPlus

                                                        Explore the Synopsys Support Community! Login is required.

                                                        SNUG

                                                        Erase boundaries and connect with the global community.