Formal Specification and Verification of Microprocessor Systems |
Common terms and phrases
3-bit opcode abstract state machine abstraction functions ADD instruction address field arithmetic functions behavioural specification Boolean values CMOS behaviour CMOS NAND gate complete components defined in terms described example executable existential quantification external memory externally visible formal methods formal proof formal specification formal verification function from discrete hardware description language hardware specification hardware verification hierarchical higher level aspects higher-order logic INCn inference rules input and output instruction set Iterate level accurately models level behaviour level of specification logic gates logical NAND lower levels microcode microinstruction microprocessor implementation microprocessor systems Mike Gordon model of CMOS multi-level simulation n-bit adder n-bit words NEXT_STATE Ntran numbers program counter programming language Ptran register-transfer level architecture relation on MOS rules of higher-order semantics specification and verification structural specification switch level model switch level primitives symbolic simulation Tamarack implementation Tamarack microprocessor target level operation target machine theorem transistors type-check VLSI design methodology well-defined wire