Contents

Click a page name

Verifying Configuration Register Logic Using Formal Methods 
Agenda 
The CoreConnect Architecture from IBM Microelectronics A "System on Chip" 
Some of the Cores/Chips/ISOCs Developed in IBM HRL 
History of Formal Methods Usage in HRL/VLSI 
Motivation: Checking Intermediate Results 
AG(req->AX(ack)) 
The Problem: Configuration Register Logic 
Number of Registers Fields to Check Example 
Implementation of the Configuration Registers 
Methods to Check Configuration Register Logic 
The Problem in the Straightforward Use of RuleBase for Checking Configuration R 
Elements of the Solution 
Assumptions 
FoCs Tool Flow (traditional) 
"New" FoCs Tool Flow 
Configuration Register - Category 1 
Configuration Register - Category 2 
Configuration Register - Category 3 (general case) 
Assumptions  
Process Flow - and Some Associated Numbers 
Fields of the Special Table Notation 
RunTime Condition Table 
Example I: General Mode - Set Formula 
Example II: General Mode - Stable Formula 
Example III: Empty Mode - with Delay 0 
Example IV: Empty Mode - Single Line, Delay D1 
Example V: Empty mode, Not a Single Line 
Example VI: Mutually Exclusive Mode (1)  
The TestBench  
Results & Conclusions