1structure vsynth = 2struct 3 4(*****************************************************************************) 5(* Conversion ("pretty printing") of output of compiler to Verilog *) 6(*****************************************************************************) 7 8(*****************************************************************************) 9(* START BOILERPLATE *) 10(*****************************************************************************) 11 12(****************************************************************************** 13* Load theories 14******************************************************************************) 15(* 16quietdec := true; 17loadPath :="dff" :: !loadPath; 18app load ["compile","wordsLib", 19 "FileSys","TextIO","Process","Char","String"]; 20open arithmeticTheory pairLib pairTheory PairRules combinTheory listTheory 21 composeTheory compileTheory compile; 22quietdec := false; 23*) 24 25(****************************************************************************** 26* Boilerplate needed for compilation 27******************************************************************************) 28 29local 30open HolKernel Parse boolLib bossLib compileTheory; 31 32(****************************************************************************** 33* Open theories 34******************************************************************************) 35 36open arithmeticTheory pairLib pairTheory PairRules combinTheory listTheory 37 unwindLib composeTheory compileTheory compile; 38 39in 40 41(*****************************************************************************) 42(* END BOILERPLATE *) 43(*****************************************************************************) 44 45(*****************************************************************************) 46(* Error reporting function *) 47(*****************************************************************************) 48 49val ERR = mk_HOL_ERR "vsynth"; 50 51(*****************************************************************************) 52(* Date and time *) 53(*****************************************************************************) 54 55fun date() = Date.fmt "%c" (Date.fromTimeLocal (Time.now ())); 56 57(*****************************************************************************) 58(* Convert a term to a string showing types of variables *) 59(* by setting show_types to true during printing *) 60(*****************************************************************************) 61 62fun term2string tm = 63 let val saved_val = !show_types 64 val _ = (show_types := true) 65 val s = Parse.term_to_string tm 66 val _ = (show_types := saved_val) 67 in 68 s 69 end; 70 71(*****************************************************************************) 72(* Test if a string is a constant *) 73(*****************************************************************************) 74 75fun is_constant s = mem s (known_constants()); 76 77(*****************************************************************************) 78(* Boilerplate definitions of primitive components *) 79(*****************************************************************************) 80 81fun string2int s = 82 let val (SOME n) = Int.fromString s in n end; 83 84(*****************************************************************************) 85(* Test if a ty is ``:word<n>`` for some n *) 86(*****************************************************************************) 87 88val is_word_type = wordsSyntax.is_word_type; 89 90(*****************************************************************************) 91(* Extraxt <n> from ``:word<n>`` *) 92(*****************************************************************************) 93 94val dest_word_type = 95 Arbnum.toInt o fcpLib.index_to_num o wordsSyntax.dest_word_type; 96 97(*****************************************************************************) 98(* Test if a type can be represented in Verilog. *) 99(* Currently this means the type is ``:word<n>``, ``:num`` or ``:bool`` *) 100(*****************************************************************************) 101 102fun is_supported_type ty = 103 is_word_type ty orelse (ty = ``:num``) orelse (ty = ``:bool``); 104 105(*****************************************************************************) 106(* ``:wordn`` --> "n-1" (e.g. ``:word32`` --> "31") *) 107(* ``:num`` --> 31 *) 108(* ``:bool`` --> "0" *) 109(*****************************************************************************) 110 111fun ty2size ty = 112 let val n = 113 if (ty = ``:bool``) then 1 114 else if (ty = ``:num``) then 115 32 116 else if is_word_type ty then 117 dest_word_type ty handle _ => 32 118 else raise ERR "ty2size" "unsupported type" 119 in 120 Int.toString(n-1) 121 end; 122 123(*****************************************************************************) 124(* ``v : num -> wordn`` --> "n-1" (e.g. ``v:word32`` --> "31") *) 125(* ``v : num -> num`` --> 31 (warning issued if !numWarning is true) *) 126(* ``v : num -> bool`` --> "0" *) 127(*****************************************************************************) 128 129val numWarning = ref true; 130fun var2size tm = 131 let val (str, [_,ty]) = dest_type(type_of tm) 132 val _ = if ((ty = ``:num``) orelse 133 (is_word_type ty andalso not (null (type_vars_in_term tm)))) 134 andalso (!numWarning) 135 then 136 (print "Warning: type of "; 137 print_term tm ; 138 print " is ``"; 139 print_type ty; 140 print "``, but is compiled to [31:0].\n") 141 else () 142 in 143 ty2size ty 144 end; 145 146 147(*****************************************************************************) 148(* ``:ty1 --> ty2`` --> (``:ty1``,``:ty2``) *) 149(*****************************************************************************) 150 151fun dest_unop_type uty = 152 let val (opr, utyl) = dest_type uty 153 val _ = if opr = "fun" 154 then () 155 else(print_type uty; 156 print "\nis not a function type\n"; 157 raise ERR "dest_unop_type" "not a function type") 158 val [argty,resty] = utyl 159 in 160 (argty,resty) 161 end 162 163(*****************************************************************************) 164(* ``:ty1 # ty2 --> ty3`` --> (``:ty1``,``:ty2``,``:ty3``) *) 165(*****************************************************************************) 166 167fun dest_binop_type bty = 168 let val (opr, btyl) = dest_type bty 169 val _ = if opr = "fun" 170 then () 171 else(print_type bty; 172 print "\nis not a function type\n"; 173 raise ERR "dest_binop_type" "not a function type") 174 val [argsty,resty] = btyl 175 val (opr, argstyl) = dest_type argsty 176 val _ = if opr = "prod" 177 then () 178 else(print_type argsty; 179 print "\nis not a product type\n"; 180 raise ERR "dest_binop_type" "not a product type") 181 val [argty1,argty2] = argstyl 182 in 183 (argty1,argty2,resty) 184 end 185 186(*****************************************************************************) 187(* Non-primitive components *) 188(*****************************************************************************) 189 190(*****************************************************************************) 191(* ``v0 <> ... <> vn`` --> [``v0``, ... ,``vn``] *) 192(*****************************************************************************) 193 194fun strip_BUS_CONCAT tm = 195 if is_BUS_CONCAT tm 196 then let val (tm1,tm2) = dest_BUS_CONCAT tm 197 in 198 strip_BUS_CONCAT tm1 @ strip_BUS_CONCAT tm2 199 end 200 else [tm]; 201 202(* 203** (|- InRise clk 204** ==> 205** (?v0 .... vn. M1(...) /\ ... /\ Mp(...)) 206** ==> 207** DEV Spec (load at clk, 208** (inp1 <> ... <> inpu) at clk, 209** done at clk, 210** (out1 <> ... <> outv) at clk)) 211** 212** --> 213** 214** (Spec, 215** (``clk``,``load``,[``inp1``,...,``inpu``],``done``,[``out1``,...,``outv``]), 216** [``v0``, ... ,``vn``], 217** [``M1(...)``, ... ,``Mp(...)``]) 218*) 219 220fun dest_cir thm = 221 let val tm = concl(SPEC_ALL thm) 222 val (tm1,tm2) = dest_imp tm 223 val (tm3,tm4) = dest_imp tm2 224 val spec_tm = rand(rator tm4) 225 val clk_tm = rand tm1 226 val [load_tm,inp_tm,done_tm,out_tm] = 227 map (rand o rator) (strip_pair(rand tm4)) 228 val (vars,bdy) = strip_exists tm3 229 val tml = strip_conj bdy 230 val inpl = strip_BUS_CONCAT inp_tm 231 val outl = strip_BUS_CONCAT out_tm 232 in 233 (spec_tm, (clk_tm,load_tm,inpl,done_tm,outl), vars, tml) 234 end; 235 236(*****************************************************************************) 237(* Name of a variable *) 238(*****************************************************************************) 239fun var_name v = fst(dest_var v); 240 241(*****************************************************************************) 242(* Create a output stream to a file called file_name, apply a printer to *) 243(* it and then flush and close the stream. *) 244(*****************************************************************************) 245fun printToFile file_name printer = 246 let val outstr = TextIO.openOut file_name 247 fun out s = TextIO.output(outstr,s) 248 in 249 (printer out; 250 TextIO.flushOut outstr; 251 TextIO.closeOut outstr) 252 end; 253 254(*****************************************************************************) 255(* [] --> [] *) 256(* ["s"] --> ["s"] *) 257(* ["s1",...,"sn"] --> ["s1", "," , ... , ",", "sn"] *) 258(*****************************************************************************) 259fun add_commas [] = [] 260 | add_commas [s] = [s] 261 | add_commas (s::sl) = s :: "," :: add_commas sl; 262 263 264(*****************************************************************************) 265(* ``DTYPE c (clk,inp,out)`` --> ``DTYPE c (clk,inp,out)`` *) 266(* ``?v. DTYPE v (clk,inp,out)`` --> ``DTYPE c (clk,inp,out)`` *) 267(*****************************************************************************) 268fun dest_DTYPE tm = 269 if is_comb tm 270 andalso is_const(fst(strip_comb tm)) 271 andalso (fst(dest_const(fst(strip_comb tm))) = "DTYPE") 272 andalso is_pair(rand tm) 273 andalso (length(strip_pair(rand tm)) = 3) 274 andalso all is_var (strip_pair(rand tm)) 275 then tm else 276 if is_exists tm 277 then dest_DTYPE(snd(strip_exists tm)) 278 else raise ERR "dest_DTYPE" "bad arg" 279 280val is_DTYPE = can dest_DTYPE; 281 282 283(*****************************************************************************) 284(* Test a term has the form ``CONSTANT c out``, *) 285(* where c is 0 or T, F or NUMERAL n or n2w n *) 286(*****************************************************************************) 287fun is_CONSTANT tm = 288 is_comb tm 289 andalso is_const(fst(strip_comb tm)) 290 andalso (fst(dest_const(fst(strip_comb tm))) = "CONSTANT") 291 andalso ((rand(rator tm) = ``0``) 292 orelse (rand(rator tm) = ``F``) 293 orelse (rand(rator tm) = ``T``) 294 orelse is_comb(rand(rator tm)) 295 andalso is_const(rator(rand(rator tm))) 296 andalso mem 297 (fst(dest_const(rator(rand(rator tm))))) 298 ["NUMERAL","n2w"]) 299 andalso is_var (rand tm); 300 301(*****************************************************************************) 302(* ``CONSTANT c out`` --> ("c", ``out``) where c is Verilog form of c *) 303(*****************************************************************************) 304fun dest_CONSTANT tm = 305 let val num = rand(rator tm) 306 val n = if (num = ``F``) then ``0`` 307 else if (num = ``T``) then ``1`` 308 else if (num = ``0``) orelse (fst(dest_const(rator num)) = "NUMERAL") 309 then num 310 else rand num 311 in 312 (Arbnum.toString(numSyntax.dest_numeral n), rand tm) 313 end; 314 315 316(*****************************************************************************) 317(* ``COMB f (i1<>...<>im,out1<>...<>outn)`` *) 318(* --> *) 319(* (f, ["i1",...,"im"], ["out1",...,"outn"]) *) 320(*****************************************************************************) 321fun dest_COMB tm = 322 if is_comb tm 323 andalso is_const(fst(strip_comb tm)) 324 andalso (fst(dest_const(fst(strip_comb tm))) = "COMB") 325 andalso (length(strip_prod(hd(fst(strip_fun(type_of(rand(rator tm))))))) 326 = length(strip_BUS_CONCAT(fst(dest_pair(rand tm))))) 327 then (rand(rator tm), 328 map var_name (strip_BUS_CONCAT(fst(dest_pair(rand tm)))), 329 map var_name (strip_BUS_CONCAT(snd(dest_pair(rand tm))))) 330 else (print "dest_COMB fails on: \n"; 331 print_term tm; print "\n"; 332 raise ERR "dest_COMB" "bad argument"); 333 334val is_COMB = can dest_COMB; 335 336(*****************************************************************************) 337(* Library associating HOL terms with ML functions for generating *) 338(* combinational Verilog. Typical example: *) 339(* *) 340(* add_vsynth *) 341(* [(``\(in1,in2). in1 >> in2``, *) 342(* (fn[i1,i2] => ("{{31{" ^ i1 ^ "[31]}}," ^ i1 ^ "} >> " ^i2))), *) 343(* (``UNCURRY $>>``, *) 344(* (fn[i1,i2] => ("{{31{" ^ i1 ^ "[31]}}," ^ i1 ^ "} >> " ^i2)))] *) 345(* *) 346(* which will cause both *) 347(* *) 348(* ``COMB (\(in1,in2). in1 >> in2) (x<>y, z)`` *) 349(* *) 350(* and *) 351(* *) 352(* ``COMB (UNCURRY $>>) (x<>y, z)`` *) 353(* *) 354(* to generate the Verilog statement *) 355(* *) 356(* assign z = {{31{x[31]}},x} >> y; *) 357(*****************************************************************************) 358val vsynth_lib = ref([] : (term * (string list -> string)) list); 359 360(*****************************************************************************) 361(* Add a list of entries to front of vsynth_lib *) 362(*****************************************************************************) 363fun add_vsynth pl = (vsynth_lib := pl @ (!vsynth_lib)); 364 365(*****************************************************************************) 366(* Lookup in vsynth_lib *) 367(*****************************************************************************) 368fun lookup_vsynth_lib [] tm = 369 raise ERR "lookup_vsynth" "not in vsynth_lib" 370 | lookup_vsynth_lib ((t, f : string list -> string)::vl) tm = 371 if aconv t tm then f else lookup_vsynth_lib vl tm; 372 373fun lookup_vsynth tm = lookup_vsynth_lib (!vsynth_lib) tm; 374 375 376(*****************************************************************************) 377(* Useful initial vsynth_lib *) 378(*****************************************************************************) 379val _ = 380 add_vsynth 381 [(``$~``, 382 fn[i] => ("~ " ^ i)), 383 (``UNCURRY $/\``, 384 fn[i1,i2] => (i1 ^ " && " ^ i2)), 385 (``UNCURRY $\/``, 386 fn[i1,i2] => (i1 ^ " || " ^ i2)), 387 (``\(sel:bool,in1:bool,in2:bool). if sel then in1 else in2``, 388 fn [i1,i2,i3] => (i1 ^ " ? " ^ i2 ^ " : " ^ i3)), 389 (``\(sel:bool,in1:num,in2:num). if sel then in1 else in2``, 390 fn [i1,i2,i3] => (i1 ^ " ? " ^ i2 ^ " : " ^ i3)) 391 ]; 392 393 394(****************************************************************************** 395Needed for crypto examples 396add_vsynth 397 [(``\(in1,in2). in1 >> in2``, 398 (fn[i1,i2] => ("{{31{" ^ i1 ^ "[31]}}," ^ i1 ^ "} >> " ^i2))), 399 (``UNCURRY $>>``, 400 (fn[i1,i2] => ("{{31{" ^ i1 ^ "[31]}}," ^ i1 ^ "} >> " ^i2)))]; 401******************************************************************************) 402 403(*****************************************************************************) 404(* Positive edge triggered Dtype register. *) 405(* Default: 32-bits wide, initial value = 1. *) 406(*****************************************************************************) 407val DTYPEvDef = 408"// Variable width edge triggered Dtype register (default initial value 1)\n\ 409\// DTYPE v (clk,d,q) = (q 0 = v) /\\\ 410\ !t. q(t+1) = if Rise clk t then d t else q t\n\n\ 411\module dtype (clk,d,q);\n\ 412\ parameter size = 31;\n\ 413\ parameter value = 1;\n\ 414\ input clk;\n\ 415\ input [size:0] d;\n\ 416\ output [size:0] q;\n\ 417\ reg [size:0] q = value;\n\ 418\\n\ 419\ always @(posedge clk) q <= d;\n\ 420\\n\ 421\endmodule\n\ 422\\n"; 423 424(*****************************************************************************) 425(* Print an instance of a Dtype with a given size and default initial value *) 426(*****************************************************************************) 427val DTYPEvInst_count = ref 0; 428fun DTYPEvInst tm (out:string->unit) [("size",size)] [clk_name,in_name,out_name] = 429 let val count = !DTYPEvInst_count 430 val _ = (DTYPEvInst_count := count+1); 431 val inst_name = "dtype" ^ "_" ^ Int.toString count 432 in 433 (out "/*\n"; 434 out(term2string tm); out "\n*/\n"; 435 out "dtype "; out inst_name; 436 out " (";out clk_name;out",";out in_name;out",";out out_name; out ");"; 437 out " defparam ";out inst_name; out ".size = "; out size; 438 out ";\n\n") 439 end; 440 441fun termToVerilog_DTYPE (out:string->unit) tm = 442 let val dest_tm = dest_DTYPE tm 443 in 444 DTYPEvInst 445 tm 446 out 447 [("size", var2size(last(strip_pair(rand dest_tm))))] 448 (map (fst o dest_var) (strip_pair(rand dest_tm))) 449 end; 450 451 452(*****************************************************************************) 453(* Clock. Default has 10 units of simulation time between edges *) 454(*****************************************************************************) 455val ClockvDef = 456"// Clock\n\ 457\module Clock (clk);\n\ 458\ parameter period = 10; // time between clock edges\n\ 459\ output clk;\n\ 460\ reg clk;\n\ 461\\n\ 462\ initial begin clk = 0; forever #period clk <= !clk; end\n\ 463\\n\ 464\endmodule\n\ 465\\n"; 466 467(*****************************************************************************) 468(* ClockvInst out n "clk" prints, using function out, an instance of Clock *) 469(* driving a line named "clk" and with n units of time between edges. *) 470(*****************************************************************************) 471val ClockvInst_count = ref 0; 472fun ClockvInst (out:string->unit) [("period",period)] [clk_name] = 473 let val count = !ClockvInst_count 474 val _ = (ClockvInst_count := count+1); 475 val inst_name = "Clock" ^ "_" ^ Int.toString count 476 in 477 (out " Clock "; out inst_name; 478 out " (";out clk_name; out ");"; 479 out " defparam ";out inst_name; out ".period = "; out period; 480 out ";\n\n") 481 end; 482 483(*****************************************************************************) 484(* Add a binary operator (gives compatibility with old code) *) 485(*****************************************************************************) 486fun AddBinop (_:string, (hbinop,vbinop)) = 487 add_vsynth[(hbinop, fn[i1,i2] => (i1 ^ " " ^ vbinop ^ " " ^ i2))]; 488 489 490(*****************************************************************************) 491(* Generate Verilog statement to implement a component *) 492(* *) 493(* ``DTYPE T (clk,inp,out)`` --> dtype dtype_<n> (clk,inp,out) *) 494(* ``?v. DTYPE v (clk,inp,out)`` --> dtype dtype_<n> (clk,inp,out) *) 495(* ``CONSTANT v out`` --> assign out = v; *) 496(* ``COMB f (i1<>...<>in,out)`` --> call generate_verilog ``f`` *) 497(*****************************************************************************) 498fun MAKE_COMPONENT_VERILOG (out:string->unit) tm = 499 if is_DTYPE tm 500 then termToVerilog_DTYPE (out:string->unit) tm else 501 if is_CONSTANT tm 502 then 503 let val (c, out_var) = dest_CONSTANT tm 504 val out_name = var_name out_var 505 in 506 (out "/*\n"; out(term2string tm); out "\n*/\n"; 507 out "assign "; out out_name; out " = "; out c; out ";\n\n") 508 end else 509 if is_COMB tm 510 then 511 let val (f, in_names, out_names) = dest_COMB tm 512 val ml_fun = (lookup_vsynth f 513 handle e => (print_term f; 514 print "\n"; print "not in vsynth_lib\n"; 515 raise e)) 516 val vstring = (ml_fun in_names 517 handle e => (print "ML function associated in vsynth_lib with:\n"; 518 print_term f; print "\nfails on\n"; 519 print_term(fst(dest_pair(rand tm))); print "\n"; 520 raise e)) 521 in 522 (out "/*\n"; out(term2string tm); out "\n*/\n"; 523 out "assign "; 524 if null(tl out_names) 525 then out(hd out_names) 526 else (out "{"; 527 out(hd out_names); 528 map (fn s => (out ","; out s)) (tl out_names); 529 out "}"); 530 out " = "; out vstring; out ";\n\n") 531 end 532 else (print "Can't generate Verilog for:\n"; 533 print_term tm; print "\n"; 534 raise ERR "MAKE_COMPONENT_VERILOG" "bad component term"); 535 536 537(* 538** MAKE_VERILOG 539** name 540** (|- InRise clk 541** ==> 542** (?v0 .... vn. <circuit>) 543** ==> 544** DEV Spec (load at clk, 545** (inp1 <> ... <> inpu) at clk, 546** done at clk, 547** (out1 <> ... <> outv) at clk)) 548** output_stream 549** 550** creates a module called name with header: 551** 552** module name (clk,load,inp1,...,inpu,done,out1,...,outv); 553** input clk,load; 554** input [<size>:0] inp1,inp2; 555** output done; 556** output [<size>:0] out; 557** wire clk,done; 558** 559** where <size> is the appropriate width computed from the types. 560** Body generated using MAKE_COMPONENT_VERILOG. 561*) 562 563 564(* New version that generates behavioral Verilog for combinational logic *) 565fun MAKE_VERILOG name thm out = 566 let val (spec_tm, 567 (clk, load_tm,inpl,done_tm,outl), 568 wire_vars, 569 modules) = dest_cir thm 570 val clk_name = var_name clk 571 val load_name = var_name load_tm 572 val inp_names = map var_name inpl 573 val done_name = var_name done_tm 574 val out_names = map var_name outl 575 val module_args = 576 [clk_name,load_name] @ inp_names @ [done_name] @ out_names 577 in 578 (out("// This file defines module " ^ name ^ " [Created: " ^ date() ^ "]\n\n"); 579 out("// Definition of Dtype register component\n\n"); 580 out DTYPEvDef; 581 out("\n// Definition of module " ^ name ^ "\n"); 582 out "module "; 583 out name; 584 out " ("; 585 map out (add_commas module_args); 586 out ");\n"; 587 out(" input " ^ clk_name ^ "," ^ load_name ^ ";\n"); 588 map 589 (fn v => out(" input [" ^ var2size v ^ ":0] " ^ var_name v ^ ";\n")) 590 inpl; 591 out(" output " ^ done_name ^ ";\n"); 592 map 593 (fn v => out(" output [" ^ var2size v ^ ":0] " ^ var_name v ^ ";\n")) 594 outl; 595 out(" wire " ^ clk_name ^ "," ^ done_name ^ ";\n"); 596 out "\n"; 597 map 598 (fn v => out(" wire [" ^ var2size v ^ ":0] " ^ var_name v ^ ";\n")) 599 wire_vars; 600 out "\n"; 601 map (MAKE_COMPONENT_VERILOG out) modules; 602 out"endmodule\n\n") 603 end; 604 605 606(* Example for testing 607val out = print 608and clk_name = "clk" 609and load_name = "load" 610and done_name = "done" 611and stimulus = [("inp1", "5"),("inp2","7")]; 612*) 613 614(*****************************************************************************) 615(* Print test bench stimulus in Verilog *) 616(*****************************************************************************) 617fun printStimulus (out:string->unit) clk_name load_name done_name stimulus = 618 (out(" always @(posedge " ^ clk_name ^") if (" ^ done_name ^ ")\n"); 619 out(" begin\n"); 620 out(" #1 " ^ load_name ^ " = 1;\n"); 621 out(" #1 "); 622 map 623 (fn (inname,inval) => out(inname ^ " = " ^ inval ^ "; ")) 624 stimulus; 625 out("\n"); 626 out(" forever @(posedge " ^ clk_name ^ ") if (" ^ done_name ^ ") $finish;\n"); 627 out(" end\n")); 628 629 630(* Example for testing 631val period = 5 632and file_name = "foo" 633and thm = Adder_cir 634and stimulus =[("inp1", "5"),("inp2","7")] 635and name = "Adder" 636and dump_all = true; 637 638printToFile "Foo.vl" (MAKE_SIMULATION period thm stimulus name); 639*) 640 641 642fun MAKE_SIMULATION name thm period stimulus dump_all out = 643 let val (spec_tm, 644 (clk, load_tm,inpl,done_tm,outl), 645 vars, 646 modules) = dest_cir thm 647 val clk_name = var_name clk 648 val load_name = var_name load_tm 649 val inp_names = map var_name inpl 650 val done_name = var_name done_tm 651 val out_names = map var_name outl 652 val module_args = 653 [clk_name,load_name] @ inp_names @ [done_name] @ out_names; 654 in 655 (MAKE_VERILOG name thm out; 656 out "\n"; 657 out ClockvDef; (* Print definition of Clock *) 658 out "module Main ();\n"; 659 out(" wire " ^ clk_name ^ ";\n"); 660 out(" reg " ^ load_name ^ ";\n"); 661 map 662 (fn v => out(" reg [" ^ var2size v ^ ":0] " ^ var_name v ^ ";\n")) 663 inpl; 664 out(" wire " ^ done_name ^ ";\n"); 665 map 666 (fn v => out(" wire [" ^ var2size v ^ ":0] " ^ var_name v ^ ";\n")) 667 outl; 668 out "\n"; 669 out(" initial\n begin\n $dumpfile(\"" ^name ^ ".vcd\");\n"); 670 (if dump_all 671 then out(" $dumpvars(1, " ^ name ^ ");\n") 672 else 673 (out(" $dumpvars(1,"); 674 map out (add_commas module_args); 675 out ");\n")); 676 out" end\n\n"; 677 out(" initial " ^ load_name ^ " = 0;\n\n"); 678 printStimulus out clk_name load_name done_name stimulus; 679 out "\n"; 680 ClockvInst out [("period", Int.toString period)] [clk_name]; (* Create a clock *) 681 out(" " ^ name ^ " " ^ name ^ " ("); 682 map out (add_commas module_args); 683 out ");\n\n"; 684 out"endmodule\n") 685 end; 686 687(* 688** PRINT_VERILOG 689** (|- InRise clk 690** ==> 691** (?v0 .... vn. <circuit>) 692** ==> 693** DEV Spec (load at clk, 694** (inp1 <> ... <> inpu) at clk, 695** done at clk, 696** (out1 <> ... <> outv) at clk)) 697** 698** Prints translation to Verilog to a file Spec.vl and creates a module Spec 699* (fails if Spec isn't a constant) 700*) 701 702fun PRINT_VERILOG thm = 703 let val name = fst(dest_const(#1(dest_cir thm))) 704 in 705 printToFile (name ^ ".vl") (MAKE_VERILOG name thm) 706 end; 707 708(*****************************************************************************) 709(* Flag (default false) to determine if all variables are dumped, *) 710(* or just the top level ones. *) 711(*****************************************************************************) 712val dump_all_flag = ref false; 713 714(* 715** PRINT_SIMULATION 716** (|- InRise clk 717** ==> 718** (?v0 .... vn. <circuit>) 719** ==> 720** DEV Spec (load at clk, 721** (inp1 <> ... <> inpu) at clk, 722** done at clk, 723** (out1 <> ... <> outv) at clk)) 724** period stimulus (!dump_all_flag) 725** 726** Prints translation to Verilog and a stimulus to a file Spec.vl and creates 727** a module Main that invokes module Spec connected to a simulation environment 728** described by stimulus. If 729** (fails if Spec isn't a constant) 730*) 731 732fun PRINT_SIMULATION thm period stimulus = 733 let val name = fst(dest_const(#1(dest_cir thm))) 734 in 735 printToFile 736 (name ^ ".vl") 737 (MAKE_SIMULATION name thm period stimulus (!dump_all_flag)) 738 end; 739 740(*****************************************************************************) 741(* User resettable paths of Verilog simulator and waveform viewer *) 742(*****************************************************************************) 743 744val iverilog_path = ref "/usr/bin/iverilog"; 745val vvp_path = ref "/usr/bin/vvp"; 746val gtkwave_path = ref "/usr/bin/gtkwave -a"; 747 748(* 749val cver_path = ref "./gplcver-2.10c.linux.bin/bin/cver"; 750val dinotrace_path = ref "./gplcver-2.10c.linux.bin/bin/dinotrace"; 751*) 752val cver_path = ref "/Users/konradslind/Desktop/gplcver-2.10c.osx.bin/bin/cver"; 753val dinotrace_path = ref "/Users/konradslind/Desktop/gplcver-2.10c.osx.bin/bin/dinotrace"; 754 755val vlogger_path = ref "/usr/bin/vlogcmd"; 756 757(* 758** Test for success of the result of Process.system 759** N.B. isSuccess was expected to primitive in next release of 760** Moscow ML, and Process.status will then lose eqtype status 761** (not happened yet apparently) 762*) 763 764val isSuccess = Process.isSuccess; 765 766(*****************************************************************************) 767(* Run iverilog on name.vl *) 768(*****************************************************************************) 769fun iverilog name = 770 let val vvp_file = (name ^ ".vvp") 771 val iverilog_command = ((!iverilog_path) ^ " -o " ^ vvp_file 772 ^ " " ^ name ^ ".vl") 773 val code1 = Process.system iverilog_command 774 val _ = if isSuccess code1 775 then print(iverilog_command ^ "\n") 776 else print 777 ("Warning:\n Process.system reports failure signal returned by\n " 778 ^ iverilog_command ^ "\n") 779 val vvp_command = ((!vvp_path) ^ " " ^ vvp_file) 780 val code2 = Process.system vvp_command 781 val _ = if isSuccess code2 782 then print(vvp_command ^ "\n") 783 else print 784 ("Warning:\n Process.system reports failure signal returned by\n " 785 ^ vvp_command ^ "\n") 786 in 787 () 788 end; 789 790(*****************************************************************************) 791(* Run cver on name.vl *) 792(*****************************************************************************) 793fun cver name = 794 let val cver_command = ((!cver_path) ^ " " ^ name ^ ".vl") 795 val code = Process.system cver_command 796 val _ = if isSuccess code 797 then print(cver_command ^ "\n") 798 else print 799 ("Warning:\n Process.system reports failure signal returned by\n " 800 ^ cver_command ^ "\n") 801 in 802 () 803 end; 804 805(*****************************************************************************) 806(* Run gtkwave on name.vcd *) 807(*****************************************************************************) 808fun gtkwave name = 809 let val vcd_file = (name ^ ".vcd") 810 val gtkwave_command = ((!gtkwave_path) ^ " " ^ vcd_file ^ "&") 811 val code = Process.system gtkwave_command 812 val _ = if isSuccess code 813 then print(gtkwave_command ^ "\n") 814 else print 815 ("Warning:\n Process.system reports failure signal returned by\n " 816 ^ gtkwave_command ^ "\n") 817 in 818 () 819 end; 820 821(*****************************************************************************) 822(* Run vlogger on name.vl *) 823(*****************************************************************************) 824fun vlogger name = 825 let val vlogger_command = ((!vlogger_path) ^ " " ^ name ^ ".vl") 826 val code = Process.system vlogger_command 827 val _ = if isSuccess code 828 then print(vlogger_command ^ "\n") 829 else print 830 ("Warning:\n Process.system reports failure signal returned by\n " 831 ^ vlogger_command ^ "\n") 832 in 833 () 834 end; 835 836(*****************************************************************************) 837(* Run dinotrace on name.vcd *) 838(*****************************************************************************) 839fun dinotrace name = 840 let val vcd_file = (name ^ ".vcd") 841 val dinotrace_command = ((!dinotrace_path) ^ " " ^ vcd_file ^ "&") 842 val code = Process.system dinotrace_command 843 val _ = if isSuccess code 844 then print(dinotrace_command ^ "\n") 845 else print 846 ("Warning:\n Process.system reports failure signal returned by\n " 847 ^ dinotrace_command ^ "\n") 848 in 849 () 850 end; 851 852(* 853val verilog_simulator = ref iverilog; 854val waveform_viewer = ref gtkwave; 855*) 856 857val verilog_simulator = ref cver; 858val waveform_viewer = ref dinotrace; 859 860(* Example for testing 861use "Ex3.ml"; 862 863val thm = DoubleDouble_cir 864and inputs = [("inp", "5")]; 865*) 866 867(*****************************************************************************) 868(* Default values for simulation *) 869(*****************************************************************************) 870 871val period_default = ref 5; 872 873fun SIMULATE thm stimulus = 874 let val _ = PRINT_SIMULATION thm (!period_default) stimulus 875 val name = fst(dest_const(#1(dest_cir thm))) 876 val _ = (!verilog_simulator) name 877 val _ = (!waveform_viewer) name 878 in 879 () 880 end; 881 882end (* local open *) 883 884end (* vsynth *) 885