pycaliper.btorinterface package
Submodules
pycaliper.btorinterface.btordesign module
pycaliper.btorinterface.pycbtorinterface module
pycaliper:
- PyCaliperSymex:
Symbolic execution engine performing PER verification on BTOR
- class pycaliper.btorinterface.pycbtorinterface.BTORVerifResult(verified, model)
Bases:
objectVerification result of a BTOR program
- verified
True if verification was successful, False otherwise
- Type:
bool
- model
Model of the BTOR program as a string
- Type:
str
-
model:
str
-
verified:
bool
- class pycaliper.btorinterface.pycbtorinterface.PYCBTORInterface(gui=None)
Bases:
objectSymbolically execute a BTOR program: the barebones
- convert_expr_to_btor2(expr, frame, pref)
Convert a PyCaliper expression to a BTOR2 expression
- dump_and_wait(assm)
- get_assm_constraints(assms, frame, pref)
Get the constraints for the assumptions
- Return type:
list
- get_assrt_constraints(assrts, frame, pref)
Get the constraints for the assertions
- get_lid(pth_, pref)
Get the LID (label-id) for a given path
- Return type:
int
- get_tt_assm_constraints(assms, frame)
Get the constraints for the assumptions
- get_tt_assrt_constraints(assrts, frame)
Get the constraints for the assumptions
pycaliper.btorinterface.vcdgenerator module
This script reads a dump file (or dump string) with lines of the form:
<line_number> <value> <signal_name>
For example: 121 001 state_1 … 1324 010 state_2
Interpretation: • The first token is simply a line number and is ignored. • The third token is of the form “baseName_cycle”. The “cycle” (last underscore-delimited token)
is converted to an integer and used as the VCD simulation time. The rest (baseName) is used as the signal name.
Each signal’s width is inferred from the length of the “value” string.
- class pycaliper.btorinterface.vcdgenerator.BTORModelParser
Bases:
object- parse(model)
Parse the BTOR model and return the signals and events.
- Return type:
BTORModel
- pycaliper.btorinterface.vcdgenerator.convert_to_vcd_from_btorfile(filename)
Convert a BTOR model file to a VCD trace.
- Return type:
str
- pycaliper.btorinterface.vcdgenerator.convert_to_vcd_from_btorstr(model)
Convert a BTOR model string to a VCD trace.
- Return type:
str
- pycaliper.btorinterface.vcdgenerator.events_from_assignments(assignments)
- pycaliper.btorinterface.vcdgenerator.parse_dump_file(filename)
Reads the dump file given by filename and parses its content. Returns a tuple (signals, events).
- pycaliper.btorinterface.vcdgenerator.parse_dump_string(input_str)
Parses dump content provided as a string. Returns a tuple (signals, events).
- pycaliper.btorinterface.vcdgenerator.parse_lines(lines)
- Processes an iterable of lines (from a file or a string) and returns:
- signals: an OrderedDict mapping base signal names -> dict with keys:
‘width’: inferred width (int) ‘vcd_id’: placeholder for later assignment.
events: a list of (time, signal, value) tuples, where time is taken from the signal name suffix.
- It assumes each line is of the form:
<line_number> <value> <full_signal>
where only the <value> and the split result of <full_signal> (base name and cycle) are used.
- pycaliper.btorinterface.vcdgenerator.process_signal_and_time(full_signal)
Process a signal name from the dump. The full signal is expected to be of the form:
baseName_cycle
where the last underscore-delimited token (cycle) is used as the simulation time. Returns a tuple (base_signal, cycle) where:
base_signal is the signal name without the cycle suffix.
cycle is the simulation time (as an integer).
If no underscore is found, the entire string is the base name and cycle is 0.
- pycaliper.btorinterface.vcdgenerator.unique_id_generator()
Generates a sequence of unique short identifiers to be used as VCD ids. It first yields single printable characters and then combinations of increasing length.
- pycaliper.btorinterface.vcdgenerator.write_vcd(signals, assignments, timescale='1ns')
Generate a VCD trace from the given signals and events. ‘signals’ is a dict mapping signal names -> width. ‘events’ is a list of tuples (time, signal, value).
The VCD output uses simulation time stamps (cycles) derived from the signal name suffix.