Equivalence checking using trace partitioning
One application of equivalence checking is to establish correspondence between a high-level, abstract design and a low-level implementation. We propose a new partitioning technique for the case in which the two designs are substantially different and traditional equivalence-point insertion fails. Th...
| Main Authors: | , , , |
|---|---|
| 格式: | Conference item |
| 出版: |
IEEE
2015
|
| _version_ | 1826306864618405888 |
|---|---|
| author | Mukherjee, R Kroening, D Melham, T Srivas, M |
| author_facet | Mukherjee, R Kroening, D Melham, T Srivas, M |
| author_sort | Mukherjee, R |
| collection | OXFORD |
| description | One application of equivalence checking is to establish correspondence between a high-level, abstract design and a low-level implementation. We propose a new partitioning technique for the case in which the two designs are substantially different and traditional equivalence-point insertion fails. The partitioning is performed in tandem in both models, exploiting the structure present in the high-level model. The approach generates many but tractable SAT/SMT queries. We present experimental data quantifying the benefit of our partitioning method for both combinational and sequential equivalence checking of difficult arithmetic circuits and control-intensive circuits. |
| first_indexed | 2024-03-07T06:54:21Z |
| format | Conference item |
| id | oxford-uuid:fd9d5f04-8bf7-43db-b79d-bd34af8972c9 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T06:54:21Z |
| publishDate | 2015 |
| publisher | IEEE |
| record_format | dspace |
| spelling | oxford-uuid:fd9d5f04-8bf7-43db-b79d-bd34af8972c92022-03-27T13:30:10ZEquivalence checking using trace partitioningConference itemhttp://purl.org/coar/resource_type/c_5794uuid:fd9d5f04-8bf7-43db-b79d-bd34af8972c9Symplectic Elements at OxfordIEEE2015Mukherjee, RKroening, DMelham, TSrivas, MOne application of equivalence checking is to establish correspondence between a high-level, abstract design and a low-level implementation. We propose a new partitioning technique for the case in which the two designs are substantially different and traditional equivalence-point insertion fails. The partitioning is performed in tandem in both models, exploiting the structure present in the high-level model. The approach generates many but tractable SAT/SMT queries. We present experimental data quantifying the benefit of our partitioning method for both combinational and sequential equivalence checking of difficult arithmetic circuits and control-intensive circuits. |
| spellingShingle | Mukherjee, R Kroening, D Melham, T Srivas, M Equivalence checking using trace partitioning |
| title | Equivalence checking using trace partitioning |
| title_full | Equivalence checking using trace partitioning |
| title_fullStr | Equivalence checking using trace partitioning |
| title_full_unstemmed | Equivalence checking using trace partitioning |
| title_short | Equivalence checking using trace partitioning |
| title_sort | equivalence checking using trace partitioning |
| work_keys_str_mv | AT mukherjeer equivalencecheckingusingtracepartitioning AT kroeningd equivalencecheckingusingtracepartitioning AT melhamt equivalencecheckingusingtracepartitioning AT srivasm equivalencecheckingusingtracepartitioning |