TY - JOUR AU - Man, Ka Lok AU - Lei, Chi-Un AU - Kapoor, Hemangee K. AU - Krilavicius, Tomas AU - Ma, Jieming AU - Zhang, Nan PY - 2016/05/31 Y2 - 2024/03/29 TI - PAFSV: A Formal Framework for Specification and Analysis of SystemVerilog JF - COMPUTING AND INFORMATICS JA - Comput. Inform. VL - 35 IS - 1 SE - Articles DO - UR - https://www.cai.sk/ojs/index.php/cai/article/view/1371 SP - 143-176 AB - 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. ER -