TY - GEN
T1 - Verification driven formal architecture and microarchitecture modeling
AU - Mahajan, Yogesh
AU - Chan, Carven
AU - Bayazit, Ali
AU - Malik, Sharad
AU - Qin, Wei
PY - 2007
Y1 - 2007
N2 - Our ability to verify complex hardware lags far behind our capacity to design and fabricate it. We argue that this gap is partly due to the limitations of RTL models when used for verification. Higher level models such as SystemC and SystemVerilog aim to raise the level of abstraction to enhance designer productivity; however, they largely provide for executable but not analyzable descriptions. We propose the use of formally analyzable design models at two distinct levels above RTL: the architecture and the microarchitecture level. At both these levels, we describe concurrent units of data computation termed transactions. The architecture level describes the computation/state updates in the transactions and their interaction through shared data. The microarchitecture level adds to this the resource usage in the transactions as well as their interaction based on shared resources. We then illustrate the applicability of these models in a top-down verification methodology which addresses several concerns of current methodologies.
AB - Our ability to verify complex hardware lags far behind our capacity to design and fabricate it. We argue that this gap is partly due to the limitations of RTL models when used for verification. Higher level models such as SystemC and SystemVerilog aim to raise the level of abstraction to enhance designer productivity; however, they largely provide for executable but not analyzable descriptions. We propose the use of formally analyzable design models at two distinct levels above RTL: the architecture and the microarchitecture level. At both these levels, we describe concurrent units of data computation termed transactions. The architecture level describes the computation/state updates in the transactions and their interaction through shared data. The microarchitecture level adds to this the resource usage in the transactions as well as their interaction based on shared resources. We then illustrate the applicability of these models in a top-down verification methodology which addresses several concerns of current methodologies.
UR - http://www.scopus.com/inward/record.url?scp=34548821239&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=34548821239&partnerID=8YFLogxK
U2 - 10.1109/MEMCOD.2007.371235
DO - 10.1109/MEMCOD.2007.371235
M3 - Conference contribution
AN - SCOPUS:34548821239
SN - 1424410509
SN - 9781424410507
T3 - Proceedings - Fifth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'07
SP - 123
EP - 132
BT - Proceedings - Fifth ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'07
T2 - 5th ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE'07
Y2 - 30 May 2007 through 1 June 2007
ER -