pycaliper.jginterface package
Submodules
pycaliper.jginterface.jasperclient module
- exception pycaliper.jginterface.jasperclient.JasperError
Bases:
Exception
- exception pycaliper.jginterface.jasperclient.SocketError
Bases:
Exception
- pycaliper.jginterface.jasperclient.close_tcp()
- pycaliper.jginterface.jasperclient.connect_tcp(host='localhost', port=8080)
- pycaliper.jginterface.jasperclient.eval(command)
- pycaliper.jginterface.jasperclient.is_online()
- pycaliper.jginterface.jasperclient.main(args)
- pycaliper.jginterface.jasperclient.shutdown_tcp()
pycaliper.jginterface.jgdesign module
pycaliper.jginterface.jgoracle module
- class pycaliper.jginterface.jgoracle.ProofResult(value)
Bases:
Enum- CEX = 1
- MAX_TRACE_LENGTH = 4
- NONE = 0
- PROVEN = 3
- SAFE = 2
- SIM = 6
- UNKNOWN = 5
- pycaliper.jginterface.jgoracle.create_vcd_trace(prop, filepath)
- pycaliper.jginterface.jgoracle.disable_all_bmc(taskcon, svacon)
Disable all BMC assumptions
- pycaliper.jginterface.jgoracle.disable_assm(taskcon, assm)
Disable an assumption
- Parameters:
taskcon (str) – proof node name
assm (str) – assumption name
- Returns:
result of the JasperGold command
- Return type:
_type_
- pycaliper.jginterface.jgoracle.enable_assm(taskcon, assm)
Enable an assumption
- Parameters:
taskcon (str) – proof node name
assm (str) – assumption name
- Returns:
result of the JasperGold command
- Return type:
_type_
- pycaliper.jginterface.jgoracle.get_wctx(taskcon, prop)
Get the hierarchical assumption name for a property wire
- Return type:
str- Parameters:
taskcon (str) – proof node name under which the property is defined
prop (str) – property name
- Returns:
hierarchical assumption name
- Return type:
str
- pycaliper.jginterface.jgoracle.is_pass(res)
Is the result a pass
- Return type:
bool
- pycaliper.jginterface.jgoracle.loadscript(script)
- pycaliper.jginterface.jgoracle.prove(taskcon, prop)
Prove a property
- Return type:
- Parameters:
taskcon (str) – proof node the property is defined under
prop (str) – property name
- Returns:
result of the proof
- Return type:
- pycaliper.jginterface.jgoracle.prove_out_bmc(taskcon, svacon, sched)
- Return type:
list[ProofResult]
- pycaliper.jginterface.jgoracle.prove_out_induction_1t(taskcon)
- Return type:
- pycaliper.jginterface.jgoracle.prove_out_induction_2t(taskcon)
- Return type:
- pycaliper.jginterface.jgoracle.set_assm_bmc(taskcon, svacon, sched)
Enable all assumptions required for 1 BMC trace properties
- pycaliper.jginterface.jgoracle.set_assm_induction_1t(taskcon, svacon)
Enable only 1-trace assumptions (required for 1 trace properties)
- Parameters:
taskcon (str) – proof node name
- pycaliper.jginterface.jgoracle.set_assm_induction_2t(taskcon, svacon)
Enable all assumptions required for 2 trace properties
- Parameters:
taskcon (str) – proof node name
- pycaliper.jginterface.jgoracle.setjwd(jwd)
pycaliper.jginterface.jgsetup module
- pycaliper.jginterface.jgsetup.setup_jasper(mod, jgc, dc)
- Return type:
bool