文件名称：hardcaml-affirm:HardCaml的验证工具
文件大小：40KB
文件格式：ZIP
更新时间：2024-06-02 09:51:37
OCaml
坚决确认 HardCaml的顺序验证工具。 NuSMV后端 从HardCaml电路生成NuSMV模型。 let circuit = HardCamlAffrim.NuSMV..make "mytest" [ outputs ] [ properties ] let () = NuSMV.write (output_string chan) circuit 在此后端中，电路是由Props.CTL和Props.LTL模块表示的输出和属性的组合。 NuSMV.make函数创建一个电路，以确保它包括属性中包括的所有原子命题。 例子; 等效检查 open HardCamlAffirm let equivalent f1 f2 input = let out1 = f1 input in let out2 = f2 input in `CTL Props.CTL.(ag (p (
【文件预览】：
hardcaml-affirm-master
----CHANGES.md(94B)
----src()
--------transform_state.ml(2KB)
--------transform_state.mli(356B)
--------waves.mli(392B)
--------nuSMV.ml(6KB)
--------props.mli(2KB)
--------props.ml(6KB)
--------bmc.ml(21KB)
--------META(339B)
--------bmc.mli(3KB)
--------jbuild(162B)
--------waves.ml(1KB)
--------nuSMV.mli(258B)
----_ocamlinit(2KB)
----examples()
--------tx_state.ml(1KB)
--------counter.ml(3KB)
--------sim.ml(4KB)
--------jbuild(162B)
----.travis.yml(142B)
----test()
--------cntr.ml(648B)
--------tseitin.ml(1KB)
--------states.ml(1KB)
--------retime.ml(694B)
--------mux.ml(959B)
--------kloop.ml(3KB)
--------bmc.ml(1KB)
--------bomo_32.ml(1KB)
--------lava_tutorial.ml(3KB)
--------gates.ml(9KB)
--------cnf.ml(559B)
--------convert.ml(2KB)
--------propbug.ml(5KB)
--------transform_ltl.ml(752B)
--------satish_l24.ml(2KB)
----LICENSE.md(757B)
----README.md(2KB)
----Makefile(567B)
----hardcaml-affirm.opam(623B)
----.travis-ci.sh(1KB)
----jbuild(95B)
----.gitignore(80B)