Bigmem-concrete-asymmetric
A byte memory model that is logically a record but provides
array-like performance for a (low-address) region of memory and association
list lookup and update for memory modeled above a certain address limit.
The concrete-asymmetric library takes its inspriation from the
bigmem library, but provides a simpler implementation that operates
faster than bigmem when memory addresses are below some limit and
operates more slowly when equal to or above this same address limit. When
accessing/updating a An
intended use of this memory model is to provide a physical-memory model for
the ACL2 x86-ISA model.
An obvious application of concrete-asymmetric is to model a byte-wide
memory; bm can be used as a child STOBJ to define a field representing a
byte memory in a parent STOBJ that models some machine's state. See
projects/x86isa/machine/state.lisp for one suchbigmem example.
