WASIM

WASIM is a word-level abstract symbolic simulation framework with customizable abstraction/refinement functions. The development of WASIM is to facilitate symbolic-simulation-based hardware verification. Typical formal property verification (model checking) is autonomous (no human intervention) after you specify the properties to check. However, autonomous model checking is hard to scale on large designs and prior works have proposed the use of symbolic trajectory evaluation in VossII/Forte for industry-scale hardware design verification, which is an example of symbolic simulation applied for verification.

WASIM is word-level (SMT-based) with customizable abstraction / concretization functions. So the human verification engineers can incorporate their insights on the design to better scale up verification capabilities.

The original WASIM framework is based on PySMT which wraps the SMT solvers with Python APIs. We are currently developing the next generation of WASIM with its core functionalities implemented completely in C++, using the SMT-Switch framework. Join us if you are interested.

Python Interface of WASIM

WASIM provides Python API to interact with the simulator. Below is a code snippet that shows how to work with WASIM through Python.

# Load design in btor2 format and parse into STS
btor_parser = BTOR2Parser()
sts,_= btor_parser.parse_file(Path("/UserPath/design.btor2"))

# Initialize WASIM simulator with symbolic values
executor = SymbolicExecutor(sts)
init_setting = executor.convert({
    'wen_stage1':'v1',
    'wen_stage2':'v2',
    'wen_stage3': 1,
    'stage1':'a',
    'stage2':'b',
    'stage3':'c'
  })
executor.init(init_setting)

# Execute simulation for traces of abstract states
s0 = executor.get_curr_state()
s0 = abstract(s0,base_sv)
executor.set_input(
    executor.convert({'rst':0, 'wen_stage3':1}), [])
executor.sim_one_step()

s1 = executor.get_curr_state()
......
s4 = executor.get_curr_state()

The code snippet shows that WASIM consumes hardware designs in Btor2 format. And then we can set symbolic initial values (e.g., a) for state variables in Verilog (e.g., wen_stage1) and perform symbolic simulation through WASIM internal Python APIs such as sim_one_step. We could obtain traces of symbolic states using get_curr_state. Each state in the trace consists of state variable assignments and assumptions. Figures below demonstrate the first and last symbolic states of the extracted trace. The tables in the figures represent the state variables (sv) and corresponding symbolic assignments (value). The assumptions are located at the bottom. Each assumption has a textual explanation before the SMT formula.