PAFSV: A Formal Framework for Specification and Analysis of SystemVerilog

In: Computing and Informatics, vol. 35, no. 1

K.l. Man - C.-U. Lei - H.k. Kapoor - T. Krilavičius - J. Ma - N. Zhang

Detaily:

Rok, strany: 2016, 143 - 176

Kľúčové slová:

SystemVerilog, process algebras, formal semantics, PAFSV, formal specification and analysis, circuit verification

O článku:

We develop a process algebraic framework PAFSV for the formal specification and analysis of IEEE 1800TM SystemVerilog designs. The formal semantics of PAFSV is defined by means of deduction rules that associate a time transition system with a PAFSV process. A set of properties of PAFSV is presented for a notion of bisimilarity. PAFSV may be regarded as the formal language of a significant subset of IEEE 1800TM SystemVerilog. To show that PAFSV is useful for the formal specification and analysis of IEEE 1800TM SystemVerilog designs, we illustrate the use of PAFSV with a multiplexer, a synchronous reset D flip-flop and an arbiter.

Ako citovať:

ISO 690:

Man, K., Lei, C., Kapoor, H., Krilavičius, T., Ma, J., Zhang, N. 2016. PAFSV: A Formal Framework for Specification and Analysis of SystemVerilog. In Computing and Informatics, vol. 35, no.1, pp. 143-176. 1335-9150.

APA:

Man, K., Lei, C., Kapoor, H., Krilavičius, T., Ma, J., Zhang, N. (2016). PAFSV: A Formal Framework for Specification and Analysis of SystemVerilog. Computing and Informatics, 35(1), 143-176. 1335-9150.