Polynomial abstraction for verification of sequentially implemented combinational circuits
2004 (English)In: DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION, VOLS 1 AND 2, PROCEEDINGS / [ed] Gielen, G; Figueras, J, LOS ALAMITOS: IEEE COMPUTER SOC , 2004, 690-691 p.Conference paper (Refereed)
Todays integrated circuits with increasing complexity cause the well known state space explosion problem in verification tools. In order to handle this problem a much simpler abstract model of the design has to be created for verification. We introduce the polynomial abstraction technique, which efficiently simplifies the verification task of sequential design blocks whose functionality can be expressed as a polynomial. Through our technique, the domains of possible values of data input signals can be reduced. This is done in such a way that the abstract model is still valid for model checking of the design functionality in terms of the system's control and data properties. We incorporate polynomial abstraction into the ForSyDe methodology, for the verification of clock domain design refinements.
Place, publisher, year, edition, pages
LOS ALAMITOS: IEEE COMPUTER SOC , 2004. 690-691 p.
Computer and Information Science
IdentifiersURN: urn:nbn:se:kth:diva-44691DOI: 10.1109/DATE.2004.1268933ISI: 000189434000116ScopusID: 2-s2.0-3042561713ISBN: 0-7695-2085-5OAI: oai:DiVA.org:kth-44691DiVA: diva2:451908
Design, Automation and Test in Europe Conference and Exhibition (DATE 04) Location: Paris, FRANCE Date: FEB 16-20, 2004
QC 201110272011-10-272011-10-252016-05-11Bibliographically approved