Created
March 15, 2018 13:33
-
-
Save buttercutter/c0583aa4696cb6192b56aad2c915a7c5 to your computer and use it in GitHub Desktop.
BMC and Induction result log for http://zipcpu.com/blog/2018/03/10/induction-exercise.html
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| phung@UbuntuHW15:~/Documents/phung/verification_example$ sby kitest.sby | |
| SBY 21:29:44 [kitest] Copy 'kitest.v' to 'kitest/src/kitest.v'. | |
| SBY 21:29:44 [kitest] engine_0: smtbmc yices | |
| SBY 21:29:44 [kitest] script: starting process "cd kitest/src; yosys -ql ../model/design.log ../model/design.ys" | |
| SBY 21:29:44 [kitest] script: finished (returncode=0) | |
| SBY 21:29:44 [kitest] smt2: starting process "cd kitest/model; yosys -ql design_smt2.log design_smt2.ys" | |
| SBY 21:29:44 [kitest] smt2: finished (returncode=0) | |
| SBY 21:29:44 [kitest] engine_0.basecase: starting process "cd kitest; yosys-smtbmc -s yices --presat --unroll --noprogress -t 30 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2" | |
| SBY 21:29:44 [kitest] engine_0.induction: starting process "cd kitest; yosys-smtbmc -s yices --presat --unroll -i --noprogress -t 30 --append 0 --dump-vcd engine_0/trace_induct.vcd --dump-vlogtb engine_0/trace_induct_tb.v --dump-smtc engine_0/trace_induct.smtc model/design_smt2.smt2" | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Solver: yices | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Solver: yices | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 0.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 30.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 0.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 29.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 1.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 1.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 28.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 2.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 2.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 27.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 3.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 3.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 26.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 4.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 4.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 25.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 24.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 5.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 5.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 23.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 22.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 6.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 6.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 21.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 20.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 7.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 7.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 19.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 18.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 8.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 8.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 17.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 16.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 9.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 9.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 15.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 14.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 10.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 10.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 13.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 12.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 11.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 11.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 11.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 10.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 12.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 12.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 9.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 13.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 13.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 8.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 7.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 14.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 14.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 6.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 15.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 15.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 5.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 4.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 16.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 3.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 16.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 2.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 17.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 17.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 1.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Trying induction in step 0.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Temporal induction failed! | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Assert failed in kitest: kitest.v:61 | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Writing trace to VCD file: engine_0/trace_induct.vcd | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 18.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 18.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 19.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 19.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 20.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 20.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 21.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 21.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 22.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 22.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 23.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 23.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Writing trace to Verilog testbench: engine_0/trace_induct_tb.v | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 24.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 24.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 25.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 25.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Writing trace to constraints file: engine_0/trace_induct.smtc | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 26.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 26.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 27.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 27.. | |
| SBY 21:29:44 [kitest] engine_0.induction: ## 0 0:00:00 Status: FAILED (!) | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 28.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 28.. | |
| SBY 21:29:44 [kitest] engine_0.induction: finished (returncode=1) | |
| SBY 21:29:44 [kitest] engine_0: Status returned by engine for induction: FAIL | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assumptions in step 29.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Checking assertions in step 29.. | |
| SBY 21:29:44 [kitest] engine_0.basecase: ## 0 0:00:00 Status: PASSED | |
| SBY 21:29:44 [kitest] engine_0.basecase: finished (returncode=0) | |
| SBY 21:29:44 [kitest] engine_0: Status returned by engine for basecase: PASS | |
| SBY 21:29:44 [kitest] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0) | |
| SBY 21:29:44 [kitest] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0) | |
| SBY 21:29:44 [kitest] summary: engine_0 (smtbmc yices) returned FAIL for induction | |
| SBY 21:29:44 [kitest] summary: engine_0 (smtbmc yices) returned PASS for basecase | |
| SBY 21:29:44 [kitest] DONE (UNKNOWN, rc=4) | |
| phung@UbuntuHW15:~/Documents/phung/verification_example$ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment