A formal framework for verification of embedded custom memories of the Motorola MPC7450 microprocessor

DOI10.1007/S10703-005-2250-1zbMATH Open1086.68517OpenAlexW1980490128MaRDI QIDQ816213FDOQ816213

Authors: Jayanta Bhadra, Andrew K. Martin, Jacob A. Abraham 

Publication date: 20 February 2006

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-005-2250-1

Recommendations

• scientific article; zbMATH DE number 1857502
• scientific article; zbMATH DE number 1701763
• Formal modeling and verification of microprocessors
• Verisym: Verifying circuits by symbolic simulation
• Automatic Verification of Sequential Circuits Using Temporal Logic

zbMATH Keywords

symbolic trajectory evaluationcustom circuit verificationefficient memory modelsembedded memory verificationequivalence checking

Mathematics Subject Classification ID

Computer system organization (68M99)

Cites Work

• Graph-Based Algorithms for Boolean Function Manipulation
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (7)

• Memory arbiter synthesis and verification for a radar memory interface card
• Verisym: Verifying circuits by symbolic simulation
• Semi-formal verification of memory systems by symbolic simulation
• Analog property checkers: a DDR2 case study
• Title not available (Why is that?)
• Computer Aided Verification
• Title not available (Why is that?)

This page was built for publication: A formal framework for verification of embedded custom memories of the Motorola MPC7450 microprocessor

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q816213)