A systematic approach to model microprocessors and their correctness is useful and necessary for practical projects of formal verifications. We extend existing models to support non-superscalar pipelines with dynamic stalling. We introduce a set of algebraic tools and methods to model the specification, implementation and verification, to define formal correctness condition in formal verification and guide the actual work of microprocessors formal verification. This method is a general basis of a uniform theoretical framework for modeling microprocessors, not limited to specific reasoning systems. We consider the microprocessors determined by iterated maps that data abstractions evolve over time from some initial state, at different levels of temporal and data abstraction. We apply this method to model a pipelined microprocessor with dynamic stalling and verify it using algebraic equations.

Feng Zhang, Wensheng Niu. Improvement of Algebraic Models of Abstract Pipelines for Formal Verification. Academic Journal of Computing & Information Science (2018) Vol. 1: 53-70.

[1] Fox A C J, Harman N. A. 2003.Algebraic models of correctness for abstract pipelines[J]. The Journal of Logic and Algebraic Programming, 2003, 57 (1): 71-107.
[2] Harman, N.A.1989. Formal specifications for digital systems. Ph.D. Thesis, School of Computer Studies, University of Leeds, 1989.
[3] Harman, N.A., Tucker, J.V.1988.Clocks, retimings, and the formal specification of a UART. In: Milne, G.J. (ed.), The Fusion of Hardware Design and Verification, pp. 375-396. Amsterdam: North-Holland, 1988.
[4] Harman, N.A., Tucker, J.V.1988. Formal specification and the design of verifiable computers. In: Proceedings of the 1988 UK IT Conference, pp. 500-503, University College Swansea, lEE, 1988.
[5] Harman, N.A., Tucker, J.V.1990. The formal specification of a digital correlator I: Abstract user specification. Theoretical Foundations for VLSI Design, In: McEvoy, K., Tucker, J.V. (eds.), Cambridge University Press Tracts in Theoretical Computer Science 10, pp. 161-262 (1990).
[6] Harman, N.A., Tucker, J.V.1992. Consistent refinements of specifications for digital systems. In: Prinetto, P., Camurati, P. (eds.), Correct Hardware Design Methodologies, pp.273-295. Amsterdam: North-Holland 1992.
[7] John O’Donnell. 2002.Overview of Hydra: A concurrent language for synchronous digital circuit design. In Proceedings of the 16th International Parallel and Distributed Processing Symposium. IEEE Computer Society Press, 2002.
[8] Harman N. A, Tucker J V. 1996.Algebraic models of microprocessors architecture and organization [J] .Acta Informatica, 1996, 33 (5): 421-456.
[9] Harman, N. A. and Tucker, J. V.1997. Algebraic models of microprocessors: the verification of a simple computer. In V.Stavridou, ed., Proceedings of the 1995 IMA Conference on Mathematics for Dependable Systems. Oxford University Press, Oxford, 1997.
[10] Harman N. A, Tucker J V. 1996.Algebraic models and the correctness of microprocessors [M]. Correct Hardware Design and Verification Methods. Springer Berlin Heidelberg, 1993: 92-108.
[11] Fox A C J, Harman N. A. 1998.Algebraic models of superscalar microprocessor implementations: A case study. [M] Prospects for Hardware Foundations. Springer Berlin Heidelberg, 1998: 138-183.
[12] Fox A C J, Harman N. A. 2003.Algebraic models of correctness for abstract pipelines [J]. The Journal of Logic and Algebraic Programming, 2003, 57 (1): 71-107.
[13] Fox A C J. An algebraic framework for modelling and verifying microprocessors using HOL [M]. University of Cambridge, Computer Laboratory, 2001.
[14] Fox A C J. 2003. Formal specification and verification of ARM6 [M]. Theorem proving in higher order logics. Springer Berlin Heidelberg, 2003: 25-40.
[15] Harman N. A.2001. Verifying a simple pipelined microprocessor using Maude. In M Cerioli and G Reggio, editors, Recent trends in algebraic development techniques: 15th International Workshop, WADT 2001, Genova, Italy, April2001. Lecture Notes in Computer Science 2267, pages 128-151, SpringerV erlag.
[16] Fox A C J. 2005. An algebraic framework for verifying the correctness of hardware with input and output: a formalization in HOL [M]. Algebra and Coalgebra in Computer Science. Springer Berlin Heidelberg, 2005: 157-174. }
[17] Harman N. A. 2007.Algebraic models of behaviour and correctness of SMT and CMT processors [J]. The Journal of Logic and Algebraic Programming, 2007, 74 (1): 32-56.
[18] Harman N. A. 2007.Algebraic models of simultaneous multithreaded and multi-core processors [M] // Algebra and Coalgebra in Computer Science. Springer Berlin Heidelberg, 2007: 294-311.
[19] S Miller and M Srivas. 1995. Formal verification of an avionics microprocessor. Technical report, SRI International Computer Science Laboratory CSL-95-04, 1995.
[20] S Miller and M Srivas. 1995.Formal verification of the AAMP5 microprocessor: a case study in the industrial use of formal methods. In Proceedings of WIFT 95, Boca Raton.
[21] M Bickford and M Srivas. 1990.Verification of a pipelined processor using Clio. In M Leeser and G Brown, editors, Proceedings of the Mathematical Sciences Institute workshop on hardware specification, Verification and Synthesis: Mathematical Aspe cts, pages 307 {332. Lecture Notes in Computer Science 408, Springer-V erlag.
[22] M Srivas and M Bickford. 1991. Formal verification of a pipelined microprocessor [J]. IEEE Software, 7 (5): 52 -64, 1991.
[23] Fox A C J.2012. Directions in ISA specification [M]. Interactive Theorem Proving. Springer Berlin Heidelberg, 2012: 338-344.
[24] Rutten JJMM. 2000. Universal coalgebra: a theory of systems [J]. Theoretical Computer Science, 2000, 249 (1): 3-80.
[25] Meinke, K. and Tucker, J. V.1992. Universal algebra. In T. S. E. Maibaum, S. Abramsky and D. Gabbay, eds, Handbook of Logic in Computer Science. Oxford University Press, Oxford, 1992, 189-411.
[26] M Wirsing. 1990. Algebraic specification. In Jvan Leeuwen, editor, Handbook of theoretical computer science, volume B: formal models and semantics, pages 675-788. Elsevier, 1990.
[27] Gratzer G A. Universal algebra [M], pages: 223-269 Springer, 2008.
[28] Ehrig H, Mahr B. 2011. Fundamentals of algebraic specification I: Equations and initial semantics [M]. Springer Publishing Company, Incorporated, 2011.
[29] Fox A C J, Harman N A. 1998. Algebraic models of temporal abstraction for initialised iterated state systems: An abstract pipelined case study [R]. Technical Report CSR 21-98 (submitted to Acta Informatica), University of Wales Swansea, 1998.