Scipediacontent: Scipediacontent moved page Draft Content 355756324 to Nurvitadhi et al 2011a

2021-02-03T17:36:30Z

Scipediacontent moved page Draft Content 355756324 to Nurvitadhi et al 2011a

Scipediacontent: Created page with " == Abstract == When a processor implementation is synthesized from a specification using an automatic framework, this implementation still should be verified against its spe..."

2021-02-03T17:36:27Z

Created page with " == Abstract == When a processor implementation is synthesized from a specification using an automatic framework, this implementation still should be verified against its spe..."

New page

== Abstract ==

When a processor implementation is synthesized from a specification using an automatic framework, this implementation still should be verified against its specification to ensure the automatic framework introduced no error. This paper presents our effort in integrating fully automated formal verification with a high-level processor pipeline synthesis framework. As an integral part of the pipeline synthesis, our framework also emits SMV models for checking the functional equivalence between the output pipelined processor implementation and its input non-pipelined specification. Well known compositional model checking techniques are automatically applied to curtail state explosion during model checking. The paper reports case studies of applying this integrated framework to synthesize and formally verify pipelined RISC and CISC processors.

== Original document ==

The different versions of the original document can be found in:

* [http://users.ece.cmu.edu/%7Ejhoe/distribution/2011/sasp11.pdf http://users.ece.cmu.edu/%7Ejhoe/distribution/2011/sasp11.pdf]

* [http://xplorestaging.ieee.org/ielx5/5934629/5941068/05941073.pdf?arnumber=5941073 http://xplorestaging.ieee.org/ielx5/5934629/5941068/05941073.pdf?arnumber=5941073],
: [http://dx.doi.org/10.1109/sasp.2011.5941073 http://dx.doi.org/10.1109/sasp.2011.5941073]

* [https://ieeexplore.ieee.org/document/5941073 https://ieeexplore.ieee.org/document/5941073],
: [https://www.researchgate.net/profile/Shih-Lien_Lu/publication/224244951_Integrating_formal_verification_and_high-level_processor_pipeline_synthesis/links/00b7d5395c6c49368c000000.pdf https://www.researchgate.net/profile/Shih-Lien_Lu/publication/224244951_Integrating_formal_verification_and_high-level_processor_pipeline_synthesis/links/00b7d5395c6c49368c000000.pdf],
: [http://yadda.icm.edu.pl/yadda/element/bwmeta1.element.ieee-000005941073 http://yadda.icm.edu.pl/yadda/element/bwmeta1.element.ieee-000005941073],
: [https://dblp.uni-trier.de/db/conf/sasp/sasp2011.html#NurvitadhiHKL11 https://dblp.uni-trier.de/db/conf/sasp/sasp2011.html#NurvitadhiHKL11],
: [https://dl.acm.org/citation.cfm?id=2061044.2062133 https://dl.acm.org/citation.cfm?id=2061044.2062133],
: [https://academic.microsoft.com/#/detail/2015009399 https://academic.microsoft.com/#/detail/2015009399]

← Older revision	Revision as of 17:36, 3 February 2021
(No difference)

Nurvitadhi et al 2011a - Revision history

Scipediacontent: Scipediacontent moved page Draft Content 355756324 to Nurvitadhi et al 2011a

Scipediacontent: Created page with " == Abstract == When a processor implementation is synthesized from a specification using an automatic framework, this implementation still should be verified against its spe..."