~cypheon/kicad2spice

9502f7f80895c42f7555c624a646caf839636ab4 — Johann Rudloff 1 year, 10 months ago 96e390b
Add basic smtlib-based netlist equivalency check.
5 files changed, 114 insertions(+), 0 deletions(-)

M eeschema2netlist.opam
A test/data/nlcompare/a.cir
A test/data/nlcompare/b.cir
M test/dune
A test/nlcompare.ml
M eeschema2netlist.opam => eeschema2netlist.opam +1 -0
@@ 12,6 12,7 @@ depends: [
  "alcotest" {build}
  "ocaml" { >= "4.08" }
  "extlib" { >= "1.7" }
  "spice" { >= "0.1.0" }
  "ppx_deriving" { build & >= "4.3" }
  "ppx_compare" { build & >= "0.12" }
]

A test/data/nlcompare/a.cir => test/data/nlcompare/a.cir +13 -0
@@ 0,0 1,13 @@
.title KiCad schematic
.include "/Users/cypheon/Downloads/lib/sub/regulators.lib"
C1 +12V 0 0.33µ
C2 Net-_C2-Pad1_ 0 0.1µ
MQ2 Net-_D1-PadA_ Net-_Q2-PadG_ 0 0 BS170
R2 Net-_Q1-PadE_ Net-_Q2-PadG_ 10k
D1 Net-_D1-PadA_ +12V 1N4148
XIC1 +12V 0 Net-_C2-Pad1_ LM7805
Vccin1 +12V 0 dc 12
R1 Net-_JP1-Pad1_ Net-_Q1-PadB_ 1k
Q1 Net-_Q1-PadB_ 0 Net-_Q1-PadE_ BC557B
Q3 +12V Net-_Q1-PadB_ Net-_Q1-PadE_ BC547
.end

A test/data/nlcompare/b.cir => test/data/nlcompare/b.cir +12 -0
@@ 0,0 1,12 @@
.title KiCad schematic (by eeschema2netlist)
C2 Net_C2_pad_1 0 0.1µ
MQ2 Net_D1_pad_A Net_Q2_pad_G 0 0 BS170
R2 Net_Q1_pad_E Net_Q2_pad_G 10k
D1 Net_D1_pad_A +12V 1N4148
XIC1 +12V 0 Net_C2_pad_1 78T
Vccin1 +12V 0 dc 12
R1 Net_JP1_pad_1 Net_Q1_pad_B 1k
Q1 Net_Q1_pad_B 0 Net_Q1_pad_E BC557B
Q3 +12V Net_Q1_pad_B Net_Q1_pad_E BC547
C1 +12V 0 0.33µ
.end

M test/dune => test/dune +7 -0
@@ 15,3 15,10 @@
  (modules test_sexp)
  (libraries eeschema alcotest)
  )

(test
  (name nlcompare)
  (modules nlcompare)
  (flags -w -27)
  (libraries extlib eeschema alcotest spice)
  )

A test/nlcompare.ml => test/nlcompare.ml +81 -0
@@ 0,0 1,81 @@
open Spice
open Netlist

let slurp filename =
  let inch = open_in filename in
  let data = Std.input_all inch in
  close_in inch;
  data

module StrSet = Set.Make(String)

let curry f = fun (a,b) -> f a b

let write_smtlib_comparison write nl_a nl_b =
  write "(set-option :produce-proofs true)\n(declare-sort Net)\n";
  let write_asserts nl nlname1 nlname2 =
    let prefix1 = nlname1 ^ "__" in
    let prefix2 = nlname2 ^ "__" in
    let write_generic_device name nets = List.iteri (fun i _ ->
      write (Printf.sprintf "(assert (= %scomp_%s_pin_%d %scomp_%s_pin_%d))\n" prefix1 name i prefix2 name i)
    ) nets in
    let write_device name = let open Device in function
      | Resistor c -> write_generic_device name [c.net_neg;c.net_pos]
      | Capacitor c -> write_generic_device name [c.net_neg;c.net_pos]
      | VoltageSource c -> write_generic_device name [c.net_neg;c.net_pos]
      | Mosfet c -> write_generic_device name [c.net_drain;c.net_gate;c.net_source;c.net_bulk]
      | SubCircuit c -> write_generic_device name c.nets
      | BJT c -> write_generic_device name [c.net_emitter;c.net_base;c.net_collector]
      | Diode c -> write_generic_device name [c.net_neg;c.net_pos]
    in
    Enum.iter (curry write_device) (ExtHashtbl.Hashtbl.enum nl.Netlist.devices);
  in
  let write_netlist nl nlname =
    let nets = ref StrSet.empty in
    let write_net name = if not (StrSet.mem name !nets) then (nets := StrSet.add name !nets; write ("(declare-const " ^ name ^ " Net)\n")) in
    let prefix = nlname ^ "__" in
    let write_generic_device name nets = List.iteri (fun i net ->
      let mangled_net = (prefix ^ "net_" ^ net) in
      write_net mangled_net;
      write (Printf.sprintf "(define-fun %scomp_%s_pin_%d () Net %s)\n" prefix name i mangled_net)
    ) nets in
    let write_device name d = Printf.eprintf "write_device: %s\n" (Device.show d);let open Device in match d with
      | Resistor c -> write_generic_device name [c.net_neg;c.net_pos]
      | Capacitor c -> write_generic_device name [c.net_neg;c.net_pos]
      | VoltageSource c -> write_generic_device name [c.net_neg;c.net_pos]
      | Mosfet c -> write_generic_device name [c.net_drain;c.net_gate;c.net_source;c.net_bulk]
      | SubCircuit c -> write_generic_device name c.nets
      | BJT c -> write_generic_device name [c.net_emitter;c.net_base;c.net_collector]
      | Diode c -> write_generic_device name [c.net_neg;c.net_pos]
    in
    Enum.iter (curry write_device) (ExtHashtbl.Hashtbl.enum nl.Netlist.devices);
    let distinct_buf = Buffer.create 4096 in
    Buffer.add_string distinct_buf "(assert (distinct";
    StrSet.iter (fun net ->
      Buffer.add_char distinct_buf ' ';
      Buffer.add_string distinct_buf net;
    ) !nets;
    Buffer.add_string distinct_buf "))\n";
    write (Buffer.contents distinct_buf);
  in
  write_netlist nl_a "a";
  write_netlist nl_b "b";
  write_asserts nl_a "a" "b";
  write "(check-sat)\n(get-model)\n(get-proof)\n"


let test () =
  let reference = Parser.netlist_of_string (slurp "../../../test/data/nlcompare/a.cir") in
  let parsed = Parser.netlist_of_string (slurp "../../../test/data/nlcompare/b.cir") in
  Printf.eprintf "reference:\n%s\n" (Netlist.show reference);
  Printf.eprintf "parsed:\n%s\n" (Netlist.show parsed);

  let outch = open_out "../../../out.z3" in
  let write_out s = output_string outch s in
  write_smtlib_comparison write_out reference parsed;
  Alcotest.(check string) "easy" "abc" "abc"

let () =
  Alcotest.run "spice_parser" [
    "all", ["simple netlist", `Quick, test]
  ]