Formal Verification through ARV-Formal™

Introduction

As the ASICs are getting larger and more complex, the netlist simulation is becoming a veritably time-consuming process, and it isn’t worth running weeks of netlist simulations corresponding to a veritably small change in RTL just to make sure that the netlist is good. Formal verification provides a solution to overcome this issue. Formal verification is a fashion used in different stages in the ASIC design life cycle in frontal-end verification, Logic Synthesis, Post Routing Checks, and for ECOs. The formal verification ways used for RTLs behavior validation are unique and more important than other verification techniques.

ARV-Formal™ is a tool developed by Agnisys Inc. for verifying RTLs without running simulation again and again after any minor changes in the RTL. There are different formal techniques such as “Formal Equivalence Checking” and “Formal Property Checking”. ARV-Formal focuses on the “Property Checking” technique as highlighted in below diagram: 

ARV-Formal™ has the capability to quickly validate the behavior of the design by generating assertions automatically corresponding to the specification of IP and provides bounded validation proof too, in some cases where it may be difficult to prove property. It also allows users to have automatic parameterized formal checks that focus on specific problems with targeted assertions, aiming to reduce debugging time. A formal block-level verification as a replacement for simulation of a block-level IP aims to prove the correctness of the system architecture for specific requirements such as cache coherence or avoiding deadlock conditions. ARV-Formal hides much of the technological complexity of validation that underpins formal verification, so the user does not need to be even semi-expert in the validation technique itself.

With the ability to parse register specifications from different supported input formats like IP-XACT, System RDL, RALF, Custom CSV, IDS Word, and IDS Excel, and facilitate a methodology where multiple teams can align and work from a golden specification for auto-generating:

·       System Verilog properties and assertions to check the register access policies.

·       Top-level file to bind DUT.

·       Verification plan to verify formal results.

·       Executable scripts.

ARV-Formal™ is developed to provide the types of assertions that are now widely used accompaniments to simulation. Designers bind assertions into their code to represent how a block is used and find violations of particular conditions. For example, an assertion may check that an acknowledgment signal follows a request after no more than ten clock cycles. Although the assertions create a learning environment, they are still easier to capture and use than bared mathematical expressions.

Focused Formal Verification:

Below are examples where formal verification techniques work for a better verification process in the Verification domain.

Clock domain crossing (CDC) is one of the applications of formal techniques that has been with us for a long time, but the proliferation of clocks in today’s SoCs has seen it rise from a low to a high-priority issue. RTL designs having a few clocks might have been addressed in simulation while those that now have hundreds of clocks are best verified in this respect beforehand. Formal model checking is run to verify the auto-generated synchronizer protocol assertions by ARV-Formal™, using the generated formal verification setup and script. The CDC protocol generation utility generates the formal compile and runs scripts. Automated formal setup significantly reduces the effort required to set up the design for formal analysis and avoids the debug effort to resolve incomplete or incorrect setup issues.

X-propagation is another application of formal verification techniques and suitable data that presents design issues for simulation. More complex RTL designs have a tendency to throw out more unknown states, this leads to miss bugs being identified. Linting tools to detect some of these issues. Agnisys Inc. is working on a combination of formal techniques that can be used to exhaustively prove whether Xs in the design are unreachable or will not have an impact on the correct operation of the logic. Techniques vary in so many flavors but in the unique and main, they get separated into automatic property checking methods to prove and validate the absence of X in the RTL design, or there is no registering with the X in it.

Summary:

ARV-Formal™ is a complete solution that takes the register specification and RTL design as input and performs formal proof to ensure all register operations conform to the specification. ARV-Formal is powered by an embedded version of (Jasper™ FPV App by Cadence Design System) to provide a one-button seamless process flow leveraging the power of modern formal verification tools. ARV-Formal automatically generates assertions directly from the specification therefore completely automating the setup and ensuring a very rapid return on investment.

Chip-in-Chip support for multiple input format

IDesignSpec^TM supports multiple design hierarchies like “chip”, and “block” to enable different architectural design flows.  A block can contain registers. A chip can contain other blocks and provide an aggregator for the blocks. 

A large SoC Design often requires multiple levels of hierarchies to place or group different block IP’s, so that these block hierarchies can be placed at different offsets in an address map or can even be on different address maps from both design and verification point of view. Chip-in-Chip hierarchy provides a functionality to aggregate the different block IP’s and address decoding at every level of hierarchy. 

To remove the limitation on the number of hierarchies over block level, chip-inside-chip is supported with input IDS-Word, IDS-Excel, IDS-NG, SystemRDL, IDS-Calc.

Now a chip can be a container for other chip hierarchies in addition to block hierarchies. 

Use Cases

Below diagram showing chip-in-chip hierarchy:

• Chip1 contains two elements “chip2”(chip element) and a “block1”(block Element).
• Chip2 contains “test_Block”(block element) with a repeat of two.

The property : “chip=true”

Chip-Inside-Chip flow is supported using the property “chip=true”. For example, in the case of a top chip, in IDS-Word specification having multiple chip(container) hierarchies, chips having property “chip=true” would be considered as chips .

IDSWord Example

IDS-Excel Example

IDS-NG Example

SystemRDL Example 

property chip { type = boolean; component = addrmap; };

addrmap Chip2 {

   chip=true;

   addrmap Chip1 {

     chip=true;

      addrmap Block1 {

       reg reg1 {

         field {

         sw=rw;

         hw=rw;

         }f1[31:0]=0;

       };

      reg1 reg1;

      };

      addrmap Block{

        reg reg2 {

         field {

         sw=rw;

         hw=rw;

         }f1[31:0]=0;

       };

       reg2 reg2;

      };

   Block1 Block1;

   Block2 Block2;

  };

  addrmap Block3 { 

       reg reg3 {

         field {

         sw=rw;

         hw=rw;

         }f1[31:0]=0;

       };

       reg3 reg3;

      };

 Chip1 Chip1;

 Block3 Block3;

 };

Conclusion – 

• IDesignSpec^TM supports chip-in-chip hierarchies, which means users can add chip inside chip along with block by using any IDS format like:- IDS-NG, IDS-Word, IDS-Excel, SystemRDL, IP-XACT etc. 
• For SystemRDL, users can use addrmap and apply “chip=true” property for each addrmap, on which they want to make a chip.
• And for other IDS input formats users need to use the reference of child chip as ref template and apply “chip=true” property on that template. Referred file can be any IDS input format. Also, this feature is supported for IDS output like:- RTL, UVM, Header, Documentation(HTML, PDF).

Tight Generator Interface support in SoC-E

Introduction

As per IP-XACT User Guide, IP-XACT defines an API called Tight Generator Interface (TGI) to query, modify, create, and delete IP-XACT XML documents. The standard defines this API in terms of SOAP (Simple Object Access Protocol) messages in order to make it programming language neutral.

The purpose of the TGI is to abstract from direct XML document manipulation and enable a client/server architecture between IP-XACT design tools and third-party TGI generators. 

The TGI uses the concept of handles to objects. Handles are called identifiers (IDs). Objects are entities that can be described in IP-XACT XML documents.

TGI in SoC-E

SoC-E also supports the TGI API for IPs described in IP-XACT XML documents. In SoC-E using these APIs users can access, modify, delete and create design data according to their own requirements.

Example

TGI API can be used together with SoC-E API and IDS TCL API for querying, creating or modifying design data available in SoC-E.

An example tcl script for TGI is as below:

soc_read -search_path “input-dir” -file { block1.ipxact.xml , block2.ipxact.xml } 

# Get ID for the component with the given VLNV and add alternate register in          memory map

set compID1 [ tgi::getID { “Agnisys_Inc.” “Agnisys_Inc.” “block1_model” “1.0” } ]

set compID2 [ tgi::getID { “Agnisys_Inc.” “Agnisys_Inc.” “block2_model” “1.0” } ]

set memMapList [  tgi::getComponentMemoryMapIDs $compID1 ]

set memMapElements [ tgi::getMemoryMapElementIDs $memMapList ]

  foreach y $memMapElements {         

    set regList [ tgi::getAddressBlockRegisterIDs $y ]

     foreach z $regList {

      set AltReg [ tgi::addRegisterAlternateRegister $z “Altr1” “AltGroup1”]

}

    }

}

# Create TOP container using soc_create API

soc_create -type block -name Top_chip -bus ahb -top

# Add apb bus in block using soc_add API

soc_add -type buses -target $compID1 -bus apb 

soc_add -type buses -target $compID2 -bus apb 

# Add blocks in TOP chip using soc_add API and  read blocks using $compID1 and $compID2 TGI

soc_add -type block -target Top_chip -name $compID1 -inst  “${compID1}_inst”

soc_add -type block -target Top_chip -name $compID2 -inst  “${compID2}_inst”

# Connect blocks in TOP chip using soc_connect API

soc_connect -dest Top_chip -source_inst “${compID1}_inst” -bus apb

soc_connect -dest Top_chip -source_inst “${compID2}_inst” -bus apb

# Using soc_savegraph API we can save graph in tex format

soc_savegraph -name “graph0.nlv” -dir “ids”

# soc_generate API are used to generate output 

soc_generate -out {v,sv} -dir ids

#This API is used to show graph

soc_graph  Top_chip

Schematic View

In this example an IP-XACT component is read into SoC-E using soc_read API. TGI API is used to get the handle of the IP-XACT component, adding an apb bus to that component and instantiating the component in a container block named Top_chip. The instance name of the component is  block1_model_inst and block2_model_inst. The container block, Top_chip, is created using soc_create API. Then, the block1_model_inst and block2_model_inst block is connected to Top_chip using an apb bus as shown in the above graph.

Conclusion

With the above feature of TGI in SOC-E, users will be able to access and manipulate IP-XACT XML documents according to their requirements. Users can also access, modify, create and delete documents using TGI rather than generate different IP-XACT XML documents for different requirements. 

Tool Qualification Kit for Functional Safety Compliance

Introduction

With growing advancements in hardware designs, the complexity of designs has increased multiple folds and brought great challenges to the lifecycle of quality management, development, validation, verification, and production. Applications, especially in the automotive industry, avionics, and space programs, have also increased the need for functional safety assurance of these complex designs to a great extent. These applications have high requirements for functional safety because the consequences of failure could lead to damage, injury, or loss of life. The risk of system (hardware and software) malfunction must be measured and thus minimized.

The Tool Qualification Kit (TQK) is an exclusive pre-qualification kit provided by Agnisys for its IDesignSpec™ tool suite to users embarking on a functionality safe design and not worrying on adding any additional measures for safety compliance on their design development processes involving this EDA tool suite.

Standard Safety Compliance

There are industry standards that provide laid-down guidance for developers to assess risks and develop appropriate measures so that the development cycle systems continue to operate safely even when failures occur. For electrical and electronic vehicular applications, ISO 26262 is the primary standard.

Part of applying ISO 26262 to the IP and system-on-chip (SoC) development process is qualifying the electronic design automation (EDA) tools used. This can place a heavy burden on the users, so tool vendors should do as much of the work as possible by providing products and flows that meet the stringent qualification requirements of the standard. The complete Agnisys IDesignSpec™ Suite of products has been certified by the internationally recognised testing organization.

IDesignSpec™ tool suite has achieved the stringent tool qualification criteria defined in ISO 26262. The Tool Suite is classified as a T2-offline-tool, suitable to be used in safety-related development according to IEC 61508. The certification means that IP and SoC developers only have to qualify the tool for its safety compliance through the mandatory TQK (tool qualification kit) to integrate it in their development flow. 

Tool Qualification Kit (TQK) details

Agnisys provides the ISO 26262 Tool Qualification Kit (TQK) for the pre-qualification of the complete suite of IDesignSpec (IDS™) software products. This mandatory kit is crafted for customers embarking on a functionally safe design to ensure the safety qualification of the Agnisys Tools at their end before actually using them in their development cycle. The kit consists of the following items to serve its purpose –

1. Tool download links with their checksum to detect transmission errors, if any.
2. The Safety Manual is a complete guide for customers to get started. Customers are expected to follow the guidelines and recommendations in this manual when working on functionally safe designs.
3. Release Notes for an overview of the latest feature enhancements and fixes in the tool with their traceable IDs.
4. A validation kit, which further consists of :

1. Agnisys Kitchen Sink (AKS) which is an all-encompassing design sample with various supported and approved structures and properties that are found to be functionally safe by Agnisys, Users can plug and use AKS components in their design structures based on their specifications and needs.
2. Test scenarios with their RUN commands/generation configuration and the expected static results for users to compare and ensure correct and expected tool behavior.
3. Verification reports of static files such as bridges that will be used in the design. 
4. Regression log for the release version to ensure backward compatibility.
5. List of known issues as waiver scenarios in the FS release.

Conclusion

For users seeking a functionally safe release for any of the IDesignSpec suite of tools, following the TQK will provide them with a clear set of actions and expectations to ensure industry standard functional safety in their created designs. This kit guarantees the capability to convert the design specification to functional safe code, provided the customer adheres to the ISO26262/IEC61508 standards for developing their specifications in accordance with the mentioned standards.