3-D chip design strategy

It is clear from previous discussions that with the ever increasing chip complexity and functionalities interconnect delay problems are going to be worse in very deep submicron technology. 3-D IC (or interconnect) technologies such as wire-bonding, micro-bumps, through-vias, and contact less interconnect are promising solution for interconnect delay concerns. This technique helps in effective large scale integration of different systems on a single IC.

3-D IC design architecture consists of a number of blocks which are divided from a 2-D chip(s). Different silicon layers are stacked one above the other and different blocks are placed on different layers, known as “tier”. Multiple layer of interconnects can be constructed in each Si tier. These interconnects are linked by vertical interconnects. By routing vertical interconnects appropriately long wire length can be shortened. Multiple active routing layers enhances the options to place the critical path components close to each other thereby decreasing RC delay and significantly improve performance of the design. Global interconnects are made common to all layers. Long wire inter-block communication delay is eliminated by placing these blocks in different layers and connecting them by a vertical interconnect. Thus system design becomes flexible with 3-D IC architecture. Three-dimensional integration can reduce the wiring and hence reduce the capacitance, power dissipation, and chip area and therefore improve overall performance of the chip.

The powerful advantage of 3-D chip design methodology can be exploited to build System on Chips (SoCs). Circuits with different voltage and performance requirements such as digital and analog components in the mixed-signal systems can be placed in different layers as shown in the Figure (1).

Figure (1) Block representation of 3-D IC [5]

Blocks are placed in different layers have lesser electromagnetic interference noise. This can achieve better noise performance of the intended design. High performance SoCs requires synchronous clock distribution. At the topmost layer of the 3-D IC optical interconnects and I/Os can be employed to achieve this.

Reference

[1] Kaustav Banerjee, Shukri J. Souri, Pawan Kapur, And Krishna C. Saraswat, 3-D ICs: A Novel Chip Design for Improving Deep-Submicrometer Interconnect Performance and Systems-on-Chip Integration, Proceedings Of The IEEE, pp.602-633,Vol. 89, NO. 5, May 2001, 0018–9219/01, 2001, IEEE

[2] Kaustav Banerjee, Shukri J. Souri, Pawan Kapur and Krishna C. Saraswat, 3-D Heterogeneous ICs: A Technology for the Next Decade and Beyond, 5th IEEE Workshop On Signal Propagation On Interconnects, Venice, Italy May, 13-16, 2001

[3] Jason Cong, An Interconnect-Centric Design Flow for Nanometer Technologies, Proceedings of the IEEE, pp.505-528, VOL. 89, No. 4, April 2001, 0018–9219/01,2001 IEEE

[4] Sungjun Im, Navin Srivastava, Kaustav Banerjee, and Kenneth E. Goodson, Thermal Scaling Analysis of Multilevel Cu/Low-k Interconnect Structures in Deep Nanometer Scale Technologies, Proceedings of the 22nd International VLSI Multilevel Interconnect Conference (VMIC), Oct. 3 - 6, Fremont, CA, pp. 525-530, 2005.

[5] Demystifying 3D ICs: The pros and cons of going vertical, http://www.ece.ncsu.edu/muse/papers/dtoc2005.pdf, 9/5/2007

Related Articles

• Introduction to Interconnect Technologies
• Limitations of the existing interconnect technologies
• Limits of Cu/low-k interconnects
• Vertical Interconnect Technologies
• Advantages of 3-D IC technologies

Read the rest of this article >>

Limits of Cu/low-k interconnects

At submicron level of 250 nm copper with low-k dielectric was introduced to decrease affects of increasing interconnect delay. But below 130 nm technology node interconnect delays are increasing further despite of introducing low-k dielectric. As the scaling increases new physical and technological effects like resistivity and barrier thickness start dominating and interconnect delay increases. Introduction of repeaters to shorten the interconnect length increases total area. The vias connecting repeaters to global layers can cause blockage in lower metal layers. Thus as the technology improves material limitations will dominate factor in the interconnect delay. Increasing metal layer width will cause increase in metallization layer. This can’t be a solution for the problem as it increases complexity, reliability and cost.

Cu low-k dielectric films are deposited by a special process known as Damascene process. Adhesion property of Cu with dielectric materials is very poor. Under electric bias they easily drift and cause short between metal layers. To avoid this problem a barrier layer is deposited between dielectric and Cu trench. Even though it decreases effective cross section of interconnects compared to drawn dimensions, it improves reliability. The barrier thickness becomes significant in deep submicron level and effective resistance of the interconnect rises further. In addition to this increasing electron scattering and self heating caused by the electron flow in interconnects due to comparable increase in internal chip temperature also contribute to increase interconnect resistance.

Related Articles

• Introduction to Interconnect Technologies
• Limitations of the existing interconnect technologies
• 3-D chip design strategy
• Vertical Interconnect Technologies
• Advantages of 3-D IC technologies

Read the rest of this article >>

Limitations of the existing interconnect technologies

Performances of deep sub micron ICs are limited by increasing interconnect loading affect. Long global clock networks account for the larger part of the power consumption in chips. Traditional CAD design methodologies are largely affected by the interconnect scaling. Capacitance and resistance of interconnects have increased due to the smaller wire cross sections, smaller wire pitch and longer length. This has resulted in increased RC delay. As technology is advancing scaling of interconnect is also increasing. In such scenario increased RC delay is becoming major bottleneck in improving performance of advanced ICs.

Figure (1) Gate and interconnect delays Vs technology nodes [1]

This problem is illustrated in Figure (1).

Here the gate delay and the interconnect delay are shown as functions of various technology nodes ranging from 180nm to 60nm. The interconnect delays shown assumes a line where repeaters are connected optimally and includes the delay due to the repeaters. From the graph it can be observed that with the shrinking of technology gate delay reduces but interconnect delay increases.

Reference

[1] Kaustav Banerjee, Shukri J. Souri, Pawan Kapur, And Krishna C. Saraswat, 3-D ICs: A Novel Chip Design for Improving Deep-Submicrometer Interconnect Performance and Systems-on-Chip Integration, Proceedings Of The IEEE, pp.602-633,Vol. 89, NO. 5, May 2001, 0018–9219/01, 2001, IEEE

[2] Kaustav Banerjee, Shukri J. Souri, Pawan Kapur and Krishna C. Saraswat, 3-D Heterogeneous ICs: A Technology for the Next Decade and Beyond, 5th IEEE Workshop On Signal Propagation On Interconnects, Venice, Italy May, 13-16, 2001

[3] Jason Cong, An Interconnect-Centric Design Flow for Nanometer Technologies, Proceedings of the IEEE, pp.505-528, VOL. 89, No. 4, April 2001, 0018–9219/01,2001 IEEE

[4] Sungjun Im, Navin Srivastava, Kaustav Banerjee, and Kenneth E. Goodson, Thermal Scaling Analysis of Multilevel Cu/Low-k Interconnect Structures in Deep Nanometer Scale Technologies, Proceedings of the 22nd International VLSI Multilevel Interconnect Conference (VMIC), Oct. 3 - 6, Fremont, CA, pp. 525-530, 2005.

[5] Demystifying 3D ICs: The pros and cons of going vertical, http://www.ece.ncsu.edu/muse/papers/dtoc2005.pdf, 9/5/2007

Related Articles

• Introduction to Interconnect Technologies
• Limits of Cu/low-k interconnects
• 3-D chip design strategy
• Vertical Interconnect Technologies
• Advantages of 3-D IC technologies

Read the rest of this article >>

Introduction to Interconnect Technologies

Interconnects are dominating in deep sub micron level VLSI design due to decreasing wire pitch. Increased complexities of circuits die size are also increasing. Planar 2-D ICs may not fulfill the requirement of heterogeneous integration of different technologies in single IC. As technology nodes advanced below 250nm, interconnect delays started dominating heavily. The introduction of Cu/low-k interconnects provided lesser resistivity and hence reduced delay. But in deep submicron domain (bellow 130 nm) even these interconnects added considerable delay due to increased resistivity owing several material limitations. [1-4]. Interconnected related problems like increased delay and power consumption are tackled by 3-D ICs which shorten the total interconnect length. [1][5].This part of the article series discusses these issues mainly based on reference [1].

Reference

[1] Kaustav Banerjee, Shukri J. Souri, Pawan Kapur, And Krishna C. Saraswat, 3-D ICs: A Novel Chip Design for Improving Deep-Submicrometer Interconnect Performance and Systems-on-Chip Integration, Proceedings Of The IEEE, pp.602-633,Vol. 89, NO. 5, May 2001, 0018–9219/01, 2001, IEEE

[2] Kaustav Banerjee, Shukri J. Souri, Pawan Kapur and Krishna C. Saraswat, 3-D Heterogeneous ICs: A Technology for the Next Decade and Beyond, 5th IEEE Workshop On Signal Propagation On Interconnects, Venice, Italy May, 13-16, 2001
[3] Jason Cong, An Interconnect-Centric Design Flow for Nanometer Technologies, Proceedings of the IEEE, pp.505-528, VOL. 89, No. 4, April 2001, 0018–9219/01,2001 IEEE
[4] Sungjun Im, Navin Srivastava, Kaustav Banerjee, and Kenneth E. Goodson, Thermal Scaling Analysis of Multilevel Cu/Low-k Interconnect Structures in Deep Nanometer Scale Technologies, Proceedings of the 22nd International VLSI Multilevel Interconnect Conference (VMIC), Oct. 3 - 6, Fremont, CA, pp. 525-530, 2005.
[5] Demystifying 3D ICs: The pros and cons of going vertical, http://www.ece.ncsu.edu/muse/papers/dtoc2005.pdf, 9/5/2007

Related Articles

• Limitations of the existing interconnect technologies
• Limits of Cu/low-k interconnects
• 3-D chip design strategy
• Vertical Interconnect Technologies
• Advantages of 3-D IC technologies
  

Read the rest of this article >>

Routing

Routing flow is shown in the Figure (1).



Figure (1) Routing flow [1]

Routing is the process of creating physical connections based on logical connectivity. Signal pins are connected by routing metal interconnects. Routed metal paths must meet timing, clock skew, max trans/cap requirements and also physical DRC requirements.

In grid based routing system each metal layer has its own tracks and preferred routing direction which are defined in a unified cell in the standard cell library.

There are four steps of routing operations:

1. Global routing
2. Track assignment
3. Detail routing
4. Search and repair

Global Route assigns nets to specific metal layers and global routing cells. Global route tries to avoid congested global cells while minimizing detours. Global route also avoids pre-routed P/G, placement blockages and routing blockages.

Track Assignment (TA) assigns each net to a specific track and actual metal traces are laid down by it. It tries to make long, straight traces to avoid the number of vias. DRC is not followed in TA stage. TA operates on the entire design at once.

Detail Routing tries to fix all DRC violations after track assignment using a fixed size small area known as “SBox”. Detail route traverses the whole design box by box until entire routing pass is complete.

Search and Repair fixes remaining DRC violations through multiple iterative loops using progressively larger SBox sizes.

Reference

[1] Astro User Guide, Version X-2005.09, September 2005


Related Articles

• Physical Design Flow
• Libraries
• Inputs–outputs from physical design process
• Floor Planning
• Power Planning
• Timing Analysis in Physical Design
• Placement
• Clock Tree Synthesis (CTS)

Read the rest of this article >>

Clock Tree Synthesis (CTS)

The goal of CTS is to minimize skew and insertion delay. Clock is not propagated before CTS as shown in Figure (1).





Figure (1) Ideal clock before CTS

After CTS hold slack should improve. Clock tree begins at .sdc defined clock source and ends at stop pins of flop. There are two types of stop pins known as ignore pins and sync pins. ‘Don’t touch’ circuits and pins in front end (logic synthesis) are treated as ‘ignore’ circuits or pins at back end (physical synthesis). ‘Ignore’ pins are ignored for timing analysis. If clock is divided then separate skew analysis is necessary.

Global skew achieves zero skew between two synchronous pins without considering logic relationship.

Local skew achieves zero skew between two synchronous pins while considering logic relationship.

If clock is skewed intentionally to improve setup slack then it is known as useful skew.

Rigidity is the term coined in Astro to indicate the relaxation of constraints. Higher the rigidity tighter is the constraints.

In Clock Tree Optimization (CTO) clock can be shielded so that noise is not coupled to other signals. But shielding increases area by 12 to 15%. Since the clock signal is global in nature the same metal layer used for power routing is used for clock also. CTO is achieved by buffer sizing, gate sizing, buffer relocation, level adjustment and HFN synthesis. We try to improve setup slack in pre-placement, in placement and post placement optimization before CTS stages while neglecting hold slack. In post placement optimization after CTS hold slack is improved. As a result of CTS lot of buffers are added. Generally for 100k gates around 650 buffers are added.

Global skew report is shown below.

**********************************************************************
*
* Clock Tree Skew Reports
*
* Tool : Astro
* Version : V-2004.06 for IA.32 -- Jul 12, 2004
* Design : sam_cts
* Date : Sat May 19 16:09:20 2007
*
**********************************************************************


======== Clock Global Skew Report =============================

Clock: clock
Pin: clock
Net: clock

Operating Condition = worst
The clock global skew = 2.884
The longest path delay = 4.206
The shortest path delay = 1.322

The longest path delay end pin: \mac21\/mult1\/mult_out_reg[2]/CP
The shortest path delay end pin: \mac22\/adder1\/add_out_reg[3]/CP



The Longest Path:
====================================================================
Pin Cap Fanout Trans Incr Arri Master/Net
--------------------------------------------------------------------
clock 0.275 1 0.000 0.000 r clock
U1118/CCLK 0.000 0.000 0.000 r pc3c01
U1118/CP 3.536 467 1.503 1.124 1.124 r n174
\mac21\/mult1\/mult_out_reg[2]/CP
4.585 3.082 4.206 r sdnrq1
[clock delay] 4.206
====================================================================



The Shortest Path:
====================================================================
Pin Cap Fanout Trans Incr Arri Master/Net
--------------------------------------------------------------------
clock 0.275 1 0.000 0.000 r clock
U1118/CCLK 0.000 0.000 0.000 r pc3c01
U1118/CP 3.536 467 1.503 1.124 1.124 r n174
\mac22\/adder1\/add_out_reg[3]/CP
1.701 0.198 1.322 r sdnrq1
[clock delay] 1.322
====================================================================






Figure (2) Clock after CTS and CTO


Related Articles

• Physical Design Flow
• Libraries
• Inputs–outputs from physical design process
• Floor Planning
• Power Planning
• Timing Analysis in Physical Design
• Placement
• Routing
  

Read the rest of this article >>

Placement

Complete placement flow is illustrated in Figure (1).



Figure (1) Placement flow [1]

Before the start of placement optimization all Wire Load Models (WLM) are removed. Placement uses RC values from Virtual Route (VR) to calculate timing. VR is the shortest Manhattan distance between two pins. VR RCs are more accurate than WLM RCs.

Placement is performed in four optimization phases:

1. Ire-placement optimization
2. In placement optimization
3. Post Placement Optimization (PPO) before clock tree synthesis (CTS)
4. PPO after CTS.

Pre-placement Optimization optimizes the netlist before placement, HFNs are collapsed. It can also downsize the cells.

In-placement optimization re-optimizes the logic based on VR. This can perform cell sizing, cell moving, cell bypassing, net splitting, gate duplication, buffer insertion, area recovery. Optimization performs iteration of setup fixing, incremental timing and congestion driven placement.

Post placement optimization before CTS performs netlist optimization with ideal clocks. It can fix setup, hold, max trans/cap violations. It can do placement optimization based on global routing. It re does HFN synthesis.

Post placement optimization after CTS optimizes timing with propagated clock. It tries to preserve clock skew.

Reference

[1] Astro User Guide, Version X-2005.09, September 2005


Related Articles

• Physical Design Flow
• Libraries
• Inputs–outputs from physical design process
• Floor Planning
• Power Planning
• Timing Analysis in Physical Design
• Clock Tree Synthesis (CTS)
• Routing

Read the rest of this article >>

Timing Analysis in Physical Design

Timing analysis at back end requires knowledge of all clock related constraints provided at front end. When .sdc file given to physical design tool (like Astro) its first object is to remove all Wire Load Models (WLM) which are used for front end timing analysis. In backend there is no term called as wire load model. Actual delays are calculated based on the RC value of metal layers. All RC values like sidewall, junction and fringe capacitances are stored as Table Look Up (TLU) format in technology file.

In backend design hold violation has higher priority compared to setup violation because hold violation is related to data path of the design. Setup violation can be eliminated by slowing down the clock.

Placement and routing goal is always to meet timing constraints provided by the .sdc file. If latency and uncertainty are not set for clock at front end then at backend doing Clock Tree Synthesis (CTS) is not possible.

Cell delay and net delay are stored as look up table.

Cell delay consists of transition, timing arcs and capacitances while net delay is constituted by RCs only. Cell delays are available in libraries

. Net delays are specified in technology files. (In front end it is in WLM). Cell delays are fixed. Net delays are not fixed and they depend on interconnect length and width. Net delay parameters Rnet and Cnet are available as Table Look Up (TLU) provided by the vendor.

There is one more set of file TLU+ which account for Ultra Deep Sub Micron (UDSM) effects. UDSM effects are not included in TLU file. A mapping file maps TLU to TLU+. UDSM effects like Optical Proximity Correction (OPC), Resumption Enhanced Technology (RET) and Litho Compliance Check (LCC) are not taken care by Astro. For the placement stage virtual RC (based on Manhattan distance) Layout Parasitic Extraction (LPE) mode is used. For CTS real R and virtual C is used and for routing Real RC is used.

Clock definition given to SAMM in front end design flow is generated as .sdc file from Design Compiler is given below. It includes clock frequency, rise and fall time, setup and hold, skew and insertion delay.

#####################################################
# Created by Design Compiler write_sdc on Fri May 11 18:35:45 2007
#####################################################
create_clock -period 4.85 -waveform {0 2.425} [get_ports {clock}]
set_clock_transition -rise 0.04 [get_clocks {clock}]
set_clock_transition -fall 0.04 [get_clocks {clock}]
set_clock_uncertainty 0.485 -setup [get_clocks {clock}]
set_clock_uncertainty 0.27 -hold [get_clocks {clock}]
set_clock_latency 0.45 [get_clocks {clock}]
set_clock_latency -source 0.45 [get_clocks {clock}]


Related Articles

• Physical Design Flow
  
• Libraries
  
• Inputs–outputs from physical design process
  
• Floor Planning
  
• Power Planning
  
• Placement
  
• Clock Tree Synthesis (CTS)
  
• Routing

Read the rest of this article >>

Power Planning

There are two types of power planning and management. They are core cell power management and I/O cell power management. In former one VDD and VSS power rings are formed around the core and macro. In addition to this straps and trunks are created for macros as per the power requirement. In the later one, power rings are formed for I/O cells and trunks are constructed between core power ring and power pads. Top to bottom approach is used for the power analysis of flatten design while bottom up approach is suitable for macros.

The power information can be obtained from the front end design. The synthesis tool reports static power information. Dynamic power can be calculated using Value Change Dump (VCD) or Switching Activity Interchange Format (SAIF) file in conjunction with RTL description and test bench. Exhaustive test coverage is required for efficient calculation of peak power. This methodology is depicted in Figure (1).

For the hierarchical design budgeting has to be carried out in front end. Power is calculated from each block of the design. Astro works on flattened netlist. Hence here top to bottom approach can be used. JupiterXT can work on hierarchical designs. Hence bottom up approach for power analysis can be used with JupiterXT. IR drops are not found in floor planning stage. In placement stage rails are get connected with power rings, straps, trunks. Now IR drops comes into picture and improper design of power can lead to large IR drops and core may not get sufficient power.

Figure (1) Power Planning methodology

Below are the calculations for flattened design of the SAMM. Only static power reported by the Synthesis tool (Design Compiler) is used instead of dynamic power.

• The number of the core power pad required for each side of the chip

= total core power / [number of side*core voltage*maximum allowable current for a I/O pad]

= 236.2068mW/ [4 * 1.08 V * 24mA] (Considering design SAMM)

= 2.278

~ 2

Therefore for each side of the chip 2 power pads (2 VDD and 2 VSS) are added.

• Total dynamic core current (mA)

= total dynamic core power / core voltage

= 236.2068mW / 1.08V

= 218.71 mA

• Core PG ring width

= (Total dynamic core current)/ (No. of sides * maximum current density of the metal layer used (Jmax) for PG ring)
=218.71 mA/(4*49.5 mA/µm)
~1.1 µm
~2 µm

• Pad to core trunk width (µm)

= total dynamic core current / number of sides * J_max where Jmax is the maximum current density of metal layer used

= 218.71 mA / [4 * 49.5 mA/µm]

= 1.104596 µm

Hence pad to trunk width is kept as 2µm.

Using below mentioned equations we can calculate vertical and horizontal strap width and required number of straps for each macro.

• Block current:

I_block= P_block / V_ddcore

• Current supply from each side of the block:

I_top=I_bottom= { I_block *[W_block / (W_block +H_block)] }/2

I_left=I_right= { I_block *[H_block / (W_block +H_block)] }/2

• Power strap width based on EM:

W_{strap_vertical} =I_top / J_metal

W_{strap_horizontal} =I_left / J_metal

• Power strap width based on IR:

W_{strap_vertical} >= [ I_top * R_oe * H_block ] / 0.1 * VDD

W_{strap_horizontal} >= [ I_left * R_oe * W_block ] / 0.1 * VDD

• Refresh width:

W_{refresh_vertical} =3 * routing pitch +minimum width of metal (M4)

W_{refresh_horizontal} =3 * routing pitch +minimum width of metal (M3)

• Refresh number

N_{refresh_vertical} = max (W_{strap_vertical} ) / W_{refresh_vertical}

N_{refresh_horizontal} = max (W_{strap_horizontal} ) / W_{refresh_horizontal}

• Refresh spacing

S_{refresh_vertical} = Wblock / N_{refresh_vertical}

S_{refresh_horizontal} = Hblock / N_{refresh_horizontal}

Figure (2) Showing core power ring, Straps and Trunks

Related Articles

• Physical Design Flow
• Libraries
• Inputs–outputs from physical design process
• Floor Planning
• Timing Analysis in Physical Design
• Placement
• Clock Tree Synthesis (CTS)
• Routing

Read the rest of this article >>

Floor Planning

Floor plan determines the size of the design cell (or die), creates the boundary and core area, and creates wire tracks for placement of standard cells. [1]. It is also a process of positioning blocks or macros on the die.

Floor planning control parameters like aspect ratio, core utilization are defined as follows:

Aspect Ratio= Horizontal Routing Resources / Vertical Routing Resources

Core Utilization= Standard Cell Area / (Row Area + Channel Area)

Total 4 metal layers are available for routing in used version of Astro. M0 and M3 are horizontal and M2 and M4 are vertical layers. Hence aspect ratio for SAMM is 1. Total number of cells =1645; total number of nets=1837 and number of ports (excluding 16 power pads) = 60. The figure depicting floor plan-die size (µm) of SAMM is shown beside.

Top Design Format (TDF) files provide Astro with special instructions for planning, placing, and routing the design. TDF files generally include pin and port information. Astro particularly uses the I/O definitions from the TDF file in the starting phase of the design flow. [1]. Corner cells are simply dummy cells which have ground and power layers. The TDF file used for SAMM is given below. The SAMM IC has total 80 I/O pads out of which 4 are dummy pads. Each side of the chip has 20 pads including 2 sets of power pads. Number of power pads required for SAMM is calculated in power planning section. Design is pad limited (pad area is more than cell area) and inline bonding (same I/O pad height) is used.

define _cell (geGetEditCell)

;create power pads

;Core power supply instantiation for left side

dbCreateCellInst (geGetEditCell) "" "pv0i.FRAM" "vss1left" "0" "NO" '(0.0 0.0) "sam3"

dbCreateCellInst (geGetEditCell) "" "pvdi.FRAM" "vdd1left" "0" "NO" '(0.0 0.0) "sam3"

dbCreateCellInst (geGetEditCell) "" "pv0i.FRAM" "vss2left" "0" "NO" '(0.0 0.0) "sam3"

dbCreateCellInst (geGetEditCell) "" "pvdi.FRAM" "vdd2left" "0" "NO" '(0.0 0.0) "sam3"

;Core power supply instantiation for top side

dbCreateCellInst (geGetEditCell) "" "pv0i.FRAM" "vss1top" "0" "NO" '(0.0 0.0) "sam3"

dbCreateCellInst (geGetEditCell) "" "pvdi.FRAM" "vdd1top" "0" "NO" '(0.0 0.0) "sam3"

dbCreateCellInst (geGetEditCell) "" "pv0i.FRAM" "vss2top" "0" "NO" '(0.0 0.0) "sam3"

dbCreateCellInst (geGetEditCell) "" "pvdi.FRAM" "vdd2top" "0" "NO" '(0.0 0.0) "sam3"

;Core power supply instantiation for right side

dbCreateCellInst (geGetEditCell) "" "pv0i.FRAM" "vss1right" "0" "NO" '(0.0 0.0) "sam3"

dbCreateCellInst (geGetEditCell) "" "pvdi.FRAM" "vdd1right" "0" "NO" '(0.0 0.0) "sam3"

dbCreateCellInst (geGetEditCell) "" "pv0i.FRAM" "vss2right" "0" "NO" '(0.0 0.0) "sam3"

dbCreateCellInst (geGetEditCell) "" "pvdi.FRAM" "vdd2right" "0" "NO" '(0.0 0.0) "sam3"

;Core power supply instantiation for bottom side

dbCreateCellInst (geGetEditCell) "" "pv0i.FRAM" "vss1bottom" "0" "NO" '(0.0 0.0) "sam3"

dbCreateCellInst (geGetEditCell) "" "pvdi.FRAM" "vdd1bottom" "0" "NO" '(0.0 0.0) "sam3"

dbCreateCellInst (geGetEditCell) "" "pv0i.FRAM" "vss2bottom" "0" "NO" '(0.0 0.0) "sam3"

dbCreateCellInst (geGetEditCell) "" "pvdi.FRAM" "vdd2bottom" "0" "NO" '(0.0 0.0) "sam3"

;dummy cell instantiation

dbCreateCellInst (geGetEditCell) "" "pc3t02.FRAM" "dummy1" "0" "NO" '(0.0 0.0) "sam3"

dbCreateCellInst (geGetEditCell) "" "pc3t02.FRAM" "dummy2" "0" "NO" '(0.0 0.0) "sam3"

dbCreateCellInst (geGetEditCell) "" "pc3t02.FRAM" "dummy3" "0" "NO" '(0.0 0.0) "sam3"

dbCreateCellInst (geGetEditCell) "" "pc3t02.FRAM" "dummy4" "0" "NO" '(0.0 0.0) "sam3"

dbCreateCellInst (geGetEditCell) "" "pc3t02.FRAM" "dummy5" "0" "NO" '(0.0 0.0) "sam3"

;corner cell instantiation

dbCreateCellInst (geGetEditCell) "" "pfrelr.FRAM" "cornerll" "270" "NO" '(10 10) "sam3"

dbCreateCellInst (geGetEditCell) "" "pfrelr.FRAM" "cornerlr" "0" "NO" '(10 10) "sam3"

dbCreateCellInst (geGetEditCell) "" "pfrelr.FRAM" "cornerul" "180" "NO" '(10 10) "sam3"

dbCreateCellInst (geGetEditCell) "" "pfrelr.FRAM" "cornerur" "90" "NO" '(10 10) "sam3"

tdfPurgePadConstr

;==================================

;pad placement for corner cells

;==================================

pad "cornerll" "bottom"

pad "cornerur" "top"

pad "cornerlr" "right"

pad "cornerul" "left"

;==================================

;pad(I/O) placement for left side

;==================================

pad "U1065" "left" 1 ;a_row0[0]

pad "U1064" "left" 2 ;a_row0[1]

pad "U1063" "left" 3 ;a_row0[2]

pad "U1062" "left" 4 ;a_row0[3]

pad "U1069" "left" 5 ;a_row1[0]

pad "U1068" "left" 6 ;a_row1[1]

pad "U1067" "left" 7 ;a_row1[2]

pad "vdd1left" "left" 8

pad "vss1left" "left" 9

pad "vdd2left" "left" 10

pad "vss2left" "left" 11

pad "U1066" "left" 12 ;a_row1[3]

pad "U1073" "left" 13 ;a_row2[0]

pad "U1072" "left" 14 ;a_row2[1]

pad "U1071" "left" 15 ;a_row2[2]

pad "U1070" "left" 16 ;a_row2[3]

pad "U1118" "left" 17 ;clock

pad "U1116" "left" 18 ;chip enable

pad "dummy1" "left" 19

pad "dummy2" "left" 20

;==================================

;pad(I/O) placement for top side

;==================================

pad "U1077" "top" 1 ;b_col0[0]

pad "U1076" "top" 2 ;b_col0[1]

pad "U1075" "top" 3 ;b_col0[2]

pad "U1074" "top" 4 ;b_col0[3]

pad "U1081" "top" 5 ;b_col1[0]

pad "U1080" "top" 6 ;b_col1[1]

pad "U1079" "top" 7 ;b_col1[2]

pad "vdd1top" "top" 8

pad "vss1top" "top" 9

pad "vdd2top" "top" 10

pad "vss2top" "top" 11

pad "U1078" "top" 12 ;b_col1[3]

pad "U1085" "top" 13 ;b_col2[0]

pad "U1084" "top" 14 ;b_col2[1]

pad "U1083" "top" 15 ;b_col2[2]

pad "U1082" "top" 16 ;b_col2[3]

pad "U1117" "top" 17 ;reset

pad "U1119" "top" 18 ;mult_over

pad "dummy3" "top" 19

pad "dummy4" "top" 20

;==================================

;pad(I/O) placement for right side

;==================================

pad "U1100" "right" 1 ;c_row1[5]

pad "U1101" "right" 2 ;c_row1[4]

pad "U1102" "right" 3 ;c_row1[3]

pad "U1103" "right" 4 ;c_row1[2]

pad "U1104" "right" 5 ;c_row1[1]

pad "U1105" "right" 6 ;c_row1[0]

pad "U1086" "right" 7 ;c_row0[9]

pad "vdd1right" "right" 8

pad "vss1right" "right" 9

pad "vdd2right" "right" 10

pad "vss2right" "right" 11

pad "U1087" "right" 12 ;c_row0[8]

pad "U1088" "right" 13 ;c_row0[7]

pad "U1089" "right" 14 ;c_row0[6]

pad "U1090" "right" 15 ;c_row0[5]

pad "U1091" "right" 16 ;c_row0[4]

pad "U1092" "right" 17 ;c_row0[3]

pad "U1093" "right" 18 ;c_row0[2]

pad "U1094" "right" 19 ;c_row0[1]

pad "U1095" "right" 20 ;c_row0[0]

;==================================

;pad(I/O) placement for bottom side

;==================================

pad "dummy5" "bottom" 1

pad "U1121" "bottom" 2 ;test_se

pad "U1106" "bottom" 3 ;c_row2[9]

pad "U1107" "bottom" 4 ;c_row2[8]

pad "U1108" "bottom" 5 ;c_row2[7]

pad "U1109" "bottom" 6 ;c_row2[6]

pad "U1110" "bottom" 7 ;c_row2[5]

pad "vdd1bottom" "bottom" 8;

pad "vss1bottom" "bottom" 9

pad "vdd2bottom" "bottom" 10

pad "vss2bottom" "bottom" 11

pad "U1111" "bottom" 12 ;c_row2[4]

pad "U1112" "bottom" 13 ;c_row2[3]

pad "U1113" "bottom" 14 ;c_row2[2]

pad "U1114" "bottom" 15 ;c_row2[1]

pad "U1115" "bottom" 16 ;c_row2[0]

pad "U1096" "bottom" 17 ;c_row1[9]

pad "U1097" "bottom" 18 ;c_row1[8]

pad "U1098" "bottom" 19 ;c_row1[7]

pad "U1099" "bottom" 20 ;c_row1[6]

;=======================================

If TDF is free from syntax errors and pins are properly numbered in consecutive steps then TDF will be read successfully and message will be displayed on scheme window.

Aspect ratio of 0.65 is set which means 65% of the core area is used for cells and remaining 35% is for routing. Since channel less row arrangement is desired for area optimization row to core ratio can be kept at 1. Rows should be arranged horizontal, they are flipped and abutted and thus double back arrangement should be enabled.

Floor planned cell

Floor planned cell is shown above and its related die size is shown first itself. All dimensions are in µm. The total die size is approximately 1.9sqmm.

Reference

[1] Astro User Guide,Version X-2005.09, September 2005

Related Articles

• Physical Design Flow
• Libraries
• Inputs–outputs from physical design process
• Power Planning
• Timing Analysis in Physical Design
• Placement
• Clock Tree Synthesis (CTS)
• Routing

Read the rest of this article >>

Inputs–outputs from physical design process

The inputs required for any physical design tool is summarized in Table (1) and the outputs generated from the same are listed in Table (2).

Data Input Requirements for Physical Design Tool

Table (1) Inputs to physical design tool

Table (2) Outputs from physical design tool

Reference

[1] Astro User Guide, Version X-2005.09, September 2005

Related Articles

• Physical Design Flow
• Libraries
• Floor Planning
• Power Planning
• Timing Analysis in Physical Design
• Placement
• Clock Tree Synthesis (CTS)
• Routing

Read the rest of this article >>

Libraries In Physical Design

Technology libraries are integral part of the ASIC backend EDA tools. Important two libraries are briefly explained below.

Technology File Libraries

Technology file defines basic characteristic of cell library pertaining to a particular technology node. They are units used in the design, graphical characteristics like colors, stipple patterns, line styles, physical parameters of metal layers, coupling capacitances, capacitance models, dielectric values, device characteristics, design rules. These specifications are divided into technology file sections.

Units for power, voltage, current etc are defined in technology section.

The color section defines primary and display colors that a tool uses to display designs in the library.

Stipple pattern are defined in stipple sections.

Different layer definitions like its current density, width etc are defined in layer section.

Fringe capacitances generated by crossing of interconnects are defined in fringe cap section.

Similarly several other specifications like metal density, design rules that apply to design in library, place and route (P&R) rules, slot rule, resistance model are defined in their respective sections.

Standard Cell Libraries, I/O Cell Libraries, Special Cell Libraries

A standard cell library is a collection of pre designed layout of basic logic gates like inverters, buffers, ANDs, ORs, NANDs etc.

All the cells in the library have same standard height and have varied width. These standard cell libraries are known as reference libraries in Astro.

These reference libraries are technology specific and are generally provided by ASIC vendor like TSMC, Artisan, IBM etc. Standard cell height for 130 TSMC process is 3.65 µM.

In addition to standard cell libraries, reference libraries contain I/O and Power/Ground pad cell libraries. It also contain IP libraries for reusable IP like RAMs, ROMs and other pre-designed, standard, complex blocks.

The TSMC universal I/O libraries include several power/ground cells that supply different voltages to the core, pre-drivers and post drivers. Internal pull-up or pull-down is provided to some cells in I/O libraries.

Reference

[1] Astro User Guide, Version X-2005.09, September 2005

Related Articles

• Physical Design Flow
• Inputs–outputs from physical design process
• Floor Planning
• Power Planning
• Timing Analysis in Physical Design
• Placement
• Clock Tree Synthesis (CTS)
• Routing

Read the rest of this article >>

Physical Design Flow

The physical design flow is generally explained in the Figure (1.). In each section of the flow EDA tools available from the two main EDA companies-Synopsys and Cadence is also listed. In each and every step of the flow timing and power analysis can be carried out. If timing and power requirements are not met then either the whole flow has to be re-exercised or going back one or two steps and optimizing the design or incremental optimization may meet the requirements

Related Articles

• Libraries
• Inputs–outputs from physical design process
• Floor Planning
• Power Planning
• Timing Analysis in Physical Design
• Placement
• Clock Tree Synthesis (CTS)
• Routing
  

Read the rest of this article >>

Formal Verification Example

Formality (from Synopsys) is the tool used to formally verify the design. The design SAMM is verified in two ways. Gate level netlist and testable netlist are formally verified. Gate level netlist in .db format is taken as reference and testable netlist in .db format is considered as implementation. The matching of these two netlists generates below log data:


*********************************** Matching Results ***********************************
498 Compare points matched by name
0 Compare points matched by signature analysis
0 Compare points matched by topology
27 Matched primary inputs, black-box outputs
0(1) Unmatched reference(implementation) compare points
0(2) Unmatched reference(implementation) primary inputs, black-box outputs
----------------------------------------------------------------------------------------
Unmatched Objects REF IMPL
----------------------------------------------------------------------------------------
Input ports (Port) 0 2
Output ports (Port) 0 1
****************************************************************************************


There are total two unmatched input ports exists in implementation. These ports are test_se and test_si which are related to Design for Test (DFT) scan circuit. Since under normal operation DFT circuits doesn’t come into picture tool has to be instructed not to match these ports. This is performed by setup option in Graphical User Interface (GUI) and setting those two signals as false as shown in below.

Formality (match)> setup
1
Formality (setup)> set_constant -type port i:/WORK/sam3/test_se 0
Set 'i:/WORK/sam3/test_se' to constant 0
1
Formality (setup)> set_constant -type port i:/WORK/sam3/test_si 0
Set 'i:/WORK/sam3/test_si' to constant 0
1



After setting these options designs match and verification succeeds. The log data of the same is shown below.


Status: Verifying...
********************************* Verification Results *********************************
Verification SUCCEEDED
----------------------
Reference design: r:/WORK/sam3
Implementation design: i:/WORK/sam3
480 Passing compare points
----------------------------------------------------------------------------------------
Matched Compare Points BBPin Loop BBNet Cut Port DFF LAT TOTAL
----------------------------------------------------------------------------------------
Passing (equivalent) 0 0 0 0 31 449 0 480
Failing (not equivalent) 0 0 0 0 0 0 0 0
Not Compared
Constant reg 18 0 18
****************************************************************************************
1


Similarly original verilog code and testable netlist is verified.

Related Articles

Introduction to Formal Verification
Why Formal Verification?
Concept of Formal Verification
Methodologies in Formal Verification
Binary Decision Diagram (BDD)
Equivalence Checking (EC)
Model Checking
Theorem Proving
Satisfiability (SAT) Solvers
Recent Advances in SAT Based Formal Verification
Hybrid Formal Verification Techniques Read the rest of this article >>

Hybrid Formal Verification Techniques

Traditional formal techniques like Model Checking and Theorem Proving are capable of analyzing and finding all bugs in a design. However, they suffer from several drawbacks due to which their applicability in practice is restricted. Model checking is limited by well known state explosion problem. For the effective use of theorem proving technique, highly knowledge and skillful manpower is necessary. In this context hybrid techniques where both formal and informal techniques are used in conjunction with each other are gaining more popularity. The general goal of a hybrid technique is to enhance coverage of the state space traversed in order to address the verification bottleneck, by using the strengths of individual methods.

Hybrid Formal Verification approaches is classified into four categories.

They are:

1. Methods combining formal and informal techniques
2. Combination of two formal techniques
3. Combination of two informal techniques
4. Combination of multiple verification approaches

Symbolic Model Verification (SMV) is a powerful method for Formal Verification but most of the realistic designs are too large and complex for pure symbolic simulation techniques. A method surveyed by [6] used concept of synthesis and verification. This hybrid technique achieved better coverage and quicker in finding bugs. One more hybrid technique which combines model checking and test generation, used general graph theoretic model, functional fault model and test generation procedures. This method is highly suitable for pipelined processors.

It is interesting to note that a number of research activities are going on in hybridization of ATPG and formal techniques. ATPGs avoid state explosion problem while formal methods are “complete”. Hybridization of these two strengthens the verification. In one of the method surveyed in [6], formal specifications (or properties) are used as input to the test generator. This method was quite successful in dealing with commercial designs. Another method combined both ATPG and BDD with the SMV. As noted by [6] results showed better coverage than either symbolic techniques or simulation in isolation. Several other hybrid techniques which combine ATPG, BDD and SMV can be found in [6].

Effectively combining two formal methods like theorem proving and model checking is a great challenge to research community. The experiment that combined “Symbolic Trajectory Evolution” (STE) with theorem proving method showed good results for the verification of 64-bit integer multiplier. Some other theorem proving methods that use external tools like ORACLE for checking formulas as theorem during proof search and they use ORACLE interface to decide Boolean formulas through connections to BDD and SAT solving libraries.

Another tool, MIST, surveyed by [6] hybridizes two model checking techniques. The technique enables an interface between STE and SMC-BDD or SAT based solvers. In this technique, once the initial set of states is obtained by using STE, SMC is used to check the property on the original circuit model. Thus the model MIST enhances both the capacity and performance of SMC. The method helps the debugging process by letting the verifier focus on critical and error prone areas.

Various other methods combining informal methods are also emerging. One among them employs “computer learning” and “Bayesian Networks” and couple of others use model based randomized functional verification.

The first proposed method combining multiple verification approaches used test pattern generation, no-reachability analysis, symbolic simulation, SAT based BMC, symbolic fix point computation and automatic abstraction. These techniques helped to focus coverage issues much earlier in the design cycle, to expose bugs in deep circuit blocks.

Hybrid Formal Verification techniques are employed in commercial tools like Megellan, Formality by Synopsys; Incissive by Cadence; FormalPro by Mentor Graphics.

Reference

[1] Sandeep K. Shukla, “An Introduction to Formal Verification”, http://www.ics.uci.edu/~rgupta/ics212/w2002/verification.pdf, 9/10/07

[2] Rolf Drechsler, “Towards Formal Verification on the System Level”, Institute of Computer Science, University of Bremen, Germany, 2005

[3] Prof. Eduard Cerny, Xiaoyu Song, “Formal Verification Methods”, University of Montrial, Canada, 1999. http://www.iro.umontreal.ca/~cerny/IFT6222/1-intro-99.0808.pdf, 9/10/07

[4] Jawahar Jain, Amit Narayan, M.Fujita, A.Sangiovanni Vincentelli, “A Survey of Techniques for Formal Verification of Combinational Circuits”, Proceedings of the 1997 International Conference on Computer Design (ICCD '97), IEEE, 1997

[5] F. Wang, “Formal Verification of Timed Systems: A Survey and Perspective”, Proceedings of the IEEE, Vol. 92, No. 8, August 2004. pp.283-1305. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[6] J. Bhadra, M. S. Abadir, L.-C. Wang, S. Ray, “Functional Verification through Hybrid Techniques: A Survey”, journal of IEEE Design & Test of Computers, March-April 2007. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[7] M. Prasad, A. Biere, A. Gupta, “A Survey of Recent Advances in SAT-Based Formal Verification”, Software Tools for Technology Transfer, Vol. 7, No. 2, 2005. pp. 156-173. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07


Related Articles

Introduction to Formal Verification
Why Formal Verification?
Concept of Formal Verification
Methodologies in Formal Verification
Binary Decision Diagram (BDD)
Equivalence Checking (EC)
Model Checking
Theorem Proving
Satisfiability (SAT) Solvers
Recent Advances in SAT Based Formal Verification
Formal Verification Example Read the rest of this article >>

Recent Advances in SAT Based Formal Verification

SAT can be used for model checking and the method is known as Bounded Model Checking. Bounded Model Checking based on SAT methods was introduced by Biere et al. [7]. This is rapidly gaining popularity as a complementary technique to BDD-based symbolic model checking. A more compact CNF for the BMC problem is used to generate structural processing. This makes the resulting SAT problem easier for the SAT solver to solve. Traditional model checking uses a method, known as cone of influence (COI) reduction. An improvement on this method the method of bounded cone of influence (BCOI) reduction. Variable ordering has long been recognized as a key determinant of the performance of SAT solvers. BMC tools using circuit-based SAT solvers essentially use some variant of the J-frontier justification heuristic popularly used in sequential ATPG tools.

Several case studies mentioned in [7] which employed BMC as Formal Verification methodology has proven the capability of the model successfully. BMC was found to significantly outperform the BDD based Symbolic Model Verification model checker for several of the benchmarks. The case studies were carried out on processors like PowerPC and Intel Pentium 4. Thus it is generally accepted in the research and industrial community that SAT-BMC tools require minimal tuning effort and work particularly well on large designs where bugs need to be searched at shallow to medium depths.
The paper [7] further surveys the several other latest trends in Model Checking algorithm based on SAT solvers. Few of them are named here: SAT-based Unbounded Model Checking, ATPG-based Model Checking, Quantified Boolean Formulae (QBF).

The SAT-based verification has been emerged as an orthogonal technology to BDD-based model checking techniques (bounded and unbounded). SAT based techniques require fewer users tuning as well as less sensitive to the problem size. However, major challenge is to develop a verification methodology which employs both SAT and BDD methods in a manner best suited to utilize their respective strengths.

Reference

[1] Sandeep K. Shukla, “An Introduction to Formal Verification”, http://www.ics.uci.edu/~rgupta/ics212/w2002/verification.pdf, 9/10/07

[2] Rolf Drechsler, “Towards Formal Verification on the System Level”, Institute of Computer Science, University of Bremen, Germany, 2005

[3] Prof. Eduard Cerny, Xiaoyu Song, “Formal Verification Methods”, University of Montrial, Canada, 1999. http://www.iro.umontreal.ca/~cerny/IFT6222/1-intro-99.0808.pdf, 9/10/07

[4] Jawahar Jain, Amit Narayan, M.Fujita, A.Sangiovanni Vincentelli, “A Survey of Techniques for Formal Verification of Combinational Circuits”, Proceedings of the 1997 International Conference on Computer Design (ICCD '97), IEEE, 1997

[5] F. Wang, “Formal Verification of Timed Systems: A Survey and Perspective”, Proceedings of the IEEE, Vol. 92, No. 8, August 2004. pp.283-1305. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[6] J. Bhadra, M. S. Abadir, L.-C. Wang, S. Ray, “Functional Verification through Hybrid Techniques: A Survey”, journal of IEEE Design & Test of Computers, March-April 2007. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[7] M. Prasad, A. Biere, A. Gupta, “A Survey of Recent Advances in SAT-Based Formal Verification”, Software Tools for Technology Transfer, Vol. 7, No. 2, 2005. pp. 156-173. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07


Related Articles

Introduction to Formal Verification
Why Formal Verification?
Concept of Formal Verification
Methodologies in Formal Verification
Binary Decision Diagram (BDD)
Equivalence Checking (EC)
Model Checking
Theorem Proving
Satisfiability (SAT) Solvers
Hybrid Formal Verification Techniques
Formal Verification Example Read the rest of this article >>

Satisfiability (SAT) Solvers

Most SAT solvers use a Conjunctive Normal Form (CNF) representation of the Boolean formula. In CNF representation the formula is represented as a conjunction of clauses, each clause is a disjunction of literals, and a literal is a variable or its negation. Each clause must evaluate to true to satisfy the formula. There exist polynomial algorithms to transform an arbitrary propositional formula into a satisfiability equivalent CNF formula that is satisfiable if and only if the original formula is satisfiable. The SAT solver may be modified to work directly on the Boolean circuit representation. Most modern SAT solvers are based on the Davis-Putnam- Logemann-Loveland (DPLL) algorithm. The DPLL algorithm finds a solution if and only if the formula is satisfiable. However, modern SAT solvers use conflict analysis techniques to analyze the reasons for a conflict.

Reference

[1] Sandeep K. Shukla, “An Introduction to Formal Verification”, http://www.ics.uci.edu/~rgupta/ics212/w2002/verification.pdf, 9/10/07

[2] Rolf Drechsler, “Towards Formal Verification on the System Level”, Institute of Computer Science, University of Bremen, Germany, 2005

[3] Prof. Eduard Cerny, Xiaoyu Song, “Formal Verification Methods”, University of Montrial, Canada, 1999. http://www.iro.umontreal.ca/~cerny/IFT6222/1-intro-99.0808.pdf, 9/10/07

[4] Jawahar Jain, Amit Narayan, M.Fujita, A.Sangiovanni Vincentelli, “A Survey of Techniques for Formal Verification of Combinational Circuits”, Proceedings of the 1997 International Conference on Computer Design (ICCD '97), IEEE, 1997

[5] F. Wang, “Formal Verification of Timed Systems: A Survey and Perspective”, Proceedings of the IEEE, Vol. 92, No. 8, August 2004. pp.283-1305. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[6] J. Bhadra, M. S. Abadir, L.-C. Wang, S. Ray, “Functional Verification through Hybrid Techniques: A Survey”, journal of IEEE Design & Test of Computers, March-April 2007. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[7] M. Prasad, A. Biere, A. Gupta, “A Survey of Recent Advances in SAT-Based Formal Verification”, Software Tools for Technology Transfer, Vol. 7, No. 2, 2005. pp. 156-173. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07


Related Articles

Introduction to Formal Verification
Why Formal Verification?
Concept of Formal Verification
Methodologies in Formal Verification
Binary Decision Diagram (BDD)
Equivalence Checking (EC)
Model Checking
Theorem Proving
Recent Advances in SAT Based Formal Verification
Hybrid Formal Verification Techniques
Formal Verification Example Read the rest of this article >>

Theorem proving

A theorem in logic is nothing but relationship (i.e. logical equivalence/logical implication) between a specification and an implementation. This theorem has to be proven within the context of a proof calculus. The implementation should satisfy specifications provided. This is then proved by mathematical reasoning. Implementation and specification expressed as formulas in a formal logic. The implementation provides axioms and assumptions that the proof can draw upon. The inference can be simplification, rewriting, induction etc.

Figure (1) Theorem proving [3]

Proof checking and generation

It is a purely syntactic matter to decide whether each theorem is an axiom or follows from previous theorems (axioms) by a rule of inference. Complete automation of theorem proving methodology is generally not possible due to theoretical limitations of decisions. However, a greater part of the theorem, like decidable subsets, specific classes of applications and specification styles can be automated. All theorem proving techniques require human guidance in indirect form.

Theorem Proving Systems

Theorem proving systems can be broadly classified into Automated Deduction Systems (e.g. Prolog) and Interactive Theorem Proving Systems. Automated deduction systems are full automatic, but only for a decidable subset of FOL. here speed is emphasized over versatility. Since this method is often developed in the context of application specific research, methodology is implemented by ad hoc decision procedures. Interactive theorem proving systems are semi-automatic, but not restricted to a decidable subset. Versatility of the method is emphasized over speed. Naturally this method is slow. Theoretically a complete proof can be generated for every theorem.

Some known theorem proving systems are Boyer-Moore (first-order logic), HOL (higher-order logic), PVS (higher-order logic) and Lambda (higher-order logic).

Advantages of Theorem Proving

* Theorem proving methodology provides high abstraction and powerful logic expressiveness and powerful reasoning.
* User is in full control of the design. Hence hierarchical structure and regularity of the design ca be fully exploited.
* The methodology is very much useful for verifying parameterized Datapath-dominated circuits. The technique can be customized for specific application i.e. larger proofs can be built based on basic ones.

Disadvantages of Theorem Proving

* User intervention and guidance is necessary for the verification process. This necessitates expertise in the field. To prove small theorems large human investment is necessary.
* The methodology is automated for narrow classes of designs only. Hence the technique is still under development.
* As the complexity of the design increases theorem proving becomes difficult.

Reference

[1] Sandeep K. Shukla, “An Introduction to Formal Verification”, http://www.ics.uci.edu/~rgupta/ics212/w2002/verification.pdf, 9/10/07

[2] Rolf Drechsler, “Towards Formal Verification on the System Level”, Institute of Computer Science, University of Bremen, Germany, 2005

[3] Prof. Eduard Cerny, Xiaoyu Song, “Formal Verification Methods”, University of Montrial, Canada, 1999. http://www.iro.umontreal.ca/~cerny/IFT6222/1-intro-99.0808.pdf, 9/10/07

[4] Jawahar Jain, Amit Narayan, M.Fujita, A.Sangiovanni Vincentelli, “A Survey of Techniques for Formal Verification of Combinational Circuits”, Proceedings of the 1997 International Conference on Computer Design (ICCD '97), IEEE, 1997

[5] F. Wang, “Formal Verification of Timed Systems: A Survey and Perspective”, Proceedings of the IEEE, Vol. 92, No. 8, August 2004. pp.283-1305. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[6] J. Bhadra, M. S. Abadir, L.-C. Wang, S. Ray, “Functional Verification through Hybrid Techniques: A Survey”, journal of IEEE Design & Test of Computers, March-April 2007. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[7] M. Prasad, A. Biere, A. Gupta, “A Survey of Recent Advances in SAT-Based Formal Verification”, Software Tools for Technology Transfer, Vol. 7, No. 2, 2005. pp. 156-173. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07


Related Articles

Introduction to Formal Verification

Why Formal Verification?

Concept of Formal Verification

Methodologies in Formal Verification

Binary Decision Diagram (BDD)

Equivalence Checking (EC)

Model Checking

Satisfiability (SAT) Solvers

Recent Advances in SAT Based Formal Verification

Hybrid Formal Verification Techniques

Formal Verification Example

Read the rest of this article >>

Model Checking

In Model Checking property is in the form of a temporal logic formula and sequential properties are usually represented in temporal logic. Various variants of temporal logic formulae are available such as Linear Temporal Logic (LTL) or Computation Tree Logic (CTL). These logics usually require dedicated algorithms. The truth of formula is determined against a semantic model of the implementation. The system is modeled by Labeled Transition Graph (LTG, LTS, and Finite Kripke Structure). The algorithm carries an exhaustive search through the state space of the system to determine if the specified property holds or not. For larger designs, this search creates “state explosion” problem. Symbolic Model Checking comes as a partial solution this problem.


Figure (1) Model Checking [3]
Figure (2) Symbolic Model Checking [3]


Symbolic Model Checking

Here transition or output relations and sets of states are symbolically represented using ROBDD as shown in the Figure (2). Model checking used an explicit representation of states. A large Hash table is used to store individual states. The states reached during a depth first traversal of the state space are memorized as hash values. Since the number of states of even small systems can be very large, e.g., a 128 bit shift register has 2128 states; this method does not scale, in particular for sequential circuits. This problem is called state explosion problem. In symbolic model checking this problem is sorted out. Symbolic model checking operates on sets of states instead of individual states and represents sets of states symbolically in a compact form.

Advantages of MC

* The verification process is completely automated.
* Counter examples are generated for identifying design errors.

Disadvantages of MC

* The main drawback is State explosion problem because of which maximum of 400 Boolean variables can be processed. In complex designs data paths pose problems.

Reference

[1] Sandeep K. Shukla, “An Introduction to Formal Verification”, http://www.ics.uci.edu/~rgupta/ics212/w2002/verification.pdf, 9/10/07

[2] Rolf Drechsler, “Towards Formal Verification on the System Level”, Institute of Computer Science, University of Bremen, Germany, 2005

[3] Prof. Eduard Cerny, Xiaoyu Song, “Formal Verification Methods”, University of Montrial, Canada, 1999. http://www.iro.umontreal.ca/~cerny/IFT6222/1-intro-99.0808.pdf, 9/10/07

[4] Jawahar Jain, Amit Narayan, M.Fujita, A.Sangiovanni Vincentelli, “A Survey of Techniques for Formal Verification of Combinational Circuits”, Proceedings of the 1997 International Conference on Computer Design (ICCD '97), IEEE, 1997

[5] F. Wang, “Formal Verification of Timed Systems: A Survey and Perspective”, Proceedings of the IEEE, Vol. 92, No. 8, August 2004. pp.283-1305. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[6] J. Bhadra, M. S. Abadir, L.-C. Wang, S. Ray, “Functional Verification through Hybrid Techniques: A Survey”, journal of IEEE Design & Test of Computers, March-April 2007. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[7] M. Prasad, A. Biere, A. Gupta, “A Survey of Recent Advances in SAT-Based Formal Verification”, Software Tools for Technology Transfer, Vol. 7, No. 2, 2005. pp. 156-173. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

Related Articles

Introduction to Formal Verification

Why Formal Verification?

Concept of Formal Verification

Methodologies in Formal Verification

Binary Decision Diagram (BDD)

Equivalence Checking (EC)

Theorem Proving

Satisfiability (SAT) Solvers

Recent Advances in SAT Based Formal Verification

Hybrid Formal Verification Techniques

Formal Verification Example

Read the rest of this article >>

Equivalence Checking (EC)

Here the goal is to ensure the equivalence of two given circuit descriptions. These circuit descriptions can be in different levels of abstractions. EC translate both designs to an internal format. In matching phase, it establishes correspondence between the two designs and proves the equivalence or in equivalence. It determines if two expressions, say F and G denote the same truth table. The extract representation of logic expressions F and G are verified either by satisfiability algorithms (propositional resolution) or by ROBDD. In the case of in-equivalence, a counter example is generated and debugging phase starts. Generated counter examples are not reachable during normal circuit operation. [2]

Combinational Equivalence Checking

Design is considered as purely combinational. Each state element is modeled as additional primary inputs and outputs. A BDD can be constructed by considering depth first vs. breadth first construction style for optimized use of memory by keeping only few levels in memory, rest on disk. Dynamic reordering can generate excessive memory usage. Partitioning of Boolean space, each represented by a separate BDD reduces complexities of verification process.

The available commercial tools which employ this methodology are: Design Verifier from Chrysalis, Formality from Synopsys, Affirma from Cadence and Tornado from Verysys.
Challenges of EC

* Complexity: It is well known fact that Moore’s law still rules! More the complexity of circuit BDDs suffer from “memory explosion” problem.

* Proof technology integration: BDDs and SAT are most popular methods applied in hardware verification tools. Modern verification tools make use of multiengine approach that combine different methodologies, like SAT, BDD and ATPG. The successful combination approach is still a bottleneck.

* Matching: For larger designs matching algorithms either fails or consume enormous computation time.

* Arithmetic: Often BDD and SAT have difficulties with arithmetic circuit, like multipliers. Arithmetic circuits that are concurrent in nature are a challenge to FV.

* Analog and mixed signal: Modern SOC designs have both analog and digital circuits integrated together. Present proof technologies assume that the circuit is purely digital; practically it is not the case. Verifying analog circuits is most challenging task.

* Multi clock domains: Present day EC solvers can’t work with multiple clock domains whereas most of the practical designs have more than one clock domain.

Reference

[1] Sandeep K. Shukla, “An Introduction to Formal Verification”, http://www.ics.uci.edu/~rgupta/ics212/w2002/verification.pdf, 9/10/07

[2] Rolf Drechsler, “Towards Formal Verification on the System Level”, Institute of Computer Science, University of Bremen, Germany, 2005

[3] Prof. Eduard Cerny, Xiaoyu Song, “Formal Verification Methods”, University of Montrial, Canada, 1999. http://www.iro.umontreal.ca/~cerny/IFT6222/1-intro-99.0808.pdf, 9/10/07

[4] Jawahar Jain, Amit Narayan, M.Fujita, A.Sangiovanni Vincentelli, “A Survey of Techniques for Formal Verification of Combinational Circuits”, Proceedings of the 1997 International Conference on Computer Design (ICCD '97), IEEE, 1997

[5] F. Wang, “Formal Verification of Timed Systems: A Survey and Perspective”, Proceedings of the IEEE, Vol. 92, No. 8, August 2004. pp.283-1305. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[6] J. Bhadra, M. S. Abadir, L.-C. Wang, S. Ray, “Functional Verification through Hybrid Techniques: A Survey”, journal of IEEE Design & Test of Computers, March-April 2007. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[7] M. Prasad, A. Biere, A. Gupta, “A Survey of Recent Advances in SAT-Based Formal Verification”, Software Tools for Technology Transfer, Vol. 7, No. 2, 2005. pp. 156-173. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07


Related Articles

Introduction to Formal Verification
Why Formal Verification?
Concept of Formal Verification
Methodologies in Formal Verification
Binary Decision Diagram (BDD)
Model Checking
Theorem Proving
Satisfiability (SAT) Solvers
Recent Advances in SAT Based Formal Verification
Hybrid Formal Verification Techniques
Formal Verification Example



Read the rest of this article >>

Binary Decision Diagram (BDD)

Decision to traverse in the binary tree is taken depending on the binary value of the variable. Each node of the diagram represent sets of objects (states) encoded as Boolean functions. Reduced Ordered BDD (ROBDD) is canonical and canonicity is essential for verification.

Certain rules have to be followed to construct ROBDD.

They are:

1. Terminal should not duplicate. Remove all duplicate terminals.
2. Remove all duplicate nodes.
3. Remove internal nodes with identical children.

Consider a function f = ac + bc. Binary Decision Diagram for this function is shown in Figure (1). Straight lines in the diagram shows path of the binary one and dotted line show binary zero. All possible combinations of variables a, b and c and corresponding outputs are drawn in the diagram. The binary values within the square boxes represent the possible output values for function f with different input combinations. This BDD can be reduced to obtain ROBDD.

Figure (1) Binary Decision Diagram (BDD) construction [1]

The steps to obtain a ROBDD are shown Figure (2).

Figure (2) ROBDDD construction [1]
Figure (3) Application to verification [1]

Application of these BDDs to check the equivalence of combinational circuits is depicted in Figure (3). If two functions, say, F= a’bc+ab’c and G=ac+bc are equivalent then their BDDs are identical. ROBDD for both F and G are identical as shown in Figure (3). Thus this methodology is applied in formal verification techniques to check the equivalence of circuit description. Some industrial packages that employ this methodology are: Intel, Lucent, Cadence, Synopsys (Formality), Bull Systems, etc.

There are some critical drawbacks related to BDD. For larger functions there may not be a canonical form existing or the existing one may be too large (exponential). Operations like complementation may yield a representation of exponential size. In this case equivalence and tautology checking becomes hard.

A detailed discussion over variable ordering, breadth first manipulation, node decompositions, partitioned ROBDDs, verification of arithmetic circuits etc can be found in [4].

Reference

[1] Sandeep K. Shukla, “An Introduction to Formal Verification”, http://www.ics.uci.edu/~rgupta/ics212/w2002/verification.pdf, 9/10/07

[2] Rolf Drechsler, “Towards Formal Verification on the System Level”, Institute of Computer Science, University of Bremen, Germany, 2005

[3] Prof. Eduard Cerny, Xiaoyu Song, “Formal Verification Methods”, University of Montrial, Canada, 1999. http://www.iro.umontreal.ca/~cerny/IFT6222/1-intro-99.0808.pdf, 9/10/07

[4] Jawahar Jain, Amit Narayan, M.Fujita, A.Sangiovanni Vincentelli, “A Survey of Techniques for Formal Verification of Combinational Circuits”, Proceedings of the 1997 International Conference on Computer Design (ICCD '97), IEEE, 1997

[5] F. Wang, “Formal Verification of Timed Systems: A Survey and Perspective”, Proceedings of the IEEE, Vol. 92, No. 8, August 2004. pp.283-1305. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[6] J. Bhadra, M. S. Abadir, L.-C. Wang, S. Ray, “Functional Verification through Hybrid Techniques: A Survey”, journal of IEEE Design & Test of Computers, March-April 2007. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[7] M. Prasad, A. Biere, A. Gupta, “A Survey of Recent Advances in SAT-Based Formal Verification”, Software Tools for Technology Transfer, Vol. 7, No. 2, 2005. pp. 156-173. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07


Related Articles
Introduction to Formal Verification
Why Formal Verification?
Concept of Formal Verification
Methodologies in Formal Verification
Equivalence Checking (EC)
Model Checking
Theorem Proving
Satisfiability (SAT) Solvers
Recent Advances in SAT Based Formal Verification
Hybrid Formal Verification Techniques
Formal Verification Example Read the rest of this article >>

Methodologies in Formal Verification

Mainly 3 methodologies are followed in Formal Verification of hardware designs.

They are:

1. Equivalence Checking (EC)
2. Model Checking (MC)
3. Theorem Proving (TP)

In Equivalence Checking method, Design Under Test and reference are reduced to an equation and Design Under Test is compared with reference design. This methodology is traditionally employed in most of the Formal Verification tools and well established as it is easy to implement.

The second Model Checking is comparatively complex and only academic tools are available. Here Design Under Test is verified for the satisfaction of given specification under all conditions. The specifications or properties provided are in terms of mathematical formulae or equations.

The third methodology, Theorem Proving is toughest of all but provides very accurate comparison and hence most efficient. Here theorem is extracted from Design Under Test and proved with respect to the reference design. Few of the industry level tools provide this methodology and it is of more research interest yet.

In each of these methodologies we can find sub methods which are employed to implement the Formal Verification algorithm. As we noted, Equivalence Checking is most commonly employed in traditional method. Under this category we find two important methodologies.

They are:

1. Binary Decision Diagram (BDD): This is more commonly implemented in Formal Verification tools. (E.g. Formality by Synopsys).

2. Satisfiability (SAT) Solvers: Several advancements are happening based on this method.

The Binary Decision Diagram and SAT solvers are fundamental methods used in latest FV developments like Symbolic Model Verification (SMV) and also Bounded Model Checking (BMC). Both the BDD and SAT solvers are professionally employed in several industrial Formal Verification tools. They are the basis of all advancement in Formal Verification. Hence it is very relevant to discuss about Binary Decision Diagram and SAT solvers in general.

Reference

[1] Sandeep K. Shukla, “An Introduction to Formal Verification”, http://www.ics.uci.edu/~rgupta/ics212/w2002/verification.pdf, 9/10/07

[2] Rolf Drechsler, “Towards Formal Verification on the System Level”, Institute of Computer Science, University of Bremen, Germany, 2005

[3] Prof. Eduard Cerny, Xiaoyu Song, “Formal Verification Methods”, University of Montrial, Canada, 1999. http://www.iro.umontreal.ca/~cerny/IFT6222/1-intro-99.0808.pdf, 9/10/07

[4] Jawahar Jain, Amit Narayan, M.Fujita, A.Sangiovanni Vincentelli, “A Survey of Techniques for Formal Verification of Combinational Circuits”, Proceedings of the 1997 International Conference on Computer Design (ICCD '97), IEEE, 1997

[5] F. Wang, “Formal Verification of Timed Systems: A Survey and Perspective”, Proceedings of the IEEE, Vol. 92, No. 8, August 2004. pp.283-1305. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[6] J. Bhadra, M. S. Abadir, L.-C. Wang, S. Ray, “Functional Verification through Hybrid Techniques: A Survey”, journal of IEEE Design & Test of Computers, March-April 2007. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[7] M. Prasad, A. Biere, A. Gupta, “A Survey of Recent Advances in SAT-Based Formal Verification”, Software Tools for Technology Transfer, Vol. 7, No. 2, 2005. pp. 156-173. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07


Related Articles

Introduction to Formal Verification
Why Formal Verification?
Concept of Formal Verification
Binary Decision Diagram (BDD)
Equivalence Checking (EC)
Model Checking
Theorem Proving
Satisfiability (SAT) Solvers
Recent Advances in SAT Based Formal Verification
Hybrid Formal Verification Techniques
Formal Verification Example Read the rest of this article >>

Concept of Formal Verification

In Formal Verification process Design Under Test (DUT) is compared with proven design or set of properties (or specifications). Proven design is considered as Reference design and is also called as Golden Reference. Both the DUT and reference is reduced to Boolean equations or mathematical theorem or models and these are compared to each other.

The DUT and reference design may be in different level of abstraction i.e. either it can be in RTL or gate level. DUT can be HDL (Verilog or VHDL or any other) code or Netlist. Similarly reference design can also be in HDL code or Netlist. Only prerequisite here is DUT and reference should have same functionality.

As shown in the figure code and post synthesis netlist can be formally verified. The post synthesis netlist is generated either in .lib or .v or .VITAL format. Formal Verification tools allow verifying these two netlists that represent same functionality.

Figure Showing Formal Verification Flow

The most attractive feature of any Formal Verification method is that the verification is completely exhaustive which not the case with simulations is. Consideration of “all possible cases” is implicit in formal verification. The correctness of circuit description is guaranteed mathematically, regardless the input values. There is no need to generate expected output sequences. The formal verification can generate an error trace if a property fails which can be confirmed by simulation. Formal verification is useful to detect and locate errors in designs.

Reference

[1] Sandeep K. Shukla, “An Introduction to Formal Verification”, http://www.ics.uci.edu/~rgupta/ics212/w2002/verification.pdf, 9/10/07

[2] Rolf Drechsler, “Towards Formal Verification on the System Level”, Institute of Computer Science, University of Bremen, Germany, 2005

[3] Prof. Eduard Cerny, Xiaoyu Song, “Formal Verification Methods”, University of Montrial, Canada, 1999. http://www.iro.umontreal.ca/~cerny/IFT6222/1-intro-99.0808.pdf, 9/10/07

[4] Jawahar Jain, Amit Narayan, M.Fujita, A.Sangiovanni Vincentelli, “A Survey of Techniques for Formal Verification of Combinational Circuits”, Proceedings of the 1997 International Conference on Computer Design (ICCD '97), IEEE, 1997

[5] F. Wang, “Formal Verification of Timed Systems: A Survey and Perspective”, Proceedings of the IEEE, Vol. 92, No. 8, August 2004. pp.283-1305. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[6] J. Bhadra, M. S. Abadir, L.-C. Wang, S. Ray, “Functional Verification through Hybrid Techniques: A Survey”, journal of IEEE Design & Test of Computers, March-April 2007. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[7] M. Prasad, A. Biere, A. Gupta, “A Survey of Recent Advances in SAT-Based Formal Verification”, Software Tools for Technology Transfer, Vol. 7, No. 2, 2005. pp. 156-173. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

Related Articles

Introduction to Formal Verification
Why Formal Verification?

Methodologies in Formal Verification

Binary Decision Diagram (BDD)

Equivalence Checking (EC)

Model Checking

Theorem Proving

Satisfiability (SAT) Solvers

Recent Advances in SAT Based Formal Verification

Hybrid Formal Verification Techniques

Formal Verification Example

Read the rest of this article >>

Why Formal Verification?

Different simulation were under use way back in 1980s itself. These are used to check the functionality of the digital designs. Even after the enormous progress of the simulation methodologies, complexities involved in the simulation have not reduced. The high cost factor of the supporting simulation libraries and more time consumed in generating input patterns are the two main road blocks of simulation tools.

The existing general simulation methodologies are slow.

Consider two types of simulators:
- Event based and
- Cycle based simulators.

“Event based simulators” simulate whenever there is an event i.e. there is a change in data value. Modelsim simulator tool is a good example for this. Since they are waiting for event they are inherently slow.

On the other hand, “cycle based simulators” simulate every cycle. These types of simulators do not wait for event and simulate independently. Hence they are around 10 times faster event based simulators.

The other type of simulators like code compiled simulators and native compiled simulators convert HDL code to either C or machine level language directly. This is known as system level simulation. SystemC and System Verilog strongly came out as a possible solution to functional verification complexities. This couldn’t solve the complexities of the simulation process as these languages are sequential in nature unlike HDL languages which are concurrent in nature.

Despite of all these developments 70% of the time is utilized for design verification and validation and only 30% of time is spent on design development. Considering the time to market span of the industry, it is essential to reduce the verification time without compromising the quality of the design verification process. Formal Verification reduces the simulation time and complexities involved in it. It is desirable to have formal verification technique at system level [2] also. Several approaches are presented [2-7] which allow verification at system level also.

Reference

[1] Sandeep K. Shukla, “An Introduction to Formal Verification”, http://www.ics.uci.edu/~rgupta/ics212/w2002/verification.pdf, 9/10/07

[2] Rolf Drechsler, “Towards Formal Verification on the System Level”, Institute of Computer Science, University of Bremen, Germany, 2005

[3] Prof. Eduard Cerny, Xiaoyu Song, “Formal Verification Methods”, University of Montrial, Canada, 1999. http://www.iro.umontreal.ca/~cerny/IFT6222/1-intro-99.0808.pdf, 9/10/07

[4] Jawahar Jain, Amit Narayan, M.Fujita, A.Sangiovanni Vincentelli, “A Survey of Techniques for Formal Verification of Combinational Circuits”, Proceedings of the 1997 International Conference on Computer Design (ICCD '97), IEEE, 1997

[5] F. Wang, “Formal Verification of Timed Systems: A Survey and Perspective”, Proceedings of the IEEE, Vol. 92, No. 8, August 2004. pp.283-1305. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[6] J. Bhadra, M. S. Abadir, L.-C. Wang, S. Ray, “Functional Verification through Hybrid Techniques: A Survey”, journal of IEEE Design & Test of Computers, March-April 2007. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

[7] M. Prasad, A. Biere, A. Gupta, “A Survey of Recent Advances in SAT-Based Formal Verification”, Software Tools for Technology Transfer, Vol. 7, No. 2, 2005. pp. 156-173. http://www.cerc.utexas.edu/~jay/fv_surveys/, 9/10/07

Related Articles

Introduction to Formal Verification
Why Formal Verification?
Concept of Formal Verification
Methodologies in Formal Verification
Binary Decision Diagram (BDD)
Equivalence Checking (EC)
Model Checking
Theorem Proving
Satisfiability (SAT) Solvers
Recent Advances in SAT Based Formal Verification
Hybrid Formal Verification Techniques
Formal Verification Example Read the rest of this article >>

Introduction to Formal Verification

Around 70% of the overall design time and cost is spent on verification and validation. It becomes very important to verify the correctness of the circuits. Modern complex designs contain several hundred million transistors. Verification of such a complex system in a shorter span of time becomes a dominating factor before it goes silicon level. Several Formal Verification methods have been proposed and are under research as an alternative to classical simulation techniques, since it can’t guarantee sufficient coverage of the design. In addition to this simulation is a slow process. Formal Verification (FV) techniques ensure 100% functional correctness and they are more reliable and cost effective, less time consuming. The main concept of FV is not to simulate some vectors, instead prove the functional correctness of a design.

There are different proof methodologies employed, the most common being Equivalence Checking (EC) methodology. The basic methodology used in most of the industry verification tools, known as Binary Decision Diagram (BDD) and Satisfiability (SAT) solvers, come under this category. These traditional methods fail to handle complex circuits efficiently. Hence new trends like SAT based Symbolic Model Checking are emerging which fall under Model Checking (MC) (Also known as Property Checking (PC)) methodology. New techniques like Bounded Model Checking (BMC) based on SAT solvers are promising better efficient methods of Formal Verification. Hybrid Formal Verification methods are under investigation which employs strength of respective Formal Verification models. Each of these methods has their own pros and cons which will be discussed in subsequent articles. The papers I have referred are listed below. For SAT solver related latest developments, [7] is referred and for hybrid Formal Verification methods [6] is referred.

Reference

[1] Sandeep K. Shukla, An Introduction to Formal Verification, http://www.ics.uci.edu/~rgupta/ics212/w2002/verification.pdf, 3/4/07

[2] Rolf Drechsler, Towards Formal Verification on the System Level, Institute of Computer Science, University of Bremen, Germany, 2005

[3] Prof. Eduard Cerny, Xiaoyu SongFormal Verification Methods, University of Montrial, Canada, 1999. http://www.iro.umontreal.ca/~cerny/IFT6222/1-intro-99.0808.pdf, 5/4/07

[4] Jawahar Jain, Amit Narayan, M.Fujita, A.Sangiovanni Vincentelli, a survey of techniques for formal verification of combinational circuits, Proceedings of the 1997 International Conference on Computer Design (ICCD '97), IEEE, 1997

[5] F. Wang, Formal Verification of Timed Systems: A Survey and Perspective, Proceedings of the IEEE, Vol. 92, No. 8, August 2004. pp.283-1305. http://www.cerc.utexas.edu/~jay/fv_surveys/, 13/4/07

[6] J. Bhadra, M. S. Abadir, L.-C. Wang, S. Ray, Functional Verification through Hybrid Techniques: A Survey, journal of IEEE Design & Test of Computers, March-April 2007. http://www.cerc.utexas.edu/~jay/fv_surveys/, 13/4/07

[7] M. Prasad, A. Biere, A. Gupta, A Survey of Recent Advances in SAT-Based Formal Verification, Software Tools for Technology Transfer, Vol. 7, No. 2, 2005. pp. 156-173. http://www.cerc.utexas.edu/~jay/fv_surveys/, 13/4/07

Related Articles

Why Formal Verification?

Concept of Formal Verification

Methodologies in Formal Verification

Binary Decision Diagram (BDD)

Equivalence Checking (EC)

Model Checking

Theorem Proving

Satisfiability (SAT) Solvers

Recent Advances in SAT Based Formal Verification

Hybrid Formal Verification Techniques

Formal Verification Example

Read the rest of this article >>

Verilog Code for Systolic Array Matrix Multiplier

Below is the Verilog code for 3x3 Systolic Array Matrix Multiplier (let me give it a name in short:SAMM !).
I am going to take this code as an example for several other articles that i am publishing in the blog.
So keep an eye on this always !

//===================================
`timescale 1ns/1ps
//----------------------------------------------------------------
module sam3( a_row0,a_row1,a_row2, //matrix a inputs
b_col0,b_col1,b_col2, //matrix b inputs
c_row0,c_row1,c_row2, //output matrix c
en,reset,clock,mult_over);//control signals
output reg [9:0] c_row0,c_row1,c_row2;
output reg mult_over;
//output mult_over;
input [3:0] a_row0,a_row1,a_row2,b_col0,b_col1,b_col2;
input en,reset,clock;
reg [3:0] aa_row0[2:0],aa_row1[2:0],aa_row2[2:0],bb_col0[2:0],bb_col1[2:0],bb_col2[2:0];//memory to hold matrix a and b;a:rowwise;b:columnwise
reg [9:0] out_reg00,out_reg01,out_reg02,out_reg10,out_reg11,out_reg12,out_reg20,out_reg21,out_reg22;//output registers to hold matrix c
//reg [9:0] cc_row0[2:0],cc_row1[2:0],cc_row2[2:0];
//reg mult_over,all_over;
reg [3:0] q;
//wire [3:0] q;
wire [9:0] cc_row_00,cc_row_01,cc_row_02,cc_row_10,cc_row_11,cc_row_12,cc_row_20,cc_row_21,cc_row_22;
//===========================================================
always @(posedge clock)
begin
if(en & !reset)
q<=q+1;
else
q<=0;
if(q>=11) mult_over=1; else mult_over=0; //multiplication is over after 11 clock cycles
//5+3 clock cycles to fill the systolic processor pipeline stage
//3 clock cycle for multiplication
end
//============================================================
//count_clock clock_counter(.en(en),.reset(reset),.clock(clock),.q(q),.mult_over(mult_over));
//============================================================
//============================================================
always @(posedge clock)
begin
if((!en) & reset)
begin
aa_row0[0]<=0;aa_row0[1]<=0;aa_row0[2]<=0;
aa_row1[0]<=0;aa_row1[1]<=0;aa_row1[2]<=0;
aa_row2[0]<=0;aa_row2[1]<=0;aa_row2[2]<=0;
bb_col0[0]<=0;bb_col0[1]<=0;bb_col0[2]<=0;
bb_col1[0]<=0;bb_col1[1]<=0;bb_col1[2]<=0;
bb_col2[0]<=0;bb_col2[1]<=0;bb_col2[2]<=0;
out_reg00<=0;out_reg01<=0;out_reg02<=0;
out_reg10<=0;out_reg11<=0;out_reg12<=0;
out_reg20<=0;out_reg21<=0;out_reg22<=0;
c_row0<=0;
c_row1<=0;
c_row2<=0;
end
else
begin
aa_row0[0]<=a_row0;aa_row0[1]<=aa_row0[0];aa_row0[2]<=aa_row0[1];
aa_row1[0]<=a_row1;aa_row1[1]<=aa_row1[0];aa_row1[2]<=aa_row1[1];
aa_row2[0]<=a_row2;aa_row2[1]<=aa_row2[0];aa_row2[2]<=aa_row2[1];
bb_col0[0]<=b_col0;bb_col0[1]<=bb_col0[0];bb_col0[2]<=bb_col0[1];
bb_col1[0]<=b_col1;bb_col1[1]<=bb_col1[0];bb_col1[2]<=bb_col1[1];
bb_col2[0]<=b_col2;bb_col2[1]<=bb_col2[0];bb_col2[2]<=bb_col2[1];
//end
if(!mult_over) //if multiplication is over send result to output one by one
begin //else update output registers with accumulated results
c_row0<=0;
c_row1<=0;
c_row2<=0;
out_reg00<=cc_row_00;
out_reg01<=cc_row_01;
out_reg02<=cc_row_02;

out_reg10<=cc_row_10;
out_reg11<=cc_row_11;
out_reg12<=cc_row_12;
out_reg20<=cc_row_20;
out_reg21<=cc_row_21;
out_reg22<=cc_row_22;
end
else
begin
c_row0<=out_reg00;out_reg00<=out_reg01;out_reg01<=out_reg02;
c_row1<=out_reg10;out_reg10<=out_reg11;out_reg11<=out_reg12;
c_row2<=out_reg20;out_reg20<=out_reg21;out_reg21<=out_reg22;
end
end
end //end of if-else loop
//==============================================================
//instantiate macs
//===================================================================
mac mac00(.row_element(aa_row0[0]),.col_element(bb_col0[0]),.mac_out(cc_row_00),.reset(reset),.clock(clock));
mac mac01(.row_element(aa_row0[1]),.col_element(bb_col1[0]),.mac_out(cc_row_01),.reset(reset),.clock(clock));
mac mac02(.row_element(aa_row0[2]),.col_element(bb_col2[0]),.mac_out(cc_row_02),.reset(reset),.clock(clock));
mac mac10(.row_element(aa_row1[0]),.col_element(bb_col0[1]),.mac_out(cc_row_10),.reset(reset),.clock(clock));
mac mac11(.row_element(aa_row1[1]),.col_element(bb_col1[1]),.mac_out(cc_row_11),.reset(reset),.clock(clock));
mac mac12(.row_element(aa_row1[2]),.col_element(bb_col2[1]),.mac_out(cc_row_12),.reset(reset),.clock(clock));
mac mac20(.row_element(aa_row2[0]),.col_element(bb_col0[2]),.mac_out(cc_row_20),.reset(reset),.clock(clock));
mac mac21(.row_element(aa_row2[1]),.col_element(bb_col1[2]),.mac_out(cc_row_21),.reset(reset),.clock(clock));
mac mac22(.row_element(aa_row2[2]),.col_element(bb_col2[2]),.mac_out(cc_row_22),.reset(reset),.clock(clock));
endmodule

Read the rest of this article >>

DFT enabled circuit analysis and fault coverage

In normal mode of operation DFT circuits are not utilized. Hence direct timing analysis of the DFT enabled netlist considers DFT related circuits and generates wrong analysis. To overcome this drawback the tool has to be instructed to exclude DFT circuitry from timing analysis. For example, in the Systolic Array Matrix Multiplier design due to scan enable signal, very large –ve slack (-105) is predicted. This problem is tackled using command set_case_analysis 0 test_se. By doing this tool is informed not to consider the scan enable signal test_se for normal timing analysis. Corresponding correct timing report after the execution of this command is shown below.

Startpoint: reset (input port)
Endpoint: out_reg00_reg[2]
(rising edge-triggered flip-flop clocked by clock)
Path Group: clock
Path Type: max
Des/Clust/Port Wire Load Model Library
------------------------------------------------
sam3 280000 cb13fs120_tsmc_max
Point Incr Path
-----------------------------------------------------------
clock (input port clock) (rise edge) 0.00 0.00
input external delay 0.40 0.40 r
reset (in) 0.00 0.40 r
U638/CIN (pc3d11) 0.95 1.35 f
U327/ZN (inv0d1) 0.25 1.59 r
………………………………… … ……………
out_reg00_reg[2]/D (sdnrq1) 0.00 4.19 f
data arrival time 4.19

clock clock (rise edge) 4.75 4.75
clock network delay (ideal) 0.90 5.65
clock uncertainty -0.47 5.18
out_reg00_reg[2]/CP (sdnrq1) 0.00 5.18 r
library setup time -0.19 4.98
data required time 4.98
-----------------------------------------------------------
data required time 4.98
data arrival time -4.19
-----------------------------------------------------------
slack (MET) 0.80


From the timing report it can be observed that slack of DFT enabled circuit has reduced.

The power report reports higher power consumption for DFT enabled circuit. Note that I/O pads are already inserted and with this consideration the total power is estimated as 110mW. Power estimation without I/O pads yields a value of 16mW. With the insertion of DFT circuits reported power is shown below.

****************************************
Report : power
-analysis_effort low
Design : sam3
Version: V-2004.06-SP1
Date : Mon Apr 23 16:26:09 2007
****************************************
Global Operating Voltage = 1.08
Power-specific unit information :
Voltage Units = 1V
Capacitance Units = 1.000000pf
Time Units = 1ns
Dynamic Power Units = 1mW (derived from V,C,T units)
Leakage Power Units = 1pW

Cell Internal Power = 284.3075 mW (99%)
Net Switching Power = 2.1465 mW (1%)
---------
Total Dynamic Power = 286.4540 mW (100%)

Cell Leakage Power = 38.3158 uW


It can be clearly observed that power consumption increased more than twice. Even though DFT circuits don’t contribute anything to normal functionality of the design, they consume static power. Hence when it comes to larger designs, keeping design trade-off in mind, DFT has to be implemented carefully.

It is very natural that DFT causes area overhead. From the previous post (Application of DFT technique) we have noticed that DFT improves testability. Thus the trade-off of testability and area and power are challenging issues for present ASIC designers.

Fault coverage of the DFT enabled design can be estimated using command estimate_test_coverage. The corresponding log data is shown below.

Starting test coverage estimation ...
12190 faults were added to fault list.

Uncollapsed Stuck Fault Summary Report
-----------------------------------------------
fault class code #faults
------------------------------ ---- ---------
Detected DT 12154
Possibly detected PT 0
Undetectable UD 36
ATPG untestable AU 0
Not detected ND 0
-----------------------------------------------
total faults 12190
test coverage 100.00%
-----------------------------------------------
Information: The test coverage above may be inferior
than the real test coverage with customized
protocol and test simulation library.

From the above data it can be observed that total 12190 faults are possible and all are testable making 100% fault coverage. But the tool informs that 100% coverage may not be practically possible.

Reference

[1] Himanshu Bhatnagar, Advanced ASIC chip Syntheis Using Synopsys Design Compiler, Physical Compiler and PrimeTime, Kluwer Academic Publishers, Second edition, 2002
[2] Design Compiler® User Guide, Version X-2005.09, September 2005

Related Articles

Synthesis Constraints
Optimization Methodology
Application of DFT technique

Read the rest of this article >>

Application of DFT technique

DFT techniques provide controllability and observability. Automatic Test Pattern Generation (ATPG) is used for combinational design and DFT is used for sequential circuits.

Basically two methodologies are followed in the industry.

They are:

1. Scan DFT
2. Built In Self Test (BIST)

Under scan DFT two sub categories are available known as full scan and partial scan. Generally tools support only full scan DFT. Built in DFT compiler of Design Compiler provide multiplexed full scan DFT.

Two ways can be followed while inserting DFT elements to the design. The first one is to compile the design first and then insert scan elements. The second method is to insert scan elements to DFT and then compile.

To check whether design has any DFT rule violations dft_drc command is used. dft_drc check can be enabled by using commands set hdlin_enable_rtldrc_info true and set test_enable_dft_drc true. A test clock for DFT is generated using command create_test_clock clock waveform {25 50}. Period of the test clock is always greater than the original clock period. Total number of scan paths and methodology used are instructed using the command create_test_protocol. Longest chain length in a scan path can also be specified. As per power report, this constraint increases power consumption. insert_scan or insert_dft command converts all Flip Flops to scan registers.

Below is the log data from DFT compiler (in built in Design Compiler). The design synthesized is 3x3 Systolic Array Matrix Multiplier.

Information: Using default scan style 'multiplexed_flip_flop'. (TESTDB-279)
Loading db file '/home/Master_Files/Libraries/gtech.db'
Loading target library 'gtech'
Loading design ...
Starting rtldrc ...
Initializing rtldrc ...
Starting rule checks ...


Information: Scan style is 'multiplexed_flip_flop'. (TEST-1212)

Information: Starting test protocol creation. (TEST-219)
...reading user specified clock signals...
Information: Identified system/test clock port clock (25.0,50.0). (TEST-265)
...reading user specified asynchronous signals...
Loading test protocol
Loading target library 'cb13fs120_tsmc_max'
Loading target library 'cb13io320_tsmc_max'
Warning: IO pad 'pc3d10' is unusable: unknown logic function. (OPT-1022)
Warning: IO pad 'pc3d00' is unusable: unknown logic function. (OPT-1022)
Loading design 'sam3'
Pre-DFT DRC enabled

Information: Starting test design rule checking. (TEST-222)
...basic checks...
...basic sequential cell checks...
...checking for scan equivalents...
...checking vector rules...
...checking pre-dft rules...
-----------------------------------------------------------------
DRC Report
Total violations: 0
-----------------------------------------------------------------
Test Design rule checking did not find violations
-----------------------------------------------------------------
Sequential Cell Report
0 out of 467 sequential cells have violations
-----------------------------------------------------------------
SEQUENTIAL CELLS WITHOUT VIOLATIONS
* 467 cells are valid scan cells

From the above log data it can be observed that there are no DFT violations in the example design considered here. By default, multiplexed flip flop scan technique is used by the tool as seen in the above log data.

Reference

[1] Himanshu Bhatnagar, Advanced ASIC chip Syntheis Using Synopsys Design Compiler, Physical Compiler and PrimeTime, Kluwer Academic Publishers, Second edition, 2002
[2] Design Compiler® User Guide, Version X-2005.09, September 2005

Related Articles

Synthesis Constraints
Optimization Methodology
DFT enabled circuit analysis and fault coverage Read the rest of this article >>

Optimization Methodology

Design Compiler uses cost functions to optimize the design. Design Compiler calculates the cost functions based on the design constraints and DRCs to optimize the design. [1]. Optimization also depends upon the compilation strategy adopted. There are 4 types of compilation strategies recommended by Design Compiler [1] [2]. They are:

1. Top-down hierarchical compile method
2. Time budget compile method
3. Compile-characterize-write script-recompile (CCWSR) method
4. Design budgeting method

In top down hierarchical compile strategy the source is compiled by reading the entire design. Constraints and attributes are applied based on the design specification. Only top level constraints are needed in this method. Even though the design had several sub modules, only one set of constraints are applied. Because of this entire design are optimized yielding better results. This method works well for the design which does not has multiple clocks or generated clocks. To get better results compile_map_effort high can be used. This command enables Design Compiler to maximize its effort to meet the specified constraints. Once the compilation is completed several design related reports can be obtained. Important of them are: report_timing, report_area and report_power.

Reference

[1] Himanshu Bhatnagar, Advanced ASIC chip Syntheis Using Synopsys Design Compiler, Physical Compiler and PrimeTime, Kluwer Academic Publishers, Second edition, 2002
[2] Design Compiler User Guide, Version X-2005.09, September 2005

Related Articles

Synthesis Constraints
Application of DFT technique
DFT enabled circuit analysis and fault coveragea Read the rest of this article >>

Synthesis Constraints

Let us discuss something about ASIC front end design and its related issues. I would like post some articles related to synthesis constraints, DFT and formal verification. I will consider Synopsys tools to support the discussion.

Three types of constraints can be set for the design in Design Compiler (DC). They are:

1) DRC constraints
2) Optimization constraints
3) Environmental constraints.

DRC constraints exist in library. DRC constraints can’t be relaxed. They can be chosen from library.

DRC constraints are: set_max_fanout, set_max_transition, set_max_capacitance.

If DRC constraints are not specified, then default values from the library are taken.

Three types of optimizations are possible-area, power and timing. We have optimization constraints related to all these.

set_max_area, set_min_area are area constraints.

Only basic level of power optimization is carried out by DC. Its primary target is to meet timing constraints. set_max_leakege and set_max_dynamic are the two power constraints that can be provided to DC.

Both DRC and optimization constraints follow environmental constraints. Setting up of operating conditions and wire load model falls under environmental constraints. The constraints are: set_operating_conditions, set_wire_load_model and set_wire_load_mode. By default enclosed wire load mode is considered by DC.

Synthesis is timing driven process. Several timing constraints are put to synthesis process of SAMM. No timing specifications may be mentioned for a design. Hence to extract the possible value of clock, derive_timing_constraints command is used. This gives a clock period of ‘x’. A nearest clock period less than ‘x’ can be chosen. This value of clock should satisfy slack requirement of DFT enabled circuit also.

Examples of timing constraints are listed bellow:
->set_clock -period 4.75 clock: Clock period constraint set at 4.75 (210 MHz).

->set_clock_uncertainty –setup 0.475 clock: -ve clock skew can lead to setup violations. Possible value of –ve skew is provided to DC so that it can model for that. Generally setup uncertainty is taken as 10% of the clock.

->set_clock_uncertainty –hold 0.27 clock: +ve clock skew can lead to hold violations. Possible value of +ve skew is provided to DC so that it can model for that. Generally hold uncertainty is taken as 5% of the clock.

->set_clock_latency 0.45 clock: This provides possible network latency constraint to DC.

->set_clock_latency –source 0.4 clock: Source latency of 0.45 is selected.

->set_clock_transition 0.04 clock: Clock transition time of 0.04 is modeled.

->set_input_delay 0.40 [all_inputs]: Input delay of 0.4 is set to all inputs.

->remove_input_delay [get_ports clock]: Constraining clock with input delay leads to wrong timing analysis. To exclude clock port from the input delay this command is used.

->set_output_delay 0.40 [all_outputs]: Output delay of 0.4 is provided. If all outputs are registered this delay does not affect the timing analysis.

I/O ports of the design become pads of the IC. Hence tool has to be informed about this so that it analyzes delay, area and power appropriately. This is done using command set_port_is_pad, which sets the I/O ports as pad and insert_pad, which inserts pad.

Reference

[1] Himanshu Bhatnagar, Advanced ASIC chip Synthesis Using Synopsys Design Compiler, Physical Compiler and PrimeTime, Kluwer Academic Publishers, Second edition, 2002
[2] Design Compiler® User Guide, Version X-2005.09, September 2005

Related Articles

Optimization Methodology
Application of DFT technique
DFT enabled circuit analysis and fault coverage Read the rest of this article >>