|
|
Rewriting Logic Formulas
SystemC is a library and macro-based extension to C++.
It is a system-level modeling language (somewhat similar to Verilog and VHDL)
capable of providing an event-driven simulator for exploring the behavior of
concurrent processes.
SCOOT is a source-to-source compiler for SystemC whose goal is to improve the performance
of the event-driven simulator produced by SystemC. In particular, a primary area in
which the efficiency of simulators can be improved is in optimizations focusing on race conditions.
SCOOT employs partial-order reduction techniques to optimize race conditions. Specifically, the model
checker SATABS is used to implement a counter-example guided abstraction-refinement loop. Within
this loop, analysis based on weakest preconditions form the basis for identifying and properly
handling commutative transitions.
In practice, logic formulas resulting from weakest precondition analysis can become large and
unweildy. They also can quickly become incomprehensible from the perspective of a human audience.
Thus, for a variety of reasons it is beneficial to be able to simplify and restructure such
formulas, a task well-suited to program transformation. Motivated by these considerations, a
logic formula normalization and simplification transformation has been developed in TL.
Normalization includes:
- Standard Boolean simplifications such as:
- not(not(x)) -> x
- x && true -> x
- x && false -> false
- Restructuring of conditional expressions. The goal of restructuring here is to flatten conditional expressions enabling conjunctive formulas to
describe a single execution path.
Optimization includes:
- Equality and relational reduction such as:
- a == 1 && a == 2 -> false
- a == 1 && !(a == 2) -> a==1
- Transitive closure of unit resolution between execution paths.
Examples of (SystemC source code, initial weakest precondition, transformed weakest precondition) tuples are given below.
|
