Subject: Integration of Simulation & Formal Verification
From: wolfstal@il.ibm.com
Date: Tue Feb 13 2001 - 10:35:38 PST
Hi All,
in the previous meeting, I talked about the important IBM sees in linking
between
FV & Simulation. I was asked to send out some material which describes IBM
work in this area.
In response, I would like to point to our paper of CAV'2000 (look at bullet
#4
in
http://www.haifa.il.ibm.com/projects/verification/RB_Homepage/publications.html
).
This paper described our FoCs tool and methodology. FoCs stands for 'FOrmal
CheckerS". Basically, FoCs takes temporal properties written in Sugar and
synthesizes them into simulation checkers. One benefit here is in the ease
of
generating complex, multiple-KLOC checkers out of concise temporal Sugar
expressions. The other key benefit is reuse of the temporal properties used
in Model Checking for chip-level simulation.
Regards - Yaron
This archive was generated by hypermail 2b28 : Tue Feb 13 2001 - 12:15:08 PST