On the Design and Verification Methodology of the Look-Aside Interface

In this paper, we present a technique to design and verify the Look-Aside (LA-1) Interface standard used in network processors. Our design flow includes several refinements starting from an informal UML specification until getting to an RTL modeled in Verilog. We integrate the verification of the LA-Interface in the design considering two intermediate levels: (1) Abstract State Machines (ASM); and (2) SystemC. The first one serves the verification by model checking of a set of PSL properties, while the second includes a set of assertions to be verified by simulation. To evaluate the performance of our approach, we used the RuleBase model checker to verify the same properties; and the OVL library to verify the same assertions.

• Type: Conference
• Year: 2004
• Where: DATE
• Authors: Ali Habibi, Asif Iqbal Ahmed, Otmane Aït Mohamed, Sofiène Tahar
• Keywords: Abstract State Machines, DATE 2004, Hardware, Informal Uml Specification, RuleBase Model Checker