Technical reports

Formal verification of VIPER’s ALU

Wai Wong

April 1993, 78 pages

DOI: 10.48456/tr-300

Abstract

This research describes the formal verification of an arithmetic logic unit of the VIPER microprocessor. VIPER is one of the first processors designed using formal methods. A formal model in HOL has been created which models the ALU at two levels: on the higher level, the ALU is specified as a function taking two 32-bit operands and returning a result; on the lower level the ALU is implemented by a number of 4-bit slices which should take the same operands and return the same results. The ALU is capable of performing thirteen different operations. A formal proof of functional equivalence of these two levels has been completed successfully. The complete HOL text of the ALU formal model and details of the proof procedures are included in this report. It has demonstrated that the HOL system is powerful and efficient enough to perform formal verification of realistic hardware design.

Full text

PDF (5.4 MB)

BibTeX record

@TechReport{UCAM-CL-TR-300,
  author =	 {Wong, Wai},
  title = 	 {{Formal verification of VIPER's ALU}},
  year = 	 1993,
  month = 	 apr,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-300.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-300},
  number = 	 {UCAM-CL-TR-300}
}