Another industrial application of ACL2 involved the formal modeling of
the Motorola CAP digital signal processor. Using ACL2, Bishop Brock
produced a bit- and cycle-accurate model of the CAP that runs
faster than a conventional SPW model,
proved the correctness of a predicate for recognizing
pipeline hazards in microcode and
proved the correctness of several CAP microcode programs.
[Next]
[Research]
[Home]