Generation of Assertions from Connectivity Spec using IDS-Integrate

Ravi Kumar

In IDS-Integrate, users can easily input instructions using TCL or Python . The tool automatically generates assertions that focus on key connectivity aspects like ad-hoc connections, bus aggregations, bridge connections. With a special output feature called “formal,” users can create detailed assertions specifically for integrated circuits.

For example, consider creating assertions for the connectivity of bus aggregation logic in an SoC. Suppose there is an APB bus at the top or wrapper block, sending signals to four different child blocks. The assertions generated will ensure that the bus aggregation logic works correctly within the design. Users can further customise and expand these assertions to fit the specific needs of their SoC design.

This approach simplifies the process, allowing users to ensure their designs are reliable and efficient with ease.

Input: Shown below  is a python  script for setting up and generating a System-on-Chip (SoC) design. This script creates a simple SoC design with a top-level “chip” block and a child “block_inst”. It connects the two using an APB bus and generates the design files needed for both implementation and formal verification.

soc_clean()
soc_set("debug")
soc_create(      name="block", bus="apb")
soc_create("top",name="chip",  bus="apb")
soc_add(parent="chip", name="block", inst="block_inst" )
soc_connect(source="chip", dest="block_inst",bus="apb" )
soc_generate("compact",out=["sv","arv_formal"],dir="formal_s")

Output – It will generate the following files –

  1. sv
  2. formal.sv
  3. sv
  4. sv
  5. formal.sv

block.sv –  The block module is designed to interface with a bus, handling communication between the bus and the internal logic of the block.

module block #(
        //parameter declaration
    )(
    //input output port declaration of bus
    );
endmodule

chip.formal.sv – The primary purpose of this file is to verify the connectivity between the top-level module and the block instance (block_inst). By asserting these connections, the designer ensures that the BUS signals from the top-level module are correctly passed down to the block_inst. This is crucial for ensuring that the communication between the two modules works as intended.

module chip_ids_assert #(
//parameter decelaration
   )(
//input deceleration of BUS signals
    );
clocking cb @(posedge pclk);
    property block_connection_check1;
      pclk |-> block_inst.pclk;
    endproperty
property block_connection_check2;
       paddr |-> block_inst.paddr;
    endproperty
    property block_connection_check12;
       pslverr |->block_inst.pslverr;
    endproperty
endclocking
block_connection_check1_assert : assert property(cb.block_connection_check1);
block_connection_check2_assert : assert property(cb.block_connection_check2);
   block_connection_check12_assert : assert property(cb.block_connection_check12);
endmodule

Clocking Block – This module checks and asserts the correct connection of BUS signals between a chip and its block instance using SystemVerilog assertions.

Properties – This module verifies that all APB signals between a chip and its block instance are correctly connected by using SystemVerilog assertions to ensure proper signal routing.

Assertions – This module uses assertions to verify that each BUS signal in the block instance  correctly matches the corresponding signal in the chip during simulation.

chip.sv – This file defines a chip module that instantiates a block module, passing BUS signals between them. It serves as a top-level wrapper that connects the chip’s inputs and outputs to the corresponding signals in the block instance.

`include "block.sv"
module chip #(
//parameter deceleration
)(
    //input & output port deceleration of bus signals
);
block block_inst(
//mapping of bus signals from child to parent
);
endmodule

chip_top_onespin.sv – This file binds assertions to the chip module to verify its signal connections during formal verification.

`include "chip.sv"
`include "chip.formal.sv"
module chip_onespin;
      bind chip chip_ids_assert chip_assert (.*);
endmodule

chip1_cover.formal.sv – This module defines assertions to verify that signals in the block_inst are correctly connected and match the expected values during simulation. Each property checks a specific signal connection, and assertions ensure these properties hold true.

module chip_ids_assert #(
//parameter declaration
    )(
//port deceleration of BUS signals
    );
clocking cb @(posedge pclk);
    property block_connection_check1;
       block_inst.pclk == pclk;
    endproperty
    property block_connection_check12;
       block_inst.pslverr == pslverr;
    endproperty
endclocking
   block_connection_check1_assert : assert property(cb.block_connection_check1);
    block_connection_check1_cover  : cover  property(cb.block_connection_check1);
    block_connection_check12_assert : assert property(cb.block_connection_check12);
endmodule

Conclusion 

In summary, the use of IDS-Integrate significantly enhances the verification process for complex ASIC designs. IDS-Integrate simplifies connectivity validation by automatically generating assertions that verify the correct routing and behaviour of signals between various blocks in an SoC design.

These tools streamline the verification workflow, improving design reliability and efficiency by detecting issues early and automating complex checks.

 

Scroll to Top