Demonstrate SAT checking of hardcaml and verilog combinatorial logic using yosys and hardcaml-bloop

.ocamlinit

#require "hardcaml,ppx_deriving_hardcaml,hardcaml-waveterm,hardcaml-bloop,hardcaml-yosys";;
#mod_use "satvlog.ml";;

satadder.ml

open HardCaml

(* the design we want to test, in comparison to a verilog implementation *)

module Make_adder(B : Comb.S) = struct

  open B

  (* full adder *)
  let fa a b cin = ((a &: b) |: (cin &: (a ^: b))), (a ^: b ^: cin)

  (* carry ripple adder *)
  let adder a b = 
    concat @@ snd @@ 
    List.fold_left2 (
      fun (cin,res) a b -> let cout,sum = fa a b cin in cout, sum::res) 
      (gnd,[]) 
      (List.rev (bits a)) 
      (List.rev (bits b))

  (* interface for the circuit *)

  module I = struct
    type 'a t = {
      a : 'a[@bits 8];
      b : 'a[@bits 8];
    }[@@deriving hardcaml]
  end

  module O = struct
    type 'a t = {
      c : 'a[@bits 8];
    }[@@deriving hardcaml]
  end

  let f i = 
    { O.c = adder i.I.a i.I.b }

end

module Adder = Make_adder(HardCaml.Signal.Comb)

(* wrap verilog circuit with hardcaml toplevel *)
module Inst = Interface.Inst(Adder.I)(Adder.O)
let sv i = Inst.make "vlog_adder" i

(* sat check *)
module S = Satvlog.Gen(Adder.I)(Adder.O)
module B = Bits.Comb.IntbitsList

let test () = 
  let fv = S.vlog_to_f ~vlog:["satadder.v"] sv in
  match S.make fv Adder.f with
  | `unsat -> Printf.printf "OK\n%!"
  | `sat(err) ->
    ignore @@ Adder.I.(map2 (fun (n,_) b -> Printf.printf "%s : %s\n" n (B.to_string b)) t err)

satadder.v

module vlog_adder (
  input [7:0] a,
  input [7:0] b,
  output [7:0] c
);

  assign c = a + b;

endmodule

satvlog.ml

(* Compare a combinatorial verilog vs hardcaml circuit using SAT.
 
   The scheme is as follows;

     * Use yosys to convert the verilog design to a JSON representation
     * Load the JSON with hardcaml-yosys
     * SAT check against the hardcaml circuit

   In terms of this project we can use it to extract interesting/complex
   combinatorial logic from the ANTs RTL code base (converted from
   system verilog, and somewhat massaged into the appropriate format).

*)

open HardCaml
open Printf

let tempfile ext = 
  Filename.temp_file "hardcaml_ants_" ext

let convert_to_json ~vlog ~json = 
  let script_name = tempfile ".yosys" in
  let script = open_out script_name in
  List.iter (fprintf script "read_verilog %s\n") vlog;
  fprintf script "hierarchy -top sat_top\n";
  fprintf script "proc\n";
  fprintf script "flatten\n";
  fprintf script "opt -mux_undef\n";
  fprintf script "clean\n";
  fprintf script "write_json %s\n" json;
  close_out script;
  let stat = Unix.system ("yosys -s " ^ script_name ^ " > /dev/null") in
  Unix.unlink script_name;
  match stat with
  | Unix.WEXITED 0 -> true
  | _ -> false

let load_json ~json = 
  let open HardCamlYosys in
  let circ = Io.read (open_in json) in
  let fns = Import.load Techlib.Simlib.cells circ in
  match fns with
  | [] -> failwith "no design loaded"
  | [x] -> x
  | _ -> failwith "multiple designs loaded"

let json_to_circ (n,(i,_,f)) = 
  let open Signal.Comb in
  let inputs = List.map (fun (n,b) -> n, input n b) i in
  let outputs = f inputs in
  Circuit.make n (List.map (fun (n,s) -> output n s) outputs)

let compare_circs c1 c2 = 
  let open Signal.Comb in
  let name s = List.hd (Signal.Types.names s) in
  let get_outputs c = List.map (fun s -> name s, s) (Circuit.outputs c) in
  let o1, o2 = get_outputs c1, get_outputs c2 in
  ~: (List.fold_left (fun x (n,s) -> x &: try (List.assoc n o2) ==: s with _ -> vdd) vdd o1)

let convert_to_circ ~vlog = 
  let json = tempfile ".json" in
  if convert_to_json ~vlog ~json then
    let open Signal.Comb in
    json_to_circ (load_json ~json)
  else
    failwith "failed to convert verilog to json"

let compare_and_sat ~vlog_circ ~circ =
  let open HardCamlBloop in
  let sat = compare_circs circ vlog_circ in
  let sat = Cnf.convert sat in
  Cnf.(report (name_map M.empty sat) @@ run sat)

let check ~vlog ~circ =
  let vlog_circ = convert_to_circ ~vlog in
  compare_and_sat ~vlog_circ ~circ

module B = Bits.Comb.IntbitsList

module Gen(I : Interface.S)(O : Interface.S) = struct

  let json_to_f ~json = 
    let n,(_,_,f) = load_json ~json in
    let mk i = 
      let o = f I.(to_list @@ map2 (fun (n,b) i -> n,i) t i) in
      O.(map (fun (n,b) -> List.assoc n o) t)
    in
    mk

  module C = Interface.Circ(I)(O)

  (* write wrapper for verilog file *)
  let write_sat_top hcf = 
    let fname = tempfile ".v" in
    let f = open_out fname in
    let circ = C.make "sat_top" hcf in
    Rtl.Verilog.write (output_string f) circ;
    close_out f;
    fname

  let vlog_to_f ~vlog top = 
    let json = tempfile ".json" in
    let ftop = write_sat_top top in 
    if convert_to_json ~vlog:(vlog@[ftop]) ~json then
      let open Signal.Comb in
      json_to_f ~json
    else
      failwith "failed to convert verilog to json"

  let get_result r = 
    List.iter (fun (n,d) -> printf "%s [%i] '%s'\n" n (String.length d) d) r;
    let err = 
      I.map (fun (n,b) ->
          try 
            let d = List.assoc n r in
            let d = String.map (fun c -> if c = '0' || c = '1' then c else '0') d in
            B.uresize (B.const d) b;
          with _ -> B.zero b) I.t
    in
    `sat(err)

  (* sat check a hardcaml implementation against a verilog reference *)
  let make fv fh = 
    let open Signal.Comb in
    let i = I.(map (fun (n,b) -> input n b) t) in
    let o1 = fv i in
    let o2 = fh i in
    let o = ~: O.(reduce (&:) @@ to_list @@ map2 (==:) o1 o2) in
    let open HardCamlBloop in
    let sat = Cnf.convert o in
    match Cnf.(report (name_map M.empty sat) @@ run sat) with
    | `unsat -> `unsat
    | `sat(r) -> get_result r

  let with_out_file name fn =
    let f = open_out name in
    let r = fn f in
    close_out f;
    r

  let tb name f err = 
    with_out_file (name ^ ".v") 
      (fun file ->
        let open Signal.Comb in
        let o = f I.(map constibl err) in
        let o = O.(map2 (fun (n,_) s -> output n s) t o) in
        let circ = Circuit.make name (O.to_list o) in
        Rtl.Verilog.write (output_string file) circ)

end