- In this paper we present our results and methods on formally verifying
the implementation of an Asynchronous Transfer Mode (ATM) network switching
fabric using the Verification Interacting with Synthesis (VIS) tool. We
also present our experience of using VIS in the reimplementation of this
fabric. The design we considered is in use for real applications in the
Cambridge Fairisle network. We produced the behavioral (RTL) and structural
(netlist) descriptions of the switch fabric at different levels of abstraction.
We then performed equivalence checking between the structural and behavioral
descriptions of each submodule of the implementation hierarchy. Using several
techniques presented in the paper, we provided a number of relevant liveness
and safety properties expressible in CTL, and accomplished their verification
in reasonable CPU time. In addition, we succeeded in discovering several
injected design errors using both property checking and equivalence checking.
The experience on the verification and reimplementation of the fabric demonstrates
that VIS can interact with Synopsys and Verilog-XL simulator easily and
hence can be used in the digital design flow to make the design more reliable.
 Download
postscript file (PS
File) |
| Download source
codes (VIS_TR97_Source.tar.Z) |
| Send comments
and suggestions to: tahar@ece.concordia.ca |