search

YosysHQ / yosys

Yosys Open SYnthesis Suite
https://yosyshq.net/yosys/
ISC License
3.49k stars 890 forks source link

sby: mathsat failures emit python errors in yosys-smc (Python IndexError exception thrown) #3785

Open dlmiles opened 1 year ago

dlmiles commented 1 year ago

Version

Yosys 0.29+21 (git sha1 147cceb51, clang 10.0.0-4ubuntu1 -fPIC -Os)

On which OS did this happen?

Linux

Reproduction Steps

This is a really basic unit test to validate the operation of each solver. In this instance only 'mathsat' is under test. The same test works with other solvers such as yices and boolector.

This example is expected to fail with the solver (DONE,FAIL,rc!=0), due to HDL being deliberate broken, via the reset value 1 being lower than the allowed ranges from assert.

The unit test is validating the Formal testing framework (of SpinalHDL) can correctly interpret the output results from logs/exitStatus/stdout/stderr.

The python Error/Exception is not seen with a successful use of mathsat solver when the result is (DONE,PASS,rc=0).

# mathsat -version
MathSAT5 version 5.6.9 (0214d34392af) (Nov 10 2022 09:51:42, gmp 6.2.0, gcc 7.5.0, 64-bit)

unnamed.sby:

[tasks]
bmc

[options]
bmc: mode bmc
bmc: depth 15

[engines]
smtbmc --progress mathsat

[script]
read -formal unnamed.sv
prep  -top unnamed

[files]
/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/rtl/unnamed.sv

unnamed.sv

// Generator : SpinalHDL dev    git head : b6fac6a0394b9422f9a429c1182b9ab898ca8c1e
// Component : unnamed

`timescale 1ns/1ps

module unnamed (
  input               reset,
  input               clk
);

  LimitedCounterEmbedded dut (
    .clk   (clk  ), //i
    .reset (reset)  //i
  );
  initial begin
    assume(reset); // FormalSimpleMathsatTester.scala:L29
  end

endmodule

module LimitedCounterEmbedded (
  input               clk,
  input               reset
);

  reg        [3:0]    value;
  wire                when_FormalSimpleMathsatTester_l16;

  assign when_FormalSimpleMathsatTester_l16 = (value < 4'b1010);
  always @(posedge clk or posedge reset) begin
    if(reset) begin
      value <= 4'b0001;
    end else begin
      if(when_FormalSimpleMathsatTester_l16) begin
        value <= (value + 4'b0001);
      end
      assert((4'b0010 <= value)); // FormalSimpleMathsatTester.scala:L21
      assert((value <= 4'b1010)); // FormalSimpleMathsatTester.scala:L22
    end
  end

endmodule

unamed_bmc/config.sby

[options]
mode bmc
depth 15

[engines]
smtbmc --progress mathsat

[script]
read -formal unnamed.sv
prep  -top unnamed

[files]
/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/rtl/unnamed.sv

logfile.txt

SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] Removing directory '/work/spinalhdl/FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc'.
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] Copy '/work/spinalhdl/FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/rtl/unnamed.sv' to '/work/spinalhdl/FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc/src/unnamed.sv'.
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] engine_0: smtbmc --progress mathsat
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] base: starting process "cd /work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] base: finished (returncode=0)
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] prep: starting process "cd /work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc/model; yosys -ql design_prep.log design_prep.ys"
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] prep: finished (returncode=0)
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] smt2: starting process "cd /work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] smt2: finished (returncode=0)
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] engine_0: starting process "cd /work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc; yosys-smtbmc -s mathsat --presat --unroll -t 15  --append 0 --dump-vcd engine_0/trace.vcd --dump-yw engine_0/trace.yw --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] engine_0: ##   0:00:00  Solver: mathsat
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] engine_0: ##   0:00:00  Checking assumptions in step 0..
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] engine_0: ##   0:00:00  Checking assertions in step 0..
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] engine_0: ##   0:00:00  Checking assumptions in step 1..
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] engine_0: ##   0:00:00  Checking assertions in step 1..
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] engine_0: ##   0:00:00  Checking assumptions in step 2..
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] engine_0: ##   0:00:00  Checking assertions in step 2..
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] engine_0: ##   0:00:00  BMC failed!
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] engine_0: ##   0:00:00  Assert failed in unnamed.dut: unnamed.sv:38.10-39.33 ($assert$unnamed.sv:38$18)
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace.vcd
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] engine_0: finished (returncode=1)
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] ERROR: engine_0: Engine terminated without status.
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] summary: engine_0 (smtbmc --progress mathsat) did not return a status
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] summary: counterexample trace: /work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc/engine_0/trace.vcd
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] summary:   failed assertion unnamed.dut.$assert$unnamed.sv:38$18 at unnamed.sv:38.10-39.33 in step 2
SBY 18:29:41 [/work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed_bmc] DONE (ERROR, rc=16)

Expected Behavior

I don't expect to see the Python exception/stack-traces in the output.

Actual Behavior

Process sby -f /work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail/unnamed.sby /work/spinalhdl/./FormalSimpleMathsatTester/Formal_mathsat_Simple_fail
Traceback (most recent call last):
  File "/opt/oss-cad-suite/libexec/yosys-smtbmc", line 1887, in <module>
    write_trace(0, last_check_step+1+append_steps, "%d" % traceidx if keep_going else '%')
  File "/opt/oss-cad-suite/libexec/yosys-smtbmc", line 1316, in write_trace
    write_vcd_trace(steps_start, steps_stop, index)
  File "/opt/oss-cad-suite/libexec/yosys-smtbmc", line 976, in write_vcd_trace
    value_list = smt.get_net_bin_list(topmod, path_list, "s%d" % i)
  File "/opt/oss-cad-suite/libexec/../share/yosys/python3/smtio.py", line 1047, in get_net_bin_list
    return [self.bv2bin(v) for v in self.get_net_list(mod_name, net_path_list, state_name)]
  File "/opt/oss-cad-suite/libexec/../share/yosys/python3/smtio.py", line 1035, in get_net_list
    return self.get_list([self.net_expr(mod_name, state_name, n) for n in net_path_list])
  File "/opt/oss-cad-suite/libexec/../share/yosys/python3/smtio.py", line 920, in get_list
    return [n[1] for n in self.parse(self.read())]
  File "/opt/oss-cad-suite/libexec/../share/yosys/python3/smtio.py", line 920, in <listcomp>
    return [n[1] for n in self.parse(self.read())]
IndexError: string index out of range
dlmiles commented 1 year ago

This commit looks like it may address this problem:

https://github.com/YosysHQ/yosys/pull/3519/commits/2ba435b6bc0a5f0f831c331abdf8d58e0fdae132

From #3519