The Bluespec System Verilog language is increasingly seen as a viable and productive alternative to conventional RTL coding for hardware design. For compiler writers like myself, the best way to learn a new language was to write a toy compiler for it. Also, where there's a lack of formal semantics for a language, writing a compiler is a good way to learn about the important and/or arbitrary decisions that have to be made. (These seem to be in the scheduler and in the way implicit guards of implicit guards are processed)
The user manual from Bluespec Inc may have restricted circulation, so this informal study was based on a couple of published studies: `HARDWARE LANGUAGES AND PROOF' by Dominic Richards of Manchester University and `A Unified Model for Hardware/Software Codesign' by Nirav Dave when at MIT.
This article gives the essence of a compiler for Bluespec. This toy compiler was coded in F Sharp using the HPR/LS library. This library provides various logic manipulation facilities and output functions for SMV, SystemC, Verilog and so on. Rather than initially writing a Bluespec parser, the test abstract-syntax trees were manually entered as separate F Sharp source files. This is actually an attractive approach but needs tidying up from what is here. The attraction is that Bluespec has a static elaborator which is basically a Haskel interpreter, but by embedding our constructs in F Sharp instead, we have the power of the ML dialect of F Sharp to do exactly the same kind of elaboration. All of the higher-order iterators and functors are exactly the same, modulo inserting 'fun () -> ' in a few places to get lazy behaviour. The good work needed is to use the domain-specific language (DSL) embedding facilities of F Sharp for the elaborated leaves. I might do this if I update this page.
(BTW: A good student project would be to add a parser for the official concrete syntax: Here is a basic Bluespec parser in FSYACC form FSHARP YACC BSV TOY PARSER and example run.)
let test_ast1 =
(* module test1();
Reg#(#UInt(15)) ctr1 <- mk_register(0)
rule test_ast1 (True) ;
ctr1.write(ctr1.read()+1)
endrule
endmodule
*)
Bsv_moduleDef("test1",
([], [], Bsv_typen "Empty"),
[
Bsv_varDeclAssign("ctr1", [B_num [15]; B_num[1]], "mkReg", []);
Bsv_rule("test_ast1", B_true, [ g_write("ctr1", B_diadic(V_plus, g_read("ctr1"), B_num[1]))])
],
[])
The first test generated the following output (which works fine: ctr is incremented on every clock cycle):
// CBG Orangepath HPR/LS System
// /home/djg11/d320/hprls/bsvc/bsv.exe -vnl test1.vnl test1
module test1(input clk, input RST_N);
reg test_ast1_FIRE;
reg [14:0] test1_ctr1_DREG;
reg [14:0] test1_ctr1_Din;
wire test1_ctr1_RDY;
reg test1_ctr1_EN;
always @(posedge clk ) begin
if (!RST_N || test1_ctr1_EN) test1_ctr1_DREG <= (!RST_N ? 0: test1_ctr1_Din);
end
assign test_ast1_FIRE = 1;
always @(*) test1_ctr1_EN = test_ast1_FIRE;
always @(*) test1_ctr1_Din = 1+test1_ctr1_DREG;
// 2 vectors of width 1
// 2 vectors of width 15
// Total state bits in module = 32 bits.
// 1 continuously assigned (wire/non-state) bits
endmodule
// eof (HPR/LS Verilog)
The second test was to compile my Dining Philosophers example: Dining Philosophers in Bluespec Verilog.
Not originally having a parser, I had to manually enter the syntax tree for the example. Fortunately it is not too long.
The main part of the grammar is:
// Bluespec: Toy abstract syntax (may not be right!)
// Various modifiers for an interface:
type bsv_provisos_t =
| Proviso_alwaysReady
| Proviso_alwaysEnabled
;
// Method prototype protocol has one of these three forms:
type bsv_protoprotocol_t =
| BsvProtoValue of bsv_type_name_t
| BsvProtoActionValue of bsv_type_name_t
| BsvProtoAction
and bsv_type_name_t =
| Bsv_typen of string // for now - separate from bsv_if_t ... but can join.
| Bsv_typen_uint_ns // Native/primitive run-time type
| Bsv_typen_uint1 of int // Native/primitive run-time type
| Bsv_typen_action
// Method prototype: has name, provisio/pragmas, return type and method formals (pairs of formal and actuals so-far bound).
and bsv_methodProto_t = Bsv_methodProto of string * bsv_provisos_t list * bsv_protoprotocol_t * (bsv_type_name_t * string) list
and bsv_sigma_protocol_t =
| BsvValue
| BsvAction of hexp_t option * (hbexp_t * hexp_t) // (en-net if needed) * (rdy-x, rdy-net)
and bsv_sigma_t = Bsv_current of string * bsv_sigma_protocol_t * (bsv_type_name_t * hexp_t option) * (hexp_t * hexp_t) list
and actuals_t = (string * (bsv_type_name_t * bsv_exp_t)) list
and formals_t = (bsv_exp_t * string) list
and bsv_moduleStmt_t = // Or actionValueStmt ?
| Bsv_varDeclAssign of string * bsv_exp_t list * string * string list
| Bsv_rule of string * bsv_bexp_t * bsv_moduleStmt_t list
| Bsv_assignStmt of string * bsv_exp_t
| Bsv_eascActionStmt of bsv_exp_t
| Bsv_pliStmt of string * bsv_exp_t list // for $display and so on
| Bsv_beginEndStmt of bsv_moduleStmt_t list
| Bsv_ifThenStmt of bsv_bexp_t * bsv_moduleStmt_t * bsv_moduleStmt_t option
| Bsv_whileStmt of bsv_bexp_t * bsv_moduleStmt_t * bsv_moduleStmt_t option | Bsv_returnStmt of bsv_exp_t // Only in actionvalue blocks.
| Bsv_CaseStmt of bsv_exp_t * (bsv_exp_t * bsv_moduleStmt_t) list * bsv_moduleStmt_t option
| Bsv_methodDef of string * formals_t * bsv_bexp_t * bsv_moduleStmt_t list
| Bsv_primBuffer of bsv_exp_t * bsv_exp_t (* Only for internal implementation *)
// There are three lots of 'parameters' to the typical module as stored in this triple.
// They are the parametric type args of the exported interface, the parameters to the generate
// function and the list of interfaces, which consists of those used plus the single interface exported.
and bsv_moduleParams_t = (bsv_type_name_t * string) list * (bsv_type_name_t * string) list * bsv_type_name_t
// The Bluespec interface definition: Generic parameters and list of methods:
and bsv_if_t = Bsv_if of (bsv_type_name_t * string) list * bsv_methodProto_t list
// Boolean expressions
and bsv_bexp_t =
| B_true
| B_false
| B_firing of string // Backdoor access to the composite guard for any rule.
| B_not of bsv_bexp_t
| B_and of bsv_bexp_t list
| B_or of bsv_bexp_t list
| B_bexp of hbexp_t // Pre-compiled forms
| B_bdiop of x_bdiop_t * bsv_exp_t list // Equality, less than and orreduce where list is a singleton.
| B_orred of bsv_exp_t
// Integer expressions
and bsv_exp_t =
| B_num of int list
| B_blift of bsv_bexp_t
| B_query of bsv_bexp_t * bsv_exp_t * bsv_exp_t
| B_var of string
| B_string of string
| B_hexp of hexp_t
| B_fsmStmt of bsv_exprFsmStmt_t
| B_ifcRef of string // Interface reference
| B_diadic of x_diop_t * bsv_exp_t * bsv_exp_t
| B_apply of string list * bsv_exp_t list
// Finite-state machine sub language.
and bsv_exprFsmStmt_t =
| Bsv_seqFsmStmt of bsv_exprFsmStmt_t list
| Bsv_parFsmStmt of bsv_exprFsmStmt_t list
| Bsv_ifFsmStmt of bsv_bexp_t * bsv_exprFsmStmt_t * bsv_exprFsmStmt_t option
| Bsv_whileFsmStmt of bsv_bexp_t * bsv_exprFsmStmt_t
| Bsv_repeatFsmStmt of bsv_exprFsmStmt_t
| Bsv_eascFsmStmt of bsv_exp_t
| Bsv_breakFsmStmt
| Bsv_continueFsmStmt
;
The encoding of the spoon (really should be called a fork!) and the philosopher and the table of five of them look like this:
(* interface Spoon_if;
method Action pickup();
method Action putdown();
endinterface
*)
Bsv_ifDef("Spoon_if",
Bsv_if([],
[
Bsv_methodProto("pickup", [], BsvProtoAction, []);
Bsv_methodProto("putdown", [], BsvProtoAction, []);
])
)
(*
module spoon (Spoon_if) ;
Reg#(Bool) inuse <- mkReg(?);
method Action pickup() if (!inuse);
action
inuse <= True;
endaction
endmethod
method Action putdown();
action
inuse <= False;
endaction
endmethod
endmodule
*)
Bsv_moduleDef("Spoon",
([], [], Bsv_typen "Spoon_if"),
[
Bsv_varDeclAssign("inuse", [B_num[1]; B_num[0]], "mkReg", []);
Bsv_methodDef("pickup", [], B_bdiop(V_dned, [g_read "inuse"; B_num[1]]), [ g_write("inuse", B_num[1]); Bsv_pliStmt("$display", [B_string "pickup"]) ]);
Bsv_methodDef("putdown", [], B_true, [ g_write("inuse", B_num[0]); Bsv_pliStmt("$display", [B_string "putdown"]) ])
],
[])
(* interface Random_if;
method ActionValue#(UInt#(15)) gen();
endinterface
*)
Bsv_ifDef("Random_if",
Bsv_if([],
[
Bsv_methodProto("gen", [], BsvProtoActionValue(Bsv_typen_uint1 15), []);
])
)
(* module mkRandom_gen #(UInt#(15) seed) (Random_if);
Reg#(UInt#(15)) prbs <- mkReg(seed);
method ActionValue#(UInt#(15)) gen();
prbs <= (prbs << 1) | (((prbs >> 14) ^ (prbs >> 13)) & 1);
return prbs;
endmethod
endmodule
*)
Bsv_moduleDef("mkRandom_gen",
([(Bsv_typen "int", "seed")], [], Bsv_typen "Random_if"),
[
Bsv_varDeclAssign("prbs", [B_num[15]; B_var "seed"], "mkReg", []);
Bsv_methodDef("gen", [], B_true,
[ g_write("prbs", B_diadic(V_bitor, B_diadic(V_lshift, g_read "prbs", B_num[1]), B_diadic(V_bitand, (B_diadic(V_bitor, B_diadic(V_rshift, g_read "prbs", B_num[14]), B_diadic(V_rshift, g_read "prbs", B_num[13]))), B_num[1])));
Bsv_returnStmt(g_read "prbs");
])
],
[])
Bsv_moduleDef("Philo",
([(Bsv_typen "int", "seed"); (Bsv_typen "int", "on")],
[(Bsv_typen "Spoon_if", "left"); (Bsv_typen "Spoon_if", "right")], Bsv_typen "Empty"),
[
Bsv_varDeclAssign("gen", [B_var "seed"], "mkRandom_gen", []);
Bsv_varDeclAssign("timer", [B_num[15]; B_num[0]], "mkReg", []);
Bsv_varDeclAssign("x", [B_num[15]; B_num[0]], "mkReg", []);
Bsv_rule("foo", B_bdiop(V_dned, [g_read("timer"); B_num[0]]), [ g_write("timer", B_diadic(V_minus, g_read "timer", B_num[1]))]);
Bsv_varDeclAssign("eating", [B_num[1]; B_num[0]], "mkReg", []);
Bsv_assignStmt("seq_behaviour",
B_fsmStmt(
Bsv_whileFsmStmt(B_true,
Bsv_seqFsmStmt
[
fsm_write("x", g_actionVal("gen", "gen", []));
fsm_write("timer", B_diadic(V_bitand, g_read "timer", B_num[31]));
fsm_await(B_bdiop(V_deqd, [g_read "timer"; B_num[0]]));
fsm_action("left", "pickup", []);
fsm_noAction();
fsm_write("x", g_actionVal("gen", "gen", []));
fsm_write("timer", B_diadic(V_bitand, g_read "timer", B_num[31]));
fsm_await(B_bdiop(V_deqd, [g_read "timer"; B_num[0]]));
fsm_action("right", "pickup", []);
fsm_noAction();
fsm_write("eating", B_num[1]);
fsm_write("timer", B_var "on");
fsm_await(B_bdiop(V_deqd, [g_read "timer"; B_num[0]]));
fsm_write("eating", B_num[0]);
fsm_noAction();
fsm_action("left", "putdown", []);
fsm_noAction();
fsm_action("right", "putdown", []);
fsm_noAction();
])));
Bsv_varDeclAssign("FSM", [B_var "seq_behaviour" ], "mkFSM", [ ]);
Bsv_rule("kickoff", B_true, [ g_action("FSM", "start", []) ]);
],
[])
Bsv_moduleDef("philoBENCH",
([], [], Bsv_typen "Empty"),
[
Bsv_varDeclAssign("spoon0", [], "Spoon", []);
Bsv_varDeclAssign("spoon1", [], "Spoon", []);
Bsv_varDeclAssign("spoon2", [], "Spoon", []);
Bsv_varDeclAssign("spoon3", [], "Spoon", []);
Bsv_varDeclAssign("spoon4", [], "Spoon", []);
Bsv_varDeclAssign("philo0", [B_num[3]; B_num[7] ], "Philo", [ "spoon0"; "spoon1" ]);
Bsv_varDeclAssign("philo1", [B_num[4]; B_num[4] ], "Philo", [ "spoon1"; "spoon2" ]);
Bsv_varDeclAssign("philo2", [B_num[2]; B_num[9] ], "Philo", [ "spoon3"; "spoon2" ]);
Bsv_varDeclAssign("philo3", [B_num[3]; B_num[6] ], "Philo", [ "spoon3"; "spoon4" ]);
Bsv_varDeclAssign("philo4", [B_num[3]; B_num[6] ], "Philo", [ "spoon4"; "spoon0" ]);
],
[])
;
Note that I have reversed the spoons to philosopher number 2. This stops the system from deadlocking straightaway!
The Verilog RTL output looks as follows (note: this was the very first run and there might be some bugs in this, but it seems to work!) HERE.
Does this deadlock? The HPR library can output also an NuSMV file of this design. We can give SMV the -ctt command line flag and it will check for deadlock (eventually?).
I shall put all the source files on the following link for your own experiments: HERE.
The above toy compiler has a default rule precedence based on the textual order of the rules in the source code. It's not hard to add priorities.
The above compiler does not have the interlock that BSV defaults to ON for each rule that stops it firing more than once per cycle. This can be added where the comment says.
Finally, the above compiler does not check alternate compositions of rule pairs to see if they have the same effect, but a simple approach based on textual equivalence of effect would work quite well because the expressions are all converted to a normal memoized form by the HPR library, so most minor artefacts arising from alternate compositions, such as operator association and operand interchange in commutative operators are eliminated.
mono bsv.exe -incdir=/home/djg11/d320/hprls/bsvc/smalltests -cpp=disable -comb-assignment-delay=10 -vnl=dut.v smalltests/SimpleProcessorTb.bsv cver dut.v vsys.v GPLCVER_2.11a of 07/05/05 (Linux-elf). Copyright (c) 1991-2005 Pragmatic C Software Corp. All Rights reserved. Licensed under the GNU General Public License (GPL). See the 'COPYING' file for details. NO WARRANTY provided. Today is Wed Nov 7 14:44:56 2012. Compiling source file "dut.v" Compiling source file "vsys.v" Highest level modules: SIMSYS 48: output regs[ 1] = 3 49: Halt at pc13 There were 0 error(s), 0 warning(s), and 24 inform(s).
The online Bluespec examples define a simple microprocessor that is provided with an assembly coding of Euclid's algorith. The above plot shows the toy compiler can now parse and correctly execute the processor and the example algorithm: the GCD of 27 and 15 is 3 which is printed from R1 at the end of the computation. The delay at the start is the download of the program into the processor by the testbench. Mind you, this hardly stretches the interesting parts of the Bluespec scheduler.
Listing ((C) Bluespec Inc):
Instruction code [14] =
{
tagged MovI { rd: R0, v: 0 }, // 0: The constant 0
tagged MovI { rd: R1, v: 15 }, // 1: x = 21
tagged MovI { rd: R2, v: 27 }, // 2: y = 27
// label_loop
tagged Brz { rs: R2, dest:label_done }, // 3: if (y == 0) goto done
tagged Gt { rd: R3, rs1: R1, rs2: R2 }, // 4: tmp = (x > y)
tagged Brz { rs: R3, dest: label_subtract }, // 5: if (x <= y) goto subtract
// swap
tagged Minus { rd: R3, rs1: R1, rs2: R0 }, // 6: tmp = x;
tagged Minus { rd: R1, rs1: R2, rs2: R0 }, // 7: x = y;
tagged Minus { rd: R2, rs1: R3, rs2: R0 }, // 8: y = tmp;
tagged Br label_loop, // 9: goto loop
// label_subtract
tagged Minus { rd: R2, rs1: R2, rs2: R1 }, // 10: y = y - x
tagged Br label_loop, // 11: goto loop
// label_done
tagged Output R1, // 12: output x
// label_last
tagged Halt // 13: halt
};
Verilog object file generated: dut.v.
Simon Moore implemented Chuck Thacker's Tiny3 Processor in Bluespec. Simon's source files are here SWM Tiny3. This design now (Jan 2013) goes through the Toy Compiler and works!
The test program is coded in an assembly language entirely written in Bluespec. It is a simple program that writes the integers 9 down to 0 to the output FIFO.
function List#(AsmLineT) my_program(function ImmT findaddr(String label)) =
/*0*/ cons(asmi("", 0, 0), // Keep register 0 clear.
/*1*/ cons(asmi("", 1, 10), // put 10 in r1
/*2*/ cons(asmi("", 2, findaddr("loop")), // loop address in r2
/*3*/ cons(asm("loop", OpOut, FDECb, ShiftNone, SkipNever, 1, 0, 1), // r1-- and output
/*4*/ cons(asm("", OpJump, FaORb, ShiftNone, SkipZero, 3, 2, 0), // jump r2 if not zero
/*5*/ cons(asm("", OpReserved, Freserved, ShiftNone, SkipNever, 0, 0, 0), // stop processor
tagged Nil))))));
Simulation output:
cver dut.v vsys.v
GPLCVER_2.12a of 05/16/07 (Linux-elf).
Copyright (c) 1991-2007 Pragmatic C Software Corp.
All Rights reserved. Licensed under the GNU General Public License (GPL).
See the 'COPYING' file for details. NO WARRANTY provided.
Today is Sun Jan 20 18:39:48 2013.
Compiling source file "dut.v"
Compiling source file "vsys.v"
Highest level modules:
SIMSYS
End of prog load
2100: fetch 00 80000000:
2700: doSkip = False
2700: r 0 = imm = 0
2900: fetch 01 8100000a:
3500: doSkip = False
3500: r 1 = imm = 10
3700: fetch 02 82000003:
4300: doSkip = False
4300: r 2 = imm = 3
4500: fetch 03 01000583:
5100: doSkip = False
5100: rd <- 1 9
Write out 00000009
5300: fetch
5300: output = 9 04 03040296:
5900: doSkip = False
6100: fetch 03 01000583:
6700: doSkip = False
6700: rd <- 1 8
Write out 00000008
6900: fetch
6900: output = 8 04 03040296:
7500: doSkip = False
7700: fetch 03 01000583:
8300: doSkip = False
8300: rd <- 1 7
Write out 00000007
8500: fetch
8500: output = 7 04 03040296:
9100: doSkip = False
9300: fetch 03 01000583:
9900: doSkip = False
9900: rd <- 1 6
Write out 00000006
10100: fetch
10100: output = 6 04 03040296:
10700: doSkip = False
10900: fetch 03 01000583:
11500: doSkip = False
11500: rd <- 1 5
Write out 00000005
11700: fetch
11700: output = 5 04 03040296:
12300: doSkip = False
12500: fetch 03 01000583:
13100: doSkip = False
13100: rd <- 1 4
Write out 00000004
13300: fetch
13300: output = 4 04 03040296:
13900: doSkip = False
14100: fetch 03 01000583:
14700: doSkip = False
14700: rd <- 1 3
Write out 00000003
14900: fetch
14900: output = 3 04 03040296:
15500: doSkip = False
15700: fetch 03 01000583:
16300: doSkip = False
16300: rd <- 1 2
Write out 00000002
16500: fetch
16500: output = 2 04 03040296:
17100: doSkip = False
17300: fetch 03 01000583:
17900: doSkip = False
17900: rd <- 1 1
Write out 00000001
18100: fetch
18100: output = 1 04 03040296:
18700: doSkip = False
18900: fetch 03 01000583:
19500: doSkip = False
19500: rd <- 1 0
Write out 00000000
19700: fetch
19700: output = 0 04 03040296:
20300: doSkip = True
20500: fetch 06 6c697374:
21100: doSkip = False
21100: rd <- 108 x
21300: fetch 07 6c697374:
21900: doSkip = True
21900: rd <- 108 x
22100: fetch 09 xxxxxxxx:
Halted at location **vsys.v(16) time 35000 from call to $finish.
There were 0 error(s), 1 warning(s), and 63 inform(s).
(C) 2012 Orangepath Project. DJ Greaves.