Q127FreeFirmware
Co-verify a memory-mapped minimum stack
Question
Build the firmware wrapper and reference model for a signed 16-entry memory-mapped I/O (MMIO) stack supporting push, pop, top, and minimum. Complete the C model and wrapper using the supplied platform adapter declarations. Adapter calls perform ordered, uncached MMIO; clear_completion completes its write-one-to-clear before returning. One caller owns the peripheral, and the platform serializes reset against mstack_exec. The DV model separately supports reset during a pending command. Its caller supplies a valid model pointer, initializes it with model_reset, calls model_go for each GO, and model_complete only on a hardware completion event; compare visible fields afterward with model_matches. Stack/depth/RDATA update at completion, while BUSY marks the captured pending command. A legal busy-time GO is ignored. DONE is set on both success and under/overflow; ERROR is sticky until the selected W1C bits, abort or reset. ABORT synchronously quiesces pending work before returning, without changing already committed stack/RDATA. Reset clears all visible state and cancels ownership; a later completion without a new GO is rejected by model_complete. The timer is monotonic modulo 2^32 and each call lasts less than one full wrap. Poll status before sticky ERROR so error from that completed operation takes priority over DONE; a completed status wins over a timeout first noticed in that poll. Required result storage is valid and separate from peripheral/model state.
Implementation scaffold
#include <stdbool.h>
#include <stddef.h>
#include <stdint.h>
typedef enum { MSTACK_OK, MSTACK_BAD_ARG, MSTACK_HW_ERROR,
MSTACK_TIMEOUT } mstack_status_t;
enum { MSTACK_PUSH = 0, MSTACK_POP = 1, MSTACK_TOP = 2, MSTACK_MIN = 3 };
enum { MSTACK_BUSY = 1u << 0, MSTACK_DONE = 1u << 1,
MSTACK_EMPTY = 1u << 2, MSTACK_FULL = 1u << 3 };
enum { MSTACK_UNDERFLOW = 1u << 0, MSTACK_OVERFLOW = 1u << 1 };
extern uint32_t mstack_status(void);
extern uint32_t mstack_error(void);
extern void mstack_clear_completion(void);
extern void mstack_write_data(int16_t value);
extern void mstack_start(uint8_t op);
extern void mstack_abort(void);
extern int16_t mstack_read_data(void);
extern uint32_t platform_ticks(void);
typedef struct {
int16_t data[16];
uint8_t depth;
int16_t rdata;
bool busy, done;
uint32_t error;
uint8_t pending_op;
int16_t pending_arg;
} mstack_model_t;
void mstack_model_reset(mstack_model_t *model) {
*model = (mstack_model_t){0};
}
// Called only for a legal accepted command, from model_complete.
uint32_t mstack_model_apply(mstack_model_t *model, uint8_t op,
int16_t arg, int16_t *result) {
// TODO: implement the signed stack operations and preserve state on error.
}
bool mstack_model_go(mstack_model_t *model, uint8_t op, int16_t arg) {
// TODO: capture only an idle legal GO.
}
bool mstack_model_complete(mstack_model_t *model) {
// TODO: apply the captured command and update sticky completion/error.
}
void mstack_model_w1c(mstack_model_t *model, bool clear_done,
uint32_t clear_error) {
// TODO: clear only the requested sticky bits.
}
void mstack_model_abort(mstack_model_t *model) {
// TODO: cancel pending work and completion/error state.
}
uint32_t mstack_model_status(const mstack_model_t *model) {
// TODO: derive BUSY, DONE, EMPTY and FULL.
}
bool mstack_model_matches(const mstack_model_t *model, uint32_t status,
uint32_t error, int16_t rdata) {
// TODO: compare all modeled visible fields.
}
mstack_status_t mstack_exec(uint8_t op, int16_t arg,
int16_t *result, uint32_t timeout) {
// TODO: validate, clear stale flags, start, poll with error priority, commit.
}
Trace one case
PUSH 5; PUSH 2; MIN; POP; MINMIN returns 2; POP returns 2; final MIN returns 5The signed-stack model returns the current minimum without changing depth. POP removes the top value, so the final MIN sees the remaining five.
Requirements
- Validate the operation and required result pointer before MMIO, write push data before GO, and clear stale completion state.
- Model only GO commands accepted while idle; TOP and MIN observe without changing depth.
- Underflow or overflow completes with an error while preserving stack contents and RDATA; error has priority over DONE.
- Keep completion and error bits sticky until their selected write-one-to-clear bits, ABORT or reset. Ignore GO while busy. ABORT cancels pending work and clears DONE/ERROR while preserving committed stack/RDATA; reset clears all visible state.