Assume-Guarantee Reasoning

Overview

Assume-guarantee (AG) reasoning is a technique for compositional model checking in which system specifications are checked under certain assumptions on system parameters or inputs, and the verification provides guarantees on observations of system state. By decomposing a global property into local assumptions on components and guarantees on their observable behavior, AG reasoning scales to systems whose monolithic analysis would be infeasible.

Categorical Framework (Lenses and Generalized Moore Machines)

A categorical framework for AG reasoning for safety problems has been developed by viewing systems as lenses, generalizing earlier work on the compositionality of generalized Moore machines. The key data structure is a tangency — a fibration with a section — that determines the flavor of generalized Moore machine under consideration. The framework gives AG reasoning specially adapted to each of the following cases:

• Ordinary Moore machines,
• Partially observable Markov (decision) processes, and
• Systems of parameterized ODEs (control systems).

In particular, the framework introduces a novel formulation of AG reasoning for (local) input-to-state stability ((L)ISS) Lyapunov functions on systems of parameterized ODEs. The construction is categorically natural and straightforwardly compositional: symmetric monoidal loose right modules of AG-certified generalized Moore machines over symmetric monoidal double categories of certified wiring diagrams can be built 2-functorially from fibrations internal to the 2-category of tangencies.

Algebra of AG Contracts

An algebraic treatment studies the algebra of assume-guarantee contracts. In this view:

• Contracts are defined together with new and known operations, and the relationships between these operations are worked out explicitly.
• Contracts are functorial: any Boolean algebra induces an associated contract algebra.
• The contract algebra supports monoid and semiring structures, and the mappings between such structures are characterized.
• The action of a Boolean algebra on its contract algebra is also studied.

SAT-Based AG in Hardware Bug Injection (ENCARSIA)

In the ENCARSIA framework for CPU bug injection, AG reasoning is used to drive the formal verification step that determines whether an injected transformation is architecturally observable. Model checking is expensive in terms of computations and memory, and its performance can be boosted by providing invariants or by partitioning the problem using assume-guarantee reasoning. Automatically deriving invariants is hard; however, when transforming the CPU, ENCARSIA is aware of one key piece of information: the trigger. For example, in a multiplexer-tree transformation, the transformation can only affect the design's output once the modified rows of the corresponding table are selected.

To reduce the search space for the formal verifier, ENCARSIA adopts a two-step assume-guarantee approach:

1. Trigger step. The SAT solver is instructed to find inputs that satisfy the trigger condition, using a property similar to c_propagated but on the mixed-up signal instead of the architecturally visible signal.
2. Propagation step. If the first step succeeded, the SAT solver is constrained to preserve the triggering sequence and is instructed to propagate the discrepancy to a user-defined list of architecturally-visible signals.

ENCARSIA provides two formal-verification setups: a performance-oriented one based on the closed-source JasperGold, and a more accessible one based on Yosys. The same two-step assume-guarantee approach is used to guide the formal verification process in the Yosys-based setup. To ensure that one bug does not hide another, ENCARSIA limits injection to a single bug per design at a time.

The formal setup mirrors fuzzer initialization: the CPUs are initially reset and several critical control and status registers are configured to predefined values. For example, the FS field of the mstatus register is set to 1 to enable floating-point instructions. These configurations are modeled with initial-value abstractions and constraints for the first clock cycle to accelerate verification. To prevent the verifier from using debug or testing features that are typically encapsulated within an SoC and therefore inaccessible to fuzzers, the considered input behavior is restricted using SVA assume statements (for example, limiting Ibex to a single hardware thread via p_hart).

For verification, the formal tool is instructed to cover the c_propagated property, which proves that the transformation can provoke an architecturally observable deviation from the original design; if the property is not covered, the transformation is deemed ineffective and excluded from the evaluation.

See Also

• ENCARSIA — uses assume-guarantee reasoning as the driver of its formal verification stage for CPU bug injection.