A Functional Specification and Validation Model for Networks on Chip in the ACL2 Logic 1
Julien Schmaltz, D. Borrione · 2004
Abstract. We present a functional model used to specifiy and validate, in the ACL2 logic, a system on a chip communication architecture named Octagon. The functional model is briefly introduced before being developed on the case study. We define and validate the routing algorithm, a simple scheduling algorithm and the correctness of read and write operations which includes the proof that messages travel over the network without being modified and eventually reach their expected destination. 1