Title :
Overview of Applying Reachability Analysis to Verifying a Physical Microprocessor
Author :
de B Johnston, R. ; Dahmoune, Ouiza
Author_Institution :
Centre Energie Mater. Telecommun. (EMT), Inst. Nat. de la Rech. Scientiflque (INRS), Montreal, QC, Canada
Abstract :
This paper outlines the application of a Model-Checker to the functional verification of a microprocessor´s physical electronic implementation. The goals are (1) testing at hardware speed, (2) reduced labor of test bench creation, and (3) a raised level of abstraction for the specifications. L. Lamport´s TLC Model-Checker is used to verify a custom version of the Xilinx PicoBlaze Micro-Controller Unit (MCU), the MCU is specified in VHDL and implemented on a Field Programmable Gate Array (FPGA). Experimental verification consists of showing that the physical device behavior conforms to a mathematical specification of its Instruction Set Architecture (ISA), for selected subsets of instructions and arguments.
Keywords :
formal verification; hardware description languages; instruction sets; microprocessor chips; VHDL; Xilinx PicoBlaze Micro-Controller Unit; field programmable gate array; instruction set architecture; model-checker; physical microprocessor; reachability analysis; Analytical models; Computational modeling; Field programmable gate arrays; Hardware; Hardware design languages; Mathematical model; Random access memory; Applying Reachability Analysis; Physical Microprocessor; functional verification;
Conference_Titel :
Microprocessor Test and Verification (MTV), 2011 12th International Workshop on
Conference_Location :
Austin, TX
Print_ISBN :
978-1-4577-2101-4
DOI :
10.1109/MTV.2011.15
